|
| 1 | +{-# OPTIONS --safe --without-K #-} |
| 2 | + |
| 3 | +------------------------------------------------------------------------ |
| 4 | +-- Gate 2 audit: N5Falsifier |
| 5 | +-- |
| 6 | +-- VERDICT: the N5 candidate (`characteristic.RoleGraded.choreo-grade-commute`) |
| 7 | +-- SURVIVES the sharpened falsifier. The candidate is ready for adoption |
| 8 | +-- as the fifth gate-2 nominee in `roadmap-gates.adoc`. |
| 9 | +-- |
| 10 | +-- Background. STATE.next-actions q2-3 (low-priority bookkeeping |
| 11 | +-- post-EI-2) calls for adopting `choreo-grade-commute` as nominee N5. |
| 12 | +-- The gate-2 audit doc surface flagged it as a candidate fifth nominee |
| 13 | +-- but did not adopt pending a falsifier attempt of the same shape that |
| 14 | +-- successfully struck down N3 (`knowledge-and-controlled-degradation`, |
| 15 | +-- formalised in `characteristic.IntegrationAudit`). |
| 16 | +-- |
| 17 | +-- The N3 sharpened falsifier exhibited: |
| 18 | +-- |
| 19 | +-- * `split-knowledge` — pure-choreo restatement (no `degrade`). |
| 20 | +-- * `split-merging` — pure-grade restatement (no role). |
| 21 | +-- * `N3-is-product` — original ≡ literal pair of the two splits. |
| 22 | +-- * `split-merging-uses-no-hypotheses` — conjunct 2 ignores N3's |
| 23 | +-- hypotheses, witnessing "no shared data between conjuncts". |
| 24 | +-- |
| 25 | +-- For N5, the same shape is structurally inapplicable: both sides of |
| 26 | +-- the equation reference both decoration witnesses (`rp`, `gp`) and |
| 27 | +-- the same data (`e`). There is no pair of pure-axis facts whose |
| 28 | +-- product reproduces the theorem, because the content of N5 is the |
| 29 | +-- *coincidence* of two action orderings on shared data. |
| 30 | +-- |
| 31 | +-- Honest narrowing (per STATE standing-decisions sd-002). The recipe |
| 32 | +-- is organising vocabulary, NOT distinctness load. Adoption of N5 is |
| 33 | +-- bookkeeping completion of the gate-2 nominee table; the gate-1 |
| 34 | +-- distinctness load is carried by truncation (echo-not-prop family) |
| 35 | +-- and 2-cell arguments (Sophisticated submodules), independently of |
| 36 | +-- this theorem. |
| 37 | +-- |
| 38 | +-- Recommendation (closing). Add `RoleGraded.choreo-grade-commute` as |
| 39 | +-- the fifth gate-2 nominee N5 in `roadmap-gates.adoc`, raising the |
| 40 | +-- audit count to 5-of-5 across the four characteristic constructions. |
| 41 | +------------------------------------------------------------------------ |
| 42 | + |
| 43 | +module characteristic.N5Falsifier where |
| 44 | + |
| 45 | +open import Data.Product.Base using (Σ; _×_; _,_) |
| 46 | +open import Relation.Binary.PropositionalEquality using (_≡_; refl) |
| 47 | + |
| 48 | +open import EchoChoreo using |
| 49 | + ( Client |
| 50 | + ; Server |
| 51 | + ; client-to-server |
| 52 | + ; _⊑c_ |
| 53 | + ; c⊑c |
| 54 | + ; c⊑s |
| 55 | + ; s⊑s |
| 56 | + ) |
| 57 | +open import EchoGraded using |
| 58 | + ( _≤g_ |
| 59 | + ; keep |
| 60 | + ; keep≤keep |
| 61 | + ) |
| 62 | +open import characteristic.RoleGraded using |
| 63 | + ( RoleGEcho |
| 64 | + ; applyRole |
| 65 | + ; applyGrade |
| 66 | + ; choreo-grade-commute |
| 67 | + ) |
| 68 | + |
| 69 | +------------------------------------------------------------------------ |
| 70 | +-- Same-data witness |
| 71 | +-- |
| 72 | +-- Both sides of N5's equation are functions of all three binders |
| 73 | +-- (`rp`, `gp`, `e`). Below, `LHS` and `RHS` package each side as a |
| 74 | +-- function consuming the full triple, making the data-dependency |
| 75 | +-- syntactic. Compare with N3, where `split-merging` was a closed term |
| 76 | +-- referencing none of N3's hypotheses; here neither side admits a |
| 77 | +-- closed-form restatement that drops one of `rp`, `gp`, or `e`. |
| 78 | +------------------------------------------------------------------------ |
| 79 | + |
| 80 | +LHS : |
| 81 | + ∀ {r1 r2 g1 g2} |
| 82 | + (rp : r1 ⊑c r2) (gp : g1 ≤g g2) (e : RoleGEcho r1 g1) → |
| 83 | + RoleGEcho r2 g2 |
| 84 | +LHS rp gp e = applyGrade gp (applyRole rp e) |
| 85 | + |
| 86 | +RHS : |
| 87 | + ∀ {r1 r2 g1 g2} |
| 88 | + (rp : r1 ⊑c r2) (gp : g1 ≤g g2) (e : RoleGEcho r1 g1) → |
| 89 | + RoleGEcho r2 g2 |
| 90 | +RHS rp gp e = applyRole rp (applyGrade gp e) |
| 91 | + |
| 92 | +-- The equation under audit. Same statement as |
| 93 | +-- `RoleGraded.choreo-grade-commute`, exposed here as a function of |
| 94 | +-- the triple `(rp, gp, e)`. |
| 95 | +N5-equation : |
| 96 | + ∀ {r1 r2 g1 g2} |
| 97 | + (rp : r1 ⊑c r2) (gp : g1 ≤g g2) (e : RoleGEcho r1 g1) → |
| 98 | + LHS rp gp e ≡ RHS rp gp e |
| 99 | +N5-equation = choreo-grade-commute |
| 100 | + |
| 101 | +-- Shared-data Σ witness. Both `LHS rp gp e` and `RHS rp gp e` arise |
| 102 | +-- from a single triple, and the equation between them is recovered |
| 103 | +-- from `choreo-grade-commute`. The Σ-type makes explicit that the |
| 104 | +-- two sides are jointly determined by `(rp, gp, e)`; there is no |
| 105 | +-- decomposition of `(LHS, RHS)` into independent components. |
| 106 | +shared-data : |
| 107 | + ∀ {r1 r2 g1 g2} |
| 108 | + (rp : r1 ⊑c r2) (gp : g1 ≤g g2) (e : RoleGEcho r1 g1) → |
| 109 | + Σ (RoleGEcho r2 g2) (λ lhs → |
| 110 | + Σ (RoleGEcho r2 g2) (λ rhs → |
| 111 | + (lhs ≡ LHS rp gp e) × (rhs ≡ RHS rp gp e) × (lhs ≡ rhs))) |
| 112 | +shared-data rp gp e = |
| 113 | + LHS rp gp e , RHS rp gp e , refl , refl , N5-equation rp gp e |
| 114 | + |
| 115 | +------------------------------------------------------------------------ |
| 116 | +-- Why the N3-shape falsifier does not apply |
| 117 | +-- |
| 118 | +-- For N3, exhibiting `(split-knowledge , split-merging)` as the |
| 119 | +-- literal product was possible because the original was a `_×_` of |
| 120 | +-- two facts that named no common term. For N5, neither side admits |
| 121 | +-- a single-axis restatement at all: stripping `applyRole` from |
| 122 | +-- `LHS rp gp e` discards the `rp` dependency, but the resulting term |
| 123 | +-- `applyGrade gp e` no longer has the type of the original LHS |
| 124 | +-- (which lives in `RoleGEcho r2 g2`, not `RoleGEcho r1 g2`). |
| 125 | +-- |
| 126 | +-- The structural witness of inapplicability is therefore: there is |
| 127 | +-- no pair `(P-choreo, P-grade)` of pure-axis statements such that |
| 128 | +-- `P-choreo × P-grade` has the type of `N5-equation`. A formal |
| 129 | +-- impossibility proof would require quantifying over Agda terms |
| 130 | +-- (meta-level), but the type-level obstruction is visible in the |
| 131 | +-- signatures of `LHS` and `RHS` above: both ineliminably consume |
| 132 | +-- all three binders. |
| 133 | +------------------------------------------------------------------------ |
| 134 | + |
| 135 | +------------------------------------------------------------------------ |
| 136 | +-- Single-axis collapses (both decorations forced to identity) |
| 137 | +-- |
| 138 | +-- When both `rp` and `gp` are identity steps (`c⊑c`/`s⊑s` and |
| 139 | +-- `keep≤keep`), the equation degenerates to reflexivity on `e`. |
| 140 | +-- These cells witness the *absence* of substantive content in the |
| 141 | +-- single-axis halves: if N5 *were* a product of pure-axis facts, the |
| 142 | +-- collapses below would expose non-trivial pure-axis content. They |
| 143 | +-- do not — they all close by `refl` because identity steps are |
| 144 | +-- identity. |
| 145 | +------------------------------------------------------------------------ |
| 146 | + |
| 147 | +-- (rp, gp) = (c⊑c, keep≤keep): both sides reduce to `e ≡ e`. |
| 148 | +collapse-cc-keep : |
| 149 | + (e : RoleGEcho Client keep) → |
| 150 | + applyGrade keep≤keep (applyRole c⊑c e) |
| 151 | + ≡ applyRole c⊑c (applyGrade keep≤keep e) |
| 152 | +collapse-cc-keep e = refl |
| 153 | + |
| 154 | +-- Symmetric case (rp, gp) = (s⊑s, keep≤keep). The source role is |
| 155 | +-- forced to `Server` by the type of `s⊑s : Server ⊑c Server`. |
| 156 | +collapse-ss-keep : |
| 157 | + (e : RoleGEcho Server keep) → |
| 158 | + applyGrade keep≤keep (applyRole s⊑s e) |
| 159 | + ≡ applyRole s⊑s (applyGrade keep≤keep e) |
| 160 | +collapse-ss-keep e = refl |
| 161 | + |
| 162 | +------------------------------------------------------------------------ |
| 163 | +-- The non-trivial cell (c⊑s, keep≤keep) |
| 164 | +-- |
| 165 | +-- The single non-trivial cell of N5. Both sides reduce to |
| 166 | +-- `client-to-server e`. The load-bearing transport is the pure |
| 167 | +-- choreographic step `client-to-server`; the grade axis contributes |
| 168 | +-- only the identity step `keep≤keep`, which does not enter the |
| 169 | +-- reduction. There is no grade-only factor available to pair with a |
| 170 | +-- pure-choreo factor — the identity grade step provides nothing to |
| 171 | +-- factor out. |
| 172 | +------------------------------------------------------------------------ |
| 173 | + |
| 174 | +non-trivial-cell-equation : |
| 175 | + (e : RoleGEcho Client keep) → |
| 176 | + applyGrade keep≤keep (applyRole c⊑s e) |
| 177 | + ≡ applyRole c⊑s (applyGrade keep≤keep e) |
| 178 | +non-trivial-cell-equation e = refl |
| 179 | + |
| 180 | +-- Both sides reduce to `client-to-server e`. |
| 181 | +non-trivial-cell-LHS-reduces : |
| 182 | + (e : RoleGEcho Client keep) → |
| 183 | + applyGrade keep≤keep (applyRole c⊑s e) ≡ client-to-server e |
| 184 | +non-trivial-cell-LHS-reduces e = refl |
| 185 | + |
| 186 | +non-trivial-cell-RHS-reduces : |
| 187 | + (e : RoleGEcho Client keep) → |
| 188 | + applyRole c⊑s (applyGrade keep≤keep e) ≡ client-to-server e |
| 189 | +non-trivial-cell-RHS-reduces e = refl |
| 190 | + |
| 191 | +-- Joint witness: both sides equal `client-to-server e`, exhibiting |
| 192 | +-- explicitly that the load-bearing transport in this cell is pure |
| 193 | +-- choreographic. There is no companion pure-grade factor; the grade |
| 194 | +-- step `keep≤keep` is identity and contributes nothing. |
| 195 | +non-trivial-cell-pure-choreo : |
| 196 | + (e : RoleGEcho Client keep) → |
| 197 | + (applyGrade keep≤keep (applyRole c⊑s e) ≡ client-to-server e) |
| 198 | + × (applyRole c⊑s (applyGrade keep≤keep e) ≡ client-to-server e) |
| 199 | +non-trivial-cell-pure-choreo e = |
| 200 | + non-trivial-cell-LHS-reduces e , non-trivial-cell-RHS-reduces e |
| 201 | + |
| 202 | +------------------------------------------------------------------------ |
| 203 | +-- Closing |
| 204 | +-- |
| 205 | +-- The N5 candidate survives the sharpened falsifier. Recommended |
| 206 | +-- action: amend `roadmap-gates.adoc` to add |
| 207 | +-- `RoleGraded.choreo-grade-commute` as the fifth gate-2 nominee N5, |
| 208 | +-- with this file linked from the gate-2 audit doc surface as the |
| 209 | +-- falsifier-attempt record. |
| 210 | +-- |
| 211 | +-- Per the set-2 task spec, this file deliberately modifies nothing |
| 212 | +-- existing. Registering N5Falsifier in `proofs/agda/All.agda` (so the |
| 213 | +-- verified suite covers it, per project convention) is the |
| 214 | +-- integrator's call. |
| 215 | +------------------------------------------------------------------------ |
0 commit comments