From a2cc7a97ec91505fcc2050937271e4a34b816059 Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Wed, 20 May 2026 17:14:01 +0100 Subject: [PATCH] =?UTF-8?q?chore=20+=20fix:=20bookkeeping=20consolidation?= =?UTF-8?q?=20+=20complete=20=E2=89=A4a-=E2=8A=94a-univ=20baseline-rot?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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) --- CLAUDE.md | 92 ++++++++++++++++++- .../echo-access-trivial-carrier.adoc | 74 +++++++++++++++ proofs/agda/EchoAccess.agda | 65 +++++++------ 3 files changed, 200 insertions(+), 31 deletions(-) create mode 100644 docs/echo-types/decisions/echo-access-trivial-carrier.adoc diff --git a/CLAUDE.md b/CLAUDE.md index 3cbd725..de527c4 100644 --- a/CLAUDE.md +++ b/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 `. 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) diff --git a/docs/echo-types/decisions/echo-access-trivial-carrier.adoc b/docs/echo-types/decisions/echo-access-trivial-carrier.adoc new file mode 100644 index 0000000..88844a4 --- /dev/null +++ b/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. diff --git a/proofs/agda/EchoAccess.agda b/proofs/agda/EchoAccess.agda index f266c63..3b273fa 100644 --- a/proofs/agda/EchoAccess.agda +++ b/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