docs: consolidate budgeted-recursive-surface rung

claude · claude · commit c9f72b7e32d8 · 2026-04-23T21:37:48.000Z
Rung-consolidation pass per the policy added in CLAUDE.md. Main has now advanced past the Pentagon rung (cancel-iso + Echo-comp-iso-pent- {B, echo}, already merged via separate landings) into the **budgeted recursive-surface rung** — `RecursiveSurfaceBudget.agda` plus the surface/extended/iterated/Veblen layer modules that feed it. This commit does no code work; it brings the human docs (CLAUDE.md, composition.md, roadmap.md) into line with what is actually on main. Changes: CLAUDE.md Ordinal-track summary extended to name the new layer modules (Order.agda's 13-constructor admitted core; surface / extended / iterated / Veblen routes; RecursiveSurfaceBudget.agda's BudgetedBT + wf-<ᵇʳᶠᵇ + <ᵇʳᶠᵇ⇒lifted). Open pieces at this rung enumerated: shared-binder constructors, unbudgeted global `_<ᵇʳᶠ_` WF, pushback into Order.agda. Current-rung-state section refreshed. Still dated 2026-04-23 as a same-day consolidation. docs/echo-types/composition.md Q4 (associativity) moved from "conjecture" to "partially landed" with the two projection-pentagon lemmas called out explicitly. Compact statement item 4 marked (Partial). The "what to formalise next" ordering updated: pentagon struck through with pointer to the full Σ-associativity iso as the remaining piece. docs/echo-types/roadmap.md Formalisation list now includes the budgeted-recursive-surface rung as [partial] alongside the pentagon [partial] entry. Suggested immediate ordering gains a step 4 for unbudgeted `_<ᵇʳᶠ_` WF; subsequent steps renumbered. Verified: agda proofs/agda/All.agda and agda proofs/agda/Smoke.agda both exit 0 under --safe --without-K. No postulates anywhere in proofs/agda. https://claude.ai/code/session_01JRLz84fAaWvRBKyXuc4tyK
diff --git a/CLAUDE.md b/CLAUDE.md
@@ -42,13 +42,42 @@ Adjacent projects, in one line each, for session bootstrapping:
 echo-types — constructive Agda formalization of fiber-based structured loss
 ("echo types"). Gated identity-claim development per roadmap-gates.adoc.
 
-Current workstream: **E (ordinal-notation / Buchholz collapsing layer)**
-per docs/buchholz-plan.adoc. Aims to land a proof-theoretic collapsing-function
-target — first credible milestone Bachmann–Howard (ψ₀(Ω_ω)), stretch
-target ψ(Ω_Ω) ≈ TFBO.
+Two active workstreams:
 
-First landed proof: `C-monotone` in proofs/agda/Ordinal/Closure.agda.
-Next planned: E3 CNF trichotomy, then E4 pedagogical `psi-notin-C`.
+1. **Composition track (Echo.agda + echo-types theory docs).** Base
+   accumulation iso `Echo-comp-iso-{to, from, from-to, to-from}`
+   landed. Cancellation forward/backward maps `cancel-iso-{to, from}`
+   landed; full iso deferred pending triangle-identity coherence.
+   Pentagon coherence partial: projection-pentagon lemmas
+   `Echo-comp-iso-pent-{B, echo}` landed as `refl`; full
+   Σ-associativity iso between the two nested Σ-shapes open.
+
+2. **Ordinal track (buchholz-plan.adoc).** Target remains Bachmann–
+   Howard (ψ₀(Ω_ω)) as first credible milestone, stretch to ψ(Ω_Ω)
+   ≈ TFBO. E1–E7 landed (OT syntax, ℕ-staged closure with
+   `C-monotone`, CNF with `cnf-trichotomy`, pedagogical ψ with
+   `psi-notin-C`/`psi-least`, Buchholz scaffold with `Cν-monotone`
+   family, well-formedness with `BH-wf`/`psi-OmegaOmega-wf`, echo
+   bridge with `ordinal-collapse-non-injective`). WF-0 partial
+   Buchholz order `_<ᵇ_` and WF-1 well-foundedness `wf-<ᵇ` landed
+   for the admitted core (currently `Order.agda`'s 13-constructor
+   set including Ω/+ and ψ/+ bridges). Surface / extended / iterated
+   / Veblen layers now live under `Ordinal/Buchholz/*` and feed a
+   second measure route via `VeblenComparisonModel.agda`.
+   Recursive-surface route has a **budgeted** well-foundedness
+   `wf-<ᵇʳᶠᵇ` in `RecursiveSurfaceBudget.agda` (carries ℕ budget
+   alongside BT); the unbudgeted global WF theorem for `_<ᵇʳᶠ_`
+   remains open.
+
+   Open pieces on this track:
+   * Full constructor set beyond the admitted core (K-limited
+     shared-binder cases such as `<ᵇ-ψα`, `<ᵇ-+2`).
+   * Unbudgeted `_<ᵇʳᶠ_` global WF — eliminate the explicit ℕ
+     budget from `wf-<ᵇʳᶠᵇ` without leaving `--safe --without-K`.
+   * Push the surface-route WF back into `Order.agda`'s main
+     `_<ᵇ_` package.
+
+Cross-repo bridge status lives in `docs/echo-types/cross-repo-bridge-status.md`.
 
 # Build
 
@@ -60,10 +89,84 @@ for f in proofs/agda/*.agda proofs/agda/Ordinal/*.agda proofs/agda/Ordinal/Buchh
 done
 ```
 
+Requires Agda ≥ 2.6.3 with stdlib ≥ 2.0. On Ubuntu 24.04 with apt's
+`agda`/`agda-stdlib` (which ships stdlib 1.7.3 and lacks
+`Data.Product.Base`), check out stdlib 2.0 from source:
+```
+git clone --depth 1 --branch v2.0 https://github.com/agda/agda-stdlib.git /opt/agda-stdlib
+sed -i 's/^name: standard-library-2.0$/name: standard-library/' /opt/agda-stdlib/standard-library.agda-lib
+mkdir -p ~/.agda && echo /opt/agda-stdlib/standard-library.agda-lib > ~/.agda/libraries
+```
+Then `LC_ALL=C.UTF-8 agda proofs/agda/All.agda` exits 0.
+
 # Working rules in this repo
 
 - No postulates unless explicitly isolated and justified.
 - `--safe --without-K` throughout.
 - Every edit ends with an Agda compile command and captured output.
-- Every headline theorem must be pinned in Smoke.agda via `using` clause.
-- Branch for ordinal-notation work: claude/add-ordinal-notation-layer-9qhSf.
+- Every headline theorem must be pinned in `Smoke.agda` via `using` clause.
+- Every new module goes into `All.agda` as an `open import` so the
+  verified suite covers it. Orphan modules that compile but are not
+  in `All.agda` are treated as dead code.
+
+## Rung-consolidation policy (added 2026-04-23)
+
+Each time a new proof rung lands on the composition or ordinal
+tracks (a named theorem or iso-shape), consolidate all outstanding
+work to `main` and refresh all documentation:
+
+1. **Branch housekeeping.** Enumerate all open remote branches
+   ahead of `main`. Decide which are landing, which are superseded,
+   and which are abandoned. Merge the landing ones; mark the
+   superseded / abandoned ones in the session ledger.
+2. **Cherry-pick to a consolidation branch** off latest `main`, in
+   dependency order. Resolve any conflicts (typically additive, in
+   `Smoke.agda` and `All.agda`).
+3. **Update human docs.** `docs/echo-types/composition.md`,
+   `docs/echo-types/roadmap.md`, `docs/echo-types/overview.md` and
+   `cross-repo-bridge-status.md` get a sweep for stale `(Open)` /
+   `[unblocked]` tags on anything that just landed. Honest labels:
+   `(Landed)`, `(Partial)`, `(Open)`.
+4. **Update machine docs (this file).** Add the new rung under the
+   active-workstream summary. Update the build instructions if the
+   toolchain changed. Note any new structural constraints that would
+   guide a fresh session's first steps.
+5. **Verify.** `agda proofs/agda/All.agda` and `agda proofs/agda/Smoke.agda`
+   both exit 0 under `--safe --without-K`. No postulates introduced.
+6. **Fast-forward `main`** to the consolidation branch and push.
+7. **Session ledger.** In the session response, record the rung
+   name, the commits folded in, the remaining open pieces of the
+   milestone, and the proposed smallest useful next advance.
+
+## Current rung state (2026-04-23)
+
+Just consolidated: **Budgeted recursive-surface rung** (on top of
+the earlier **Pentagon rung**). Folded in:
+
+* Composition-track (already upstream via separate landings):
+  `cancel-iso-{to, from}`, `Echo-comp-iso-pent-{B, echo}`.
+* Ordinal-track (new on this sweep): `RecursiveSurfaceBudget.agda`
+  with `BudgetedBT = ℕ × BT`, `_<ᵇʳᶠᵇ_`, `wf-<ᵇʳᶠᵇ`,
+  `<ᵇʳᶠᵇ-irreflexive`, and the `<ᵇʳᶠᵇ⇒lifted` bridge into the
+  iterated-wrapper tower. Auxiliary layers (`ExtendedOrder`,
+  `LiftedExtendedOrder`, `IteratedExtendedOrder`,
+  `RecursiveSurfaceOrder`, `SurfaceOrder`, `VeblenInterface`,
+  `VeblenIdentityModel`, `VeblenMeasureTarget`,
+  `VeblenProjectionMeasure`, `VeblenComparisonTarget`,
+  `VeblenComparisonModel`, `VeblenObligations`) are all wired
+  into `All.agda` and pinned in `Ordinal/Buchholz/Smoke.agda`.
+
+Open at this rung:
+
+* Composition side: full cancel-iso round-trips (needs triangle
+  identity); full Σ-associativity iso for pentagon; approximate-echo
+  skeleton `EchoApprox.agda`.
+* Ordinal side: unbudgeted global WF for `_<ᵇʳᶠ_` — eliminate the
+  explicit ℕ budget from `wf-<ᵇʳᶠᵇ` without leaving `--safe --without-K`;
+  then push that back into `Order.agda`'s `_<ᵇ_` package so the
+  WF proof covers the full surface route rather than the admitted
+  core only.
+
+Verified post-rebase: `agda proofs/agda/All.agda` and
+`agda proofs/agda/Smoke.agda` both exit 0 under `--safe --without-K`.
+No postulates introduced.
diff --git a/docs/echo-types/composition.md b/docs/echo-types/composition.md
@@ -153,19 +153,33 @@ coarser bounds.
 *Status.* Entirely speculative. Requires a formal definition of
 approximate echo first.
 
-### Q4. Associativity
+### Q4. Associativity — partially landed
 
 *Question.* Does the accumulation isomorphism above satisfy the
 pentagon coherence for three-fold composition? I.e., for
-`f : A → B`, `g : B → C`, `h : C → D`, does the two ways of
-associating `Echo((h ∘ g) ∘ f) = Echo(h ∘ (g ∘ f))` yield equivalent
+`f : A → B`, `g : B → C`, `h : C → D`, do the two ways of
+associating `Echo((h ∘ g) ∘ f) ≃ Echo(h ∘ (g ∘ f))` yield equivalent
 iso's?
 
-*Expectation.* Yes, but the proof requires the iso to land as a
-`map-over` morphism whose `commute` field is itself proved by
-pentagon-style transitivity. `Echo.map-over-comp` already bottles
-the relevant shape. Proving pentagon on top is routine but not
-written down.
+*Answer (partial).* Yes for the load-bearing projections. The two
+pentagon-style lemmas `Echo-comp-iso-pent-B` and
+`Echo-comp-iso-pent-echo` (both `refl`) confirm that the two
+natural factorings — inner-first `(f, h∘g)` versus outer-first
+`(g∘f, h)` then `(f, g)` — produce the same `f x` at the B-component
+and the same `(x , refl) : Echo f (f x)` at the Echo-f witness. The
+full Σ-associativity iso between the two nested Σ-shapes (which
+differ by whether the intermediate `c : C` with `g b ≡ c` is
+carried or absorbed) is the remaining open piece of pentagon
+coherence.
+
+*Evidence this is the right shape.* Both lemmas land as `refl`
+without any `trans-assoc` / `cong-trans` manipulation, because
+`Echo-comp-iso-to`'s body `(x , p) ↦ (f x , (x , refl) , p)` is
+structurally symmetric in the outer function — the f-component
+and witness do not depend on which outer is peeled off. If the
+iso had a `trans`-shaped body instead, pentagon would have
+required real coherence lemmas; the `refl` outcome is evidence
+the iso has the right design.
 
 ### Q5. Interaction with role-indexing, gradings, linearity
 
@@ -209,7 +223,10 @@ Collecting the above:
    `s-right`). Round-trips deferred pending a triangle-identity
    coherence or a stdlib `Function.Bundles.Inverse` shim.
 
-4. **(Open) Pentagon.** Three-fold composition associates.
+4. **(Partial) Pentagon.** Three-fold composition associates at
+   the projections. `Echo-comp-iso-pent-B` and
+   `Echo-comp-iso-pent-echo` both `refl`; full Σ-shape iso still
+   open.
 
 5. **(Open) Tolerance calculus.** For approximate echoes, tolerances
    compose with a Lipschitz-like law.
@@ -229,9 +246,10 @@ Ranked by unblock-value. (1) and (2) landed; (3) onwards is open.
 2. ~~**Cancellation corollary.**~~ Partially landed as
    `cancel-iso-to` / `cancel-iso-from`; full iso deferred pending
    triangle-identity coherence (see §3 above).
-3. **Pentagon coherence.** Three-fold composition associates.
-   Moderate proof on top of `Echo-comp-iso`, probably one more
-   lemma. Next concrete follow-up on this track.
+3. ~~**Pentagon coherence.**~~ Partially landed: the two
+   projection-level pentagon lemmas (`-pent-B`, `-pent-echo`)
+   ship as `refl`. The full Σ-associativity iso between the two
+   nested shapes remains open.
 4. **Full cancel-iso with round-trips.** Needs an equivalence
    record that packages `s-left`, `s-right`, and the triangle
    identity as three fields, or direct use of stdlib's
diff --git a/docs/echo-types/roadmap.md b/docs/echo-types/roadmap.md
@@ -58,8 +58,23 @@ Paths marked **[unblocked]** can proceed today. Paths marked
   needing only the relevant half of g's iso structure. Round-trips
   are **deferred** pending a triangle-identity coherence or a stdlib
   `Function.Bundles.Inverse` shim. See `composition.md` §3.
-- **[unblocked]** Pentagon coherence for three-fold composition.
-  Routine proof on top of `Echo-comp-iso`; next concrete follow-up.
+- **[partial]** Pentagon coherence for three-fold composition.
+  `Echo-comp-iso-pent-B` and `Echo-comp-iso-pent-echo` both `refl`
+  in `Echo.agda`. The full Σ-associativity iso between the two
+  nested Σ-shapes (outer-first carries an extra intermediate
+  `c : C` with `g b ≡ c`; inner-first absorbs it) remains the open
+  piece of pentagon.
+- **[partial]** Budgeted recursive-surface WF on the ordinal track.
+  `Ordinal/Buchholz/RecursiveSurfaceBudget.agda` ships
+  `BudgetedBT = ℕ × BT`, the budgeted relation `_<ᵇʳᶠᵇ_` with its
+  `spend` constructor, `wf-<ᵇʳᶠᵇ : WellFounded _<ᵇʳᶠᵇ_` (via
+  subrelation on ℕ), and `<ᵇʳᶠᵇ⇒lifted` transporting each budgeted
+  step into the iterated-wrapper tower (`IteratedExtendedOrder`).
+  The unbudgeted global theorem — eliminate the explicit ℕ budget
+  from `wf-<ᵇʳᶠᵇ` to get `WellFounded _<ᵇʳᶠ_` — is the next
+  concrete ordinal-track milestone. Pushing that result back into
+  `Ordinal/Buchholz/Order.agda`'s main `_<ᵇ_` package is the step
+  after that.
 - **[unblocked]** `EchoApprox.agda`: new module for ε-indexed echoes
   over a metric codomain. First-class taxonomy axis 2 artifact.
 - **[unblocked]** Per-decoration composition lemmas in `EchoGraded`,
@@ -157,23 +172,32 @@ tractable today:
    iso plus both cancellation maps now live in `Echo.agda`; the full
    cancellation iso (with round-trips) is the first deferred item —
    needs a triangle-identity coherence (see composition.md §3).
-3. **Agda: pentagon coherence for `Echo-comp-iso`** — 1 day. Next
-   natural follow-up on the composition track.
-4. **Gate 1 adjacency refresh against the new taxonomy** — 1 day.
+3. ~~**Agda: pentagon coherence for `Echo-comp-iso`**~~ — projection
+   pentagon landed as `Echo-comp-iso-pent-{B, echo}`. Full
+   Σ-associativity iso between the two nested Σ-shapes is one of
+   two next composition-track follow-ups (the other is
+   full-cancel-iso round-trips, which needs a triangle identity).
+4. **Agda: unbudgeted `_<ᵇʳᶠ_` WF on the ordinal track** — eliminate
+   the explicit ℕ budget from `wf-<ᵇʳᶠᵇ` in
+   `RecursiveSurfaceBudget.agda`. Sharpest next ordinal-track move
+   since the budgeted version already ships. Keep `--safe --without-K`.
+   Pushing the result back into `Order.agda`'s `_<ᵇ_` is the step
+   after.
+5. **Gate 1 adjacency refresh against the new taxonomy** — 1 day.
    Cheap coherence pass on existing docs.
-5. **Theory: pick one axis-8 refinement and formalise it** — 1–2
+6. **Theory: pick one axis-8 refinement and formalise it** — 1–2
    days. Four candidates in `taxonomy.md` §8 (cost-indexed echo,
    graded access modality, decidability-respecting echo, witness-
    search abstract machine). Choosing commits the repo to one
    formal handle on computational vs information-theoretic access.
-6. **Agda: `EchoApprox.agda`** — 2–3 days. First artifact of axis 2.
-7. **Applications chapter: compiler-analysis residue** — 2 days.
+7. **Agda: `EchoApprox.agda`** — 2–3 days. First artifact of axis 2.
+8. **Applications chapter: compiler-analysis residue** — 2 days.
    Largest reader value; entirely unblocked.
-8. **Per-decoration composition lemmas** — 1 day each. Useful
+9. **Per-decoration composition lemmas** — 1 day each. Useful
    coverage.
 
-Steps 1–4 are ~5–6 days of honest work that require nothing from
-proof assistants, external repos, or the blocked Buchholz path.
+Steps 1 and 5–6 are ~5–6 days of honest work that require nothing
+from proof assistants, external repos, or the blocked Buchholz path.
 Steps 5–7 extend into Agda but depend only on infrastructure we
 already have in-suite.
 
