This file is the artefact the README and roadmap-gates.adoc require for
Gate 2 of the identity claim. It audits the nominees against the gate’s
falsifier — "naturally echo-shaped, not reducible to generic sigma/fiber
lemmas" — and reports the threshold outcome.
This is Revision 5 (2026-05-26). It is the close-out re-audit
required by roadmap.adoc §Lane 2: it re-checks that the
Revision-4 nominee table still clears the comfortable threshold
(≥ 3 of 4 surviving) under everything that has landed in this
lane since then. Verdict: still 4/4 surviving; comfortable
threshold met by margin of one. The Revision-5 substance is in
§Revision-5 re-audit (2026-05-26); the per-nominee
audits below are unchanged from Revision 4. See §Revision
notes for the full diff.
- 1. Inherited spec
- 2. The nominee list (current)
- 3. Audit of N1:
EchoGraded.degrade-via-join - 4. Audit of N2:
EchoGraded.degrade-compose - 5. Audit of N3:
EchoChoreo.applyChoreo-compose - 6. Audit of N4:
EchoLinear.degradeMode-compose - 7. Threshold check
- 8. New construction:
characteristic.RoleGraded(closes handoff Observation E) - 9. Withdrawn nominees (historical record)
- 10. Honest qualifications
- 11. Open work and recommendations
- 12. Revision notes (what changed across audit revisions)
- 13. Revision-5 re-audit (2026-05-26)
- 14. Cross-lane observations
- 15. Pointers
|
Note
|
The artefact path named in |
For the sceptic-facing evidence map ("is this just renamed Σ?",
organised under five demands and cross-linked to every in-tree
artefact), see docs/echo-types/sigma-distinctness-map.adoc and its
internal companion core/skepticisms/is-this-just-sigma-types.md.
That doc is an evidence index; this file is the per-nominee Gate 2
audit and remains the authoritative gate artefact.
roadmap-gates.adoc Gate 2:
There exist theorems whose statements are naturally echo-shaped and are not reducible to generic sigma/fiber lemmas.
For each nominated theorem, answer in writing:
Would this theorem be stated, or stated in this form, without the echo framing?
A theorem that survives only as "fiber lemma X with renamed components" does not count.
At least two of three nominees must survive. (The current revision
of roadmap-gates.adoc lists four nominees; the threshold scales
proportionally — a comfortable pass requires at least 3 of 4 to
survive, an honest minimum requires at least 2 of 4.)
Per the amended roadmap-gates.adoc Gate 2 table:
| Tag | Module / lemma | Claim |
|---|---|---|
N1 |
|
Categorical join law on the loss-grade lattice. |
N2 |
|
Compositional degradation along the grade lattice. |
N3 |
|
Compositional choreographic transport along the role-reachability lattice. |
N4 |
|
Compositional weakening along the linearity-mode lattice. |
The audit below treats each in turn. §Threshold check reports the gate outcome. §New construction documents the audit-derived module that closes the handoff’s Observation E.
degrade-via-join :
∀ {g1 g2 g}
(p1 : g1 ≤g g) (p2 : g2 ≤g g) (e : GEcho g1) →
degrade p1 e
≡ degrade (≤g-⊔g-univ p1 p2) (degrade (≤g-⊔g-left g1 g2) e)The lemma states a categorical join law on the loss-grade lattice:
degrading directly to a common upper bound g agrees with degrading
first to the join g1 ⊔g g2 and then onward via the universal arrow.
Substantive ingredients:
-
≤g-⊔g-left,≤g-⊔g-right,≤g-⊔g-univ— the join structure. These exhibit⊔gas the categorical join in≤g. -
≤g-prop— propositionality of the order. -
The
GEchofamily — different types per grade (Echo collapse ttat keep, residue certificate at residue,⊤at forget).
A naïve reduction: "this is a generic categorical join law on graded families." Correct in shape, lossy in content. The lemma is about the specific lattice modeling information loss.
Exhibit a non-loss-ordered three-element propositional join-semilattice where the same lemma is also load-bearing for a structurally unrelated reason. We currently have no such exhibition.
degrade-compose :
∀ {g1 g2 g3}
(p12 : g1 ≤g g2) (p23 : g2 ≤g g3) (p13 : g1 ≤g g3)
(e : GEcho g1) →
degrade p23 (degrade p12 e) ≡ degrade p13 eSame structural ingredients as N1: degrade-comp (associativity along
a chosen factoring) and ≤g-prop (propositionality of the order). The
lemma’s content: any factoring of a degradation through an intermediate
grade equals the direct degradation.
Same as for N1.
applyChoreo-compose :
∀ {r1 r2 r3 : Role}
(p12 : r1 ⊑c r2) (p23 : r2 ⊑c r3) (p13 : r1 ⊑c r3)
{y : Bool} (e : RoleEcho r1 y) →
applyChoreo p23 (applyChoreo p12 e) ≡ applyChoreo p13 eThe structurally-parallel theorem to N2, on the choreographic decoration. Substantive ingredients:
-
applyChoreo-comp— decomposition of choreographic transport. -
⊑c-prop— propositionality of the role-reachability order. -
RoleEcho r yisEcho (obs r) y— a family of echoes indexed by role, with each role giving a different observation function. -
The transport
applyChoreo c⊑s = client-to-serverfactors throughmap-squareover a role-changing commuting square (swap-square).
Two-stage falsifier:
-
Exhibit a non-choreographic two-element propositional reachability order where the same lemma is also load-bearing.
-
Exhibit a different commuting square (i.e. a different role embedding) under which the lemma fails.
We currently have no such exhibitions.
degradeMode-compose :
∀ {m1 m2 m3}
(p12 : m1 ≤m m2) (p23 : m2 ≤m m3) (p13 : m1 ≤m m3)
(e : LEcho m1) →
degradeMode p23 (degradeMode p12 e) ≡ degradeMode p13 eThe third instance of the same recipe, on the linearity-mode decoration. Substantive ingredients:
-
degradeMode-comp— associativity of mode weakening. -
≤m-prop— propositionality of the mode order. Two-element lattice (linear ≤m affine) with three constructors; same propositional structure as the role lattice and same general shape as the grade lattice. -
LEcho m— a family that varies type per mode:Echo collapse ttat linear,EchoR ⊤ TrivialCert ttat affine. Same per-decoration type variation asGEcho. -
The strict step
degradeMode linear≤affineisweaken, which factors throughcollapse-to-residuefromEchoResidue. This is specific content — the weakening is not the identity, and it has the irreversibility witnessno-section-collapse-to-residueattached.
A naïve reduction: "this is associativity of weakening in any
two-element propositional order." Correct in shape, lossy in content.
The lemma is about the specific propositional order on linearity
modes, with the strict weakening weaken having concrete
non-recoverability content.
Same two-stage falsifier as N3, with mode-lattice substituted for
role-lattice and weaken substituted for client-to-server:
-
Exhibit a non-linearity two-element propositional order where the same lemma is load-bearing for a structurally unrelated reason.
-
Exhibit a different choice of strict-step weakening under which the lemma fails — i.e. show the lemma depends on the specific
weakenand not on a generic two-element order action.
We currently have no such exhibitions. The lemma is the third
instance of the same recipe (custom propositional decoration order
echo-indexed family + transport action), confirming that the recipe
is not unique to a single decoration.
| Nominee | Module | Status | Reason |
|---|---|---|---|
N1 |
|
SURVIVES |
Categorical join law on the loss-grade lattice; not a fiber lemma. |
N2 |
|
SURVIVES |
Compositional degradation on the loss-grade lattice; not a fiber lemma. |
N3 |
|
SURVIVES |
Compositional transport on the role-reachability lattice; specific commuting-square content. |
N4 |
|
SURVIVES |
Compositional weakening on the linearity-mode lattice; specific irreversibility content. |
roadmap-gates.adoc threshold:
Gate 2 fails if fewer than two candidates survive.
Survivors: N1, N2, N3, N4. Count: 4. Threshold: ≥ 2. Met by margin of two.
Gate 2 passes — 4-of-4 surviving across three modules.
The Revision-3 handoff document recorded the following open recommendation in Observation E:
A genuine integration theorem — one in which a single Echo carries both a role/choreographic decoration and a graded decoration, and the two conjuncts share data — is not currently in the repository. Building one is open work.
This revision closes that recommendation.
proofs/agda/characteristic/RoleGraded.agda defines:
-
RoleGEcho : Role → Grade → Set— a 2D family that varies non-trivially in both axes. At keep grade,RoleGEcho r keep = RoleEcho r true; at residue and forget grades,⊤. -
applyRole : (r1 ⊑c r2) → RoleGEcho r1 g → RoleGEcho r2 g— role transport. At keep grade it does real work (client-to-serverforc⊑s); past keep, identity on⊤. -
applyGrade : (g1 ≤g g2) → RoleGEcho r g1 → RoleGEcho r g2— grade degradation, parametric in the role.
choreo-grade-commute :
∀ {r1 r2 g1 g2}
(rp : r1 ⊑c r2) (gp : g1 ≤g g2)
(e : RoleGEcho r1 g1) →
applyGrade gp (applyRole rp e) ≡ applyRole rp (applyGrade gp e)The two actions commute: applying them in either order on a
RoleGEcho yields the same result. Eighteen cases, each closing by
refl after pattern matching. The non-trivial case is
(c⊑s, keep≤keep) where both sides reduce to client-to-server e.
A combined two-decoration action applyBoth is also provided, with
its agreement under either factoring proved as a corollary.
| Test | Verdict |
|---|---|
1. Single 2D family on which both decorations act. |
Pass: |
2. Single combined action consuming both decoration witnesses. |
Pass: |
3. Same-data test: both sides of the conclusion mention both decoration witnesses. |
Pass: both |
The withdrawn knowledge-and-controlled-degradation nominee failed
test 3 (its conjuncts were over different functions and shared no
data). choreo-grade-commute passes all three.
The three Observation-E tests are protocol tests: they ask whether
the construction has the right shape (single 2D family, single
combined action, same-data conclusion). RoleGraded passes by
construction.
What the protocol tests do not ask: how much of the 2D family’s
content is non-trivial. Of choreo-grade-commute’s 18 cases (3
role constructors × 6 grade constructors), exactly one carries
non-trivial cross-decoration content ((c⊑s, keep≤keep), reducing
to `client-to-server e). The other 17 close trivially because
residue/forget grades collapse RoleGEcho to ⊤ (12 cases) or
because the role-reachability constructors are reflexive (5 cases).
The 2D family is asymmetric — the role parameter is only live at
keep grade.
This is a protocol-correct closure of EI-1. It is substantively
narrow. The follow-up question — is the recipe robust across
other 2D combinations (Role × Mode, Mode × Grade, etc.), or did
RoleGraded benefit from a fortunate axis pair? — is tracked as
EI-2 in docs/next-questions.adoc. EI-2 is a sharpening question,
not a survival question; its negative resolution would weaken
EI-1’s closure to "closed-but-narrow" but would not invalidate it.
Do not relabel EI-1 as open. The protocol pass is the protocol pass. EI-2 records what’s still substantively open without moving the goalposts.
choreo-grade-commute is a candidate fifth Gate 2 nominee. Its
audit, were it nominated:
Exhibit a 2D propositional family with two independent actions where
the same commutation holds for structurally unrelated reasons. The
candidate falsifier is: any 2D family where one or both decorations
collapse to a degenerate type (here, ⊤ at residue/forget) admits a
trivial commutation. The non-trivial commutation case is at
(c⊑s, keep≤keep), where both sides reduce to client-to-server e
— this is not trivial; it depends on the specific role-action
content of client-to-server.
A complete falsifier would need to exhibit a non-echo construction where the keep-grade row of the 2D family carries a non-trivial role action under which the commutation also holds. We do not currently have such a construction.
Verdict (if nominated): SURVIVES.
The lemma is not currently in roadmap-gates.adoc Gate 2’s nominee
table. Whether to add it is a separate decision; this audit flags it
as a candidate without recommending the amendment. Adding it would
push the audit count to 5-of-5 surviving across four constructions
(EchoGraded, EchoChoreo, EchoLinear, characteristic.RoleGraded).
Two nominees in earlier roadmap revisions did not survive. The audits are retained here for the historical record; the lemmas remain in their original modules for whatever value they carry.
visible : State → Bool -- State = Bool × Bool
visible = proj₁
visible-constraint :
∀ {y : Bool} (e : Echo visible y) → proj₁ (proj₁ e) ≡ y
visible-constraint (_ , p) = pvisible := proj₁ definitionally, so Echo visible y is
Σ State (λ s → proj₁ s ≡ y). The standard proj₂ on this Σ has the
same type as visible-constraint, and both compute by refl on every
inhabitant. The reduction visible-constraint ≡ proj₂ is formalised
in proofs/agda/characteristic/VisibleConstraintAudit.agda.
Per the Gate 2 test, "fiber lemma X with renamed components does not
count." visible-constraint is proj₂ with renamed components.
knowledge-and-controlled-degradation :
∀ {y : Bool} {P : Global → Set} →
(∀ g → P g → P (scramble-server g)) →
Knows Client P y →
(∀ e → P (proj₁ (client-stability e)))
× (degrade keep≤residue echo-true ≡ degrade keep≤residue echo-false)The two conjuncts are over different functions: conjunct 1 over
obs Client : Global → Bool; conjunct 2 over collapse : Bool → ⊤.
The proof closes by literally pairing the two facts. The hypotheses
flow only into conjunct 1.
The formal exhibit is in
proofs/agda/characteristic/IntegrationAudit.agda:
-
split-knowledge,split-merging— the two conjuncts in isolation. -
N3-is-product : knowledge-and-controlled-degradation inv k ≡ (split-knowledge inv k , split-merging), byrefl. -
split-merging-uses-no-hypotheses— confirming no shared data.
The "integration" is × with no logical link. The named theorem
does not integrate; it pairs.
The theorem stands as a true proposition. It marks the slot where a
genuine integration theorem would live. As of Revision 4, that slot
is filled by characteristic.RoleGraded.choreo-grade-commute; the
withdrawn lemma can be left in place as a historical signpost.
-
The pass is 4-of-4, distributed across three modules (EchoGraded carries N1 and N2; EchoChoreo carries N3; EchoLinear carries N4). This is a comfortable pass; the threshold of 2 surviving is met by margin of two.
-
All four survivors are instances of the same recipe: a custom propositional decoration order, an echo-indexed family that varies per decoration, an action transporting echoes along the order. If Gate 1 finds that this recipe is not echo-specific (e.g. found in plain refinement-type theory or any propositionally-ordered graded action setting), all four would weaken in parallel.
-
Each survivor has at least one unattempted concrete falsifier (§§3.2, §§4.2, §§5.2, §§6.2). The pass is conditional on those falsifiers being attempted and not succeeding.
-
The new construction
characteristic.RoleGradedexhibits a fourth decoration combination (Role × Grade), demonstrating the recipe extends to 2D products. Its headline theoremchoreo-grade-commuteis not currently nominated; its addition as a fifth nominee would push the audit count to 5-of-5 across four constructions.
-
Try the falsifiers. Each survivor has an unattempted falsifier. Attempting them would either harden the pass or expose hidden generality.
-
Consider nominating
characteristic.RoleGraded.choreo-grade-commute. The construction closes Observation E and provides a concrete exhibit of cross-decoration integration that the withdrawn N3 was trying but failing to provide. -
Consider further decorations. The recipe extends to additional axes (e.g., epistemic level, indexed step, tropical valuation — see
EchoEpistemic,EchoIndexed,EchoTropical). Each gives an analogous composition law. Diminishing returns set in past three or four examples; the family does not need padding.
| Revision | Substance |
|---|---|
1 |
Original audit. 3 nominees: |
2 |
Sharpened the N3 falsifier; N3 retracted. Withdrew N1; replaced with |
3 |
Amendment to |
4 |
Added |
5 (2026-05-26) |
Close-out re-audit per |
5b (2026-05-27) |
Within-Rev-5 follow-up: |
This section is the close-out audit named in roadmap.adoc §Lane 2
close-out criterion (3). It re-checks the Revision-4 nominee table
against everything that has landed in the characteristic / Gate-2
lane since Revision 4. Three categories of evidence were considered;
none weakens the Revision-4 verdict.
roadmap.adoc §Lane 2 distinguishes two thresholds (taken from
roadmap-gates.adoc Gate 2): the honest minimum (≥ 2 of 4
surviving) and the comfortable threshold (≥ 3 of 4 surviving).
Revision 4 reported 4/4. Lane 2 close-out asks: under everything
this lane has produced since, does that still hold by the
comfortable bar?
-
EI-2 terminated — negative verdict, PATH B (
docs/EI2_REPORT.adoc, authoritative). Eight investigation phases, seven data points (sibling 2D constructionscharacteristic.RoleMode,characteristic.ModeGraded, 3Dcharacteristic.RoleModeGradewith three pairwise commutations + a triple, self-pairingcharacteristic.RoleRole), plus the formal exhibitcharacteristic.ChoreoInjectivefor the non-loss-only criterion and the partial genericcharacteristic.RecipeTheorem. The termination finding is that the integration recipe with the existing five named axes does not carry substantive simultaneous cross-axis content — every "non-trivial" cell carries one-axis-at- a-time content. The five doc locations enumerated in EI2_REPORT §"Documentation cascade" have all been updated accordingly. -
Q2.1 /
characteristic.NonTruncatable. The general statement ofecho-not-propfor(f, y)with two distinct preimages is re-exported under the Q2.1 name; the received-yform is PARTIALLY REDUCIBLE per the module’s own Gate-2 falsifier audit (proof factors through generic Σ; echo-specific content is in the statement only). The constructed-yform, which buildsyfrom bare non-injectivity, carries echo-specific content but is not on the Revision-4 nominee table — it is closer to a Gate-3 example obligation than a Gate-2 nominee. -
characteristic.N5Falsifier— RESOLVED 2026-05-27, NOW GREEN AND IN CI CLOSURE. Originally KNOWN BROKEN, deliberately excluded (UnsolvedConstraints+UnsolvedMetaVariables). The Lane-2 N5-sharpening pass on 2026-05-27 closed the unsolved metas by making the implicitr1/r2/gparameters ofapplyRole/applyGradeexplicit at the four call sites; the obstacle was inference, not content (Agda cannot recover the role fromRoleGEcho r keep = Echo (obs r) truebecauseobsis not injective, but supplying the role explicitly resolves it). The module is now imported incharacteristic/All.agdaand the broken-banner has been updated with the resolution record. Crucially: the resolution does not change the Rev-4 conclusion about candidate N5 — the only non-trivial cell is still the(c⊑s, keep≤keep)Choreo content already credited to N3, so adoption would still be cosmetic. The cleaned-up green falsifier exhibit does tighten the audit story (the SURVIVES verdict is now mechanised instead of being a not-mechanised attempt-of-record) without changing the N5-not-adopted decision.
| Nominee | Module | Status as of Rev 5 | Reason |
|---|---|---|---|
N1 |
|
SURVIVES (unchanged from Rev 4) |
The lemma is on the loss-grade lattice’s join, not on any integration claim. EI-2 termination does not touch it. No falsifier attempted since Rev 4. |
N2 |
|
SURVIVES (unchanged from Rev 4) |
As N1: single-decoration lemma; EI-2 termination is orthogonal. No falsifier attempted since Rev 4. |
N3 |
|
SURVIVES (unchanged from Rev 4) |
Single-decoration role-reachability lemma; the |
N4 |
|
SURVIVES (unchanged from Rev 4) |
Single-decoration mode lemma with the specific |
Survivors: N1, N2, N3, N4. Count: 4. Honest threshold (≥ 2): met.
Comfortable threshold (≥ 3): met by margin of one. The Lane 2
close-out criterion in roadmap.adoc is satisfied.
-
Does not nominate N5. The candidate fifth nominee (
characteristic.RoleGraded.choreo-grade-commute) remains a candidate. EI-2’s termination shows the protocol-pass-but-narrow reading from Rev 4 was correct: the only non-trivial cell of the 2D family’s commutation is(c⊑s, keep≤keep), reducing toclient-to-server e— the same Choreo content N3 already carries. Nominating it would push the count to 5/5, but the marginal evidence is the sameclient-to-servercontent already credited to N3, so nominating it would be cosmetic. Left unadopted on the same logic as Rev 4. -
Does not retroactively retract any Rev-4 verdict. No nominee’s falsifier was attempted and failed; the absence of attempts is carried forward as a Rev-4 honest qualification (§Honest qualifications item 3), not a Rev-5 finding.
-
Does not promote
characteristic.NonTruncatable.Q2-1to the nominee table. Its own broken-Gate-2 audit (PARTIALLY REDUCIBLE) was applied honestly; the lemma remains useful as a Gate-3 signpost, not as a Gate-2 survivor.
-
proofs/agda/characteristic/RoleMode.agda,RoleModeGrade.agda,RoleRole.agda,ModeGraded.agda,ChoreoInjective.agda,RecipeNonTriviality.agda,RecipeSpec.agda,RecipeTheorem.agda,InteractionTest.agda— EI-2 investigation lane. Not Gate-2 nominees; supply the EI-2-termination evidence the §"Evidence reviewed" item 1 cites. -
proofs/agda/characteristic/NonTruncatable.agda— Q2.1, see §"Evidence reviewed" item 2. -
proofs/agda/characteristic/N5Falsifier.agda— KNOWN BROKEN, NOT IN CI CLOSURE; see §"Evidence reviewed" item 3. -
docs/EI2_REPORT.adoc— authoritative EI-2 verdict. -
proofs/agda/characteristic/All.agda— the lane-local CI seam.
-
The current nominees:
-
proofs/agda/EchoGraded.agda—degrade-via-join(N1),degrade-compose(N2), supporting≤g-prop,≤g-⊔g-univ,≤g-⊔g-left,degrade-comp,GEcho. -
proofs/agda/EchoChoreo.agda—applyChoreo-compose(N3), supporting⊑c-prop,applyChoreo-comp,applyChoreo,RoleEcho,client-to-server,swap-square. -
proofs/agda/EchoLinear.agda—degradeMode-compose(N4), supporting≤m-prop,degradeMode-comp,weaken,LEcho.
-
-
The audit-derived new construction:
-
proofs/agda/characteristic/RoleGraded.agda—RoleGEcho,applyRole,applyGrade,choreo-grade-commute,applyBoth. Candidate N5 if amended into the roadmap.
-
-
Withdrawn nominees, retained for expository value in their original modules:
-
proofs/agda/EchoCharacteristic.agda(visible-constraint). -
proofs/agda/EchoIntegration.agda(knowledge-and-controlled-degradation).
-
-
Falsifier exhibits in this lane:
-
proofs/agda/characteristic/VisibleConstraintAudit.agda— formalises the reductionvisible-constraint ≡ proj₂. -
proofs/agda/characteristic/IntegrationAudit.agda— formalises thatknowledge-and-controlled-degradationis×of independent facts.
-
-
The gate spec:
roadmap-gates.adoc§Gate 2. -
The neighbouring frameworks (Gate 1’s territory):
docs/adjacency/.