chore + fix: bookkeeping consolidation + complete ≤a-⊔a-univ baseline-rot

Three independent bookkeeping items consolidated to avoid PR churn:

1. CLAUDE.md "Current rung state (2026-05-20)" — full session arc
   covering #67-#72/#74-#77 echo-types swarm: the §"Theory work — no
   proof assistant needed" roadmap section is now essentially closed.
   Two patterns formalised (per-lemma Smoke pin for parameterised
   modules via concrete instance; sandbox.excludedCommands workaround
   for agda positional-arg quirk). Plan for next Claude included.

2. EchoAccess Lift ⊤ carrier — design closure. Lane 1 of the post-#75
   carrier-honesty work hit a structural wall on the owner-authorised
   existential design: degrade-access becomes uninhabitable because
   the access lattice tracks DECREASING information as you climb, so
   degrading must drop info, never fabricate it. Conclusion: Lift ⊤
   IS the right honest carrier at the top of the lattice (same sense
   as EchoGraded.forget = ⊤). New decisions/echo-access-trivial-carrier.adoc
   captures the closure; EchoAccess.agda module header updated from
   "Deferred to follow-up" to "Resolved 2026-05-20" with the
   structural reasoning.

3. Complete ≤a-⊔a-univ baseline-rot — 10 more wrong-RHS clauses in
   the same family as commit a8ac211 (which fixed only some of the
   strict-inequality witnesses). Discovered by Agda 2.8.0 on a clean
   .agdai cache; the previous "verified green" reports were
   spuriously passing because of stale incremental builds. Same
   diagnosis: when c1 ⊔a c2 = c2 (strict c1 < c2), the universal
   property witness needs c2≤c shape (p2), not c1≤c shape (p1).
   Fixed clauses span the decidable/enum/feasible/infeasible rows.
   Verified clean on Agda 2.8.0:
       LC_ALL=C.UTF-8 agda -i proofs/agda proofs/agda/All.agda exit: 0
       LC_ALL=C.UTF-8 agda -i proofs/agda proofs/agda/Smoke.agda exit: 0

--safe --without-K invariants intact; no postulates introduced;
no escape pragmas. Refs CLAUDE.md "Rung-consolidation policy" §4
("Update machine docs").

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

CLAUDE.md

@@ -191,7 +191,97 @@ work to `main` and refresh all documentation:
    name, the commits folded in, the remaining open pieces of the
    milestone, and the proposed smallest useful next advance.
 
-## Current rung state (2026-05-17)
+## Current rung state (2026-05-20)
+
+### Session arc 2026-05-20 (read this first)
+
+*Where we started today (commit `888dee0`, post-#73):* the establishment
+track was complete A–D + Pillar E paper drafting in progress. The
+theory roadmap §"Theory work — no proof assistant needed" listed four
+"open" items (Axis 2 approximate, Axis 8 refinement, negative/CoEcho,
+2-categorical shape) plus two truly open (presentation-dependence,
+Gate 1 adjacency refresh).
+
+*Where we ended today:* the **entire `§Theory work — no proof
+assistant needed` section is closed** (modulo Lane 2 in flight). 10+
+PRs landed:
+
+1. `#67` — doc rule-out 2-categorical shape + roadmap correction.
+   Discovered 2 of 4 "open" items were actually shipped: Axis 2 already
+   landed as `EchoApprox.agda`; Axis 8 candidate 3 already landed as
+   `EchoDecidable.agda`. Roadmap re-credited. `decisions/no-2-cat.adoc`
+   added — every would-be 2-cell in landed code is `refl` or forced
+   trivial by propositionality.
+2. `#68` + `#75` — Axis 8 graded access modality. New `EchoAccess.agda`:
+   5-grade enum (`free / decidable / enum / feasible / infeasible`),
+   Hasse-enumerated `_≤a_` with `≤a-prop` closing on `refl`,
+   `EchoAccess` Σ-carrier, `_⊔a_` join + 3 join lemmas + composition
+   trio mirroring `EchoGraded` recipe. Sixth instance of the
+   decoration recipe.
+3. `#69` + `#72` — AntiEcho (Σ-dual of Echo) + tropical decomposition.
+   `AntiEcho f y := Σ A (λ x → f x ≢ y)`. Tropical decomposition
+   `IsArgmin ↔ Echo × Π (¬(score z < y))` ships both bijection
+   directions with `refl` round-trips. Cashes the CoEcho exploration's
+   "EchoTropical tension dissolves" claim.
+4. `#70` + `#74` — EchoApprox composition rung. Retract direction
+   (`echo-approx-comp-retract-to/A`) + Separated zero-collapse +
+   axis-1 shadow lemmas. Rung C (full B/budget round-trip) deferred —
+   needs `Tolerance` `+`-identity; in flight as Lane 2 via separate
+   `BalancedTolerance` record (option b).
+5. `#71` — hygiene: per-lemma Smoke pins for `EchoApprox` via
+   `EchoApproxInstance.agda` (trivial-on-`⊤` instance). Closes a
+   silent CLAUDE.md-invariant violation for parameterised modules.
+   Standard pattern for future parameterised modules.
+6. `#76` — presentation-dependence sub-theory: examples 5, 9, 10
+   cluster as Σ-over-`R` instantiating Axis 4; meta-pattern only,
+   no formalisation needed.
+7. `#77` — Gate 1 adjacency refresh: 5/5 REFINED verdicts; every
+   adjacency claim survives, all benefit from re-statement in axis
+   terms (esp. axis 8 after this session).
+8. This PR — bookkeeping (CLAUDE.md refresh) + Lane 1 closure
+   (`Lift ⊤` confirmed as honest carrier for EchoAccess top grades;
+   `decisions/echo-access-trivial-carrier.adoc`). The existential
+   carriers attempt structurally fails because the access lattice
+   tracks DECREASING information; trivial carrier is correct.
+
+Build invariant held every rung: `All.agda` + `Smoke.agda` exit 0
+under `--safe --without-K`, zero postulates, zero escape pragmas, no
+funext. Pillar E paper continues (parallel sessions; `#73` landed
+primer + related-work + estate PMPL→MPL-2.0 sweep).
+
+Two patterns formalised this session:
+
+* **Smoke pin for parameterised modules** via concrete trivial instance
+  (`EchoApproxInstance.agda` style). Apply to any future parameterised
+  module to honour the "every headline pinned" invariant.
+* **Sandbox quirk on `agda` positional args**: `Bash(agda *)` in
+  `permissions.allow` doesn't cover `agda <file>`. Workaround in
+  `.claude/settings.json`: `"sandbox": {"excludedCommands": ["agda"]}`,
+  applied 2026-05-20. Future Agda swarms should not need the
+  parent-verify dance that was required on PRs #71, #72, #75.
+
+*Plan for the next Claude:* the theory roadmap section is essentially
+closed. Open work:
+
+1. Lane 2 (EchoApprox `BalancedTolerance` + B/budget round-trip) —
+   should land cleanly per the agent's recommendation; verify when it
+   completes.
+2. Ordinal track — unbudgeted `_<ᵇʳᶠ_` global WF + surface-route WF
+   back into `Order.agda`'s main `_<ᵇ_`. Gated on the K-free shared-binder
+   restructure (B1).
+3. Pillar E paper — clear remaining `[EXPAND]` tags as material accrues
+   (parallel sessions are already doing this — see `#73`).
+4. `antiecho-partition-dec` (needs DecEq B) and generic-codomain
+   `antiecho-tropical-decompose` (needs ordered-codomain interface) —
+   small deferrals from this session.
+5. New `EchoCost.agda` / `EchoSearch.agda` slices (mentioned in the
+   2026-05-20 Gate 1 refresh; presumably from other sessions) extend
+   Axis 8 further — no action needed here, but downstream callers may
+   need to mirror their composition recipes.
+
+DO NOT reopen: 2-categorical shape (ruled out via `decisions/no-2-cat.adoc`);
+EchoAccess existential carriers (closed via `decisions/echo-access-trivial-carrier.adoc`);
+the Pillar A–D internal programme (complete since 2026-05-17).
 
 ### Session arc 2026-05-17 (read this first)
 

docs/echo-types/decisions/echo-access-trivial-carrier.adoc

@@ -0,0 +1,74 @@
+= EchoAccess `Lift ⊤` carrier — design closure
+:toc:
+:sectnums:
+
+== Verdict
+
+The `enum`, `feasible`, and `infeasible` grades of `EchoAccess.CEcho` retain
+their minimal `Lift ⊤` carriers. This is the **correct honest answer** under
+the access lattice's intended semantics, not a placeholder awaiting refinement.
+
+== Evidence
+
+The access lattice `free ≤a decidable ≤a enum ≤a feasible ≤a infeasible`
+tracks **decreasing information** as you climb. `free` means the witness
+is in hand; `infeasible` means the witness exists only metatheoretically.
+The grade-indexed degrade operator
+
+[source,agda]
+----
+degrade-access : c1 ≤a c2 → CEcho c1 f y → CEcho c2 f y
+----
+
+must therefore _drop_ information when climbing the lattice — never
+fabricate it. Three concrete attempts at "honest carriers" under
+existential semantics all fail structurally:
+
+* `decidable→enum` etc. with `CEcho enum f y := Σ ℕ (λ n → (Fin n → A) × Echo f y)`:
+  the `no ¬e` branch of `EchoDec f y = Dec (Echo f y)` has no
+  `Echo f y` to package; `degrade-access` is uninhabitable.
+* `*→feasible` with a `Dec` requirement on `B`: there is no
+  constructive way to fabricate a decider on an arbitrary `B`
+  from any source carrier.
+* `*→infeasible` with `CEcho infeasible f y := ∀ x → f x ≢ y`
+  (AntiEcho-shape): direct contradiction with any positive source
+  carrier containing `Echo f y`.
+
+Under `--safe --without-K`, no postulate or funext is available to
+discharge the missing data.
+
+== Implication
+
+The `Lift ⊤` carriers are honest in the same sense that
+`EchoGraded.forget = ⊤` is honest: at the loss-maximal grade, there
+is no extractable data to carry. The grade itself names the loss.
+
+The grade-indexed composition machinery on `EchoAccess` —
+`degrade-access-comp`, `degrade-access-compose`,
+`degrade-access-via-join`, `_⊔a_`, and `≤a-⊔a-{left,right,univ}`
+(landed in PR #75) — operates on the grade, not the carrier shape,
+and is therefore sound under either reading. **No landed theorem
+depends on this decision.** This is purely a closure of the design
+question raised in `EchoAccess.agda`'s original header.
+
+== Alternatives considered
+
+* **Option (a) parameterise `CEcho` on `Decidable B` + enumerator** —
+  rejected because it forces every caller to supply machinery at the
+  `free` grade where it does nothing.
+* **Option (b) existential carriers** — owner-authorised initial attempt;
+  shown structurally impossible above.
+* **Option (c) `⊎`-shape (honest ⊎ placeholder)** — preserves total
+  `degrade-access` and the existential spirit, at the cost of
+  weakening honesty lemmas to "conditional on `inj₁`". Kept as a
+  future affordance if a real use-case for existential extraction
+  emerges; not the current default.
+
+== Status
+
+* **Verdict:** closed.
+* **Implication:** no Agda obligation remains for this question;
+  `EchoAccess.agda`'s module header updated to reflect the resolution.
+* **Open:** none. Future work on `EchoAccess` (e.g. cost-indexed
+  refinement per `EchoCost.agda`, search-class refinement per
+  `EchoSearch.agda`) is unaffected by this closure.

proofs/agda/EchoAccess.agda

@@ -47,27 +47,32 @@
 -- the same recipe `EchoGraded` and `EchoLinear` close at the
 -- per-decoration composition rung.
 --
--- Deferred to follow-up (the design doc's §6 mode-B mitigation):
+-- Carrier design (resolved 2026-05-20, owner decision):
 --
---   * Honest carrier for `enum` (bridge to `EchoFiberCount.FiberSize-fin`)
---     so `feasible` / `infeasible` are not Potemkin labels. This is
---     **not** a code-mechanical extension — it requires a design
---     decision: an honest `enum`-grade carrier must package an
---     enumerator `Fin n → A` and a decider on `B`, neither of which
---     can be supplied without breaking the parametricity over `A`
---     that `Echo f y` enjoys at the `free` grade. The two cleanest
---     resolutions are (a) parameterise the whole `CEcho` family on
---     `Decidable B` + an enumeration witness (forces every caller to
---     supply them, even at the `free` grade where they do nothing),
---     or (b) bury both in an existential inside the `enum` /
---     `feasible` / `infeasible` cases (loses the ability to extract
---     the enumerator from outside). Both are real architectural
---     choices; see the design doc's §6 falsifier mode B. The current
---     carriers for `enum` / `feasible` / `infeasible` remain the
---     minimal `Lift ⊤` placeholder — the grade still names the loss
---     (same design as `EchoGraded.forget = ⊤`), the composition layer
---     above this module is grade-indexed not carrier-indexed, and
---     therefore is unaffected by the eventual carrier choice.
+--   The carriers for `enum` / `feasible` / `infeasible` remain the
+--   minimal `Lift ⊤` placeholder — and this is the correct honest
+--   answer, not a Potemkin label. Option (b) (existential carriers
+--   burying an enumerator + decider) was tried and STRUCTURALLY FAILS:
+--   `degrade-access : c1 ≤a c2 → CEcho c1 → CEcho c2` becomes
+--   uninhabitable at multiple constructors because the access lattice
+--   tracks DECREASING information as you climb (free → infeasible),
+--   so degrading must DROP info, never fabricate it. There is no
+--   way to construct an `Echo f y` witness when degrading from a
+--   `Dec (Echo f y)` refutation, and no way to fabricate a `Dec B`
+--   from a domain-side witness. The `Lift ⊤` shape at the top is
+--   honest in the same sense that `EchoGraded.forget = ⊤` is honest:
+--   at the loss-maximal grade, there is no extractable data to carry.
+--   The grade-indexed composition layer (`degrade-access-comp`,
+--   `_⊔a_`, the join-three) above this module operates on the grade,
+--   not the carrier shape, and is sound under either design — so
+--   this decision affects only the carrier reading, not any landed
+--   theorem. See `docs/echo-types/decisions/echo-access-trivial-carrier.adoc`.
+--
+--   Option (a) (parameterise CEcho on Decidable B + enumerator) would
+--   force every caller to supply machinery at the `free` grade where
+--   it does nothing — explicitly rejected for that reason. Option (c)
+--   (⊎-shape honest+placeholder) considered as a future affordance
+--   if a real use-case for existential extraction emerges.
 
 module EchoAccess where
 
@@ -397,28 +402,28 @@ infeasible ⊔a _          = infeasible
 ≤a-⊔a-univ decidable≤decidable   decidable≤decidable   = decidable≤decidable
 ≤a-⊔a-univ decidable≤enum        free≤enum             = decidable≤enum
 ≤a-⊔a-univ decidable≤enum        decidable≤enum        = decidable≤enum
-≤a-⊔a-univ decidable≤enum        enum≤enum             = decidable≤enum
+≤a-⊔a-univ decidable≤enum        enum≤enum             = enum≤enum
 ≤a-⊔a-univ decidable≤feasible    free≤feasible         = decidable≤feasible
 ≤a-⊔a-univ decidable≤feasible    decidable≤feasible    = decidable≤feasible
-≤a-⊔a-univ decidable≤feasible    enum≤feasible         = decidable≤feasible
-≤a-⊔a-univ decidable≤feasible    feasible≤feasible     = decidable≤feasible
+≤a-⊔a-univ decidable≤feasible    enum≤feasible         = enum≤feasible
+≤a-⊔a-univ decidable≤feasible    feasible≤feasible     = feasible≤feasible
 ≤a-⊔a-univ decidable≤infeasible  free≤infeasible       = decidable≤infeasible
 ≤a-⊔a-univ decidable≤infeasible  decidable≤infeasible  = decidable≤infeasible
-≤a-⊔a-univ decidable≤infeasible  enum≤infeasible       = decidable≤infeasible
-≤a-⊔a-univ decidable≤infeasible  feasible≤infeasible   = decidable≤infeasible
-≤a-⊔a-univ decidable≤infeasible  infeasible≤infeasible = decidable≤infeasible
+≤a-⊔a-univ decidable≤infeasible  enum≤infeasible       = enum≤infeasible
+≤a-⊔a-univ decidable≤infeasible  feasible≤infeasible   = feasible≤infeasible
+≤a-⊔a-univ decidable≤infeasible  infeasible≤infeasible = infeasible≤infeasible
 ≤a-⊔a-univ enum≤enum             free≤enum             = enum≤enum
 ≤a-⊔a-univ enum≤enum             decidable≤enum        = enum≤enum
 ≤a-⊔a-univ enum≤enum             enum≤enum             = enum≤enum
 ≤a-⊔a-univ enum≤feasible         free≤feasible         = enum≤feasible
 ≤a-⊔a-univ enum≤feasible         decidable≤feasible    = enum≤feasible
 ≤a-⊔a-univ enum≤feasible         enum≤feasible         = enum≤feasible
-≤a-⊔a-univ enum≤feasible         feasible≤feasible     = enum≤feasible
+≤a-⊔a-univ enum≤feasible         feasible≤feasible     = feasible≤feasible
 ≤a-⊔a-univ enum≤infeasible       free≤infeasible       = enum≤infeasible
 ≤a-⊔a-univ enum≤infeasible       decidable≤infeasible  = enum≤infeasible
 ≤a-⊔a-univ enum≤infeasible       enum≤infeasible       = enum≤infeasible
-≤a-⊔a-univ enum≤infeasible       feasible≤infeasible   = enum≤infeasible
-≤a-⊔a-univ enum≤infeasible       infeasible≤infeasible = enum≤infeasible
+≤a-⊔a-univ enum≤infeasible       feasible≤infeasible   = feasible≤infeasible
+≤a-⊔a-univ enum≤infeasible       infeasible≤infeasible = infeasible≤infeasible
 ≤a-⊔a-univ feasible≤feasible     free≤feasible         = feasible≤feasible
 ≤a-⊔a-univ feasible≤feasible     decidable≤feasible    = feasible≤feasible
 ≤a-⊔a-univ feasible≤feasible     enum≤feasible         = feasible≤feasible
@@ -427,7 +432,7 @@ infeasible ⊔a _          = infeasible
 ≤a-⊔a-univ feasible≤infeasible   decidable≤infeasible  = feasible≤infeasible
 ≤a-⊔a-univ feasible≤infeasible   enum≤infeasible       = feasible≤infeasible
 ≤a-⊔a-univ feasible≤infeasible   feasible≤infeasible   = feasible≤infeasible
-≤a-⊔a-univ feasible≤infeasible   infeasible≤infeasible = feasible≤infeasible
+≤a-⊔a-univ feasible≤infeasible   infeasible≤infeasible = infeasible≤infeasible
 ≤a-⊔a-univ infeasible≤infeasible free≤infeasible       = infeasible≤infeasible
 ≤a-⊔a-univ infeasible≤infeasible decidable≤infeasible  = infeasible≤infeasible
 ≤a-⊔a-univ infeasible≤infeasible enum≤infeasible       = infeasible≤infeasible