diff --git a/CLAUDE.md b/CLAUDE.md index 62f942f..429fd8d 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -210,7 +210,78 @@ 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-06-18) +## Current rung state (2026-06-20) + +### Session arc 2026-06-20 — variance resolution + Veblen climb rungs 3–6 + ordinal-fidelity ladder PARKED (read this first) + +*Where we started:* user supplied the sharpened understanding of an +echo-type (a tropically-graded modality of structured loss: graded-(co)monad +machinery over the min-plus semiring, recoverable *exact on a homotopy +fibre rather than complement-storing*, variance unsettled). Then asked to +RESOLVE the monad/comonad/adjunction variance in `--safe` Agda, then to +continue the ordinal track toward ψ₀(Ω_ω). + +*Where we ended:* SEVEN PRs merged to `main`, then the ordinal ladder +PARKED by owner decision. All `--safe --without-K`, zero postulates, no +`TERMINATING`, kernel-guard PASS. + +1. **Variance resolved (#243).** `EchoVariance.agda` — verdict: echo + (fibre-based loss) is a graded **MONAD of accumulation** (the `+` axis, + `accumulate = Echo-comp-iso-from`) with a section/retraction + **ADJUNCTION exact on the grade-0 fibre** (`recoverable-fibre = + A↔ΣEcho`); it is **NOT a graded comonad** — the comonad reading is the + LOSSLESS complement-storing writer (`EchoGradedComonadF1`'s `δ` is `coe` + along a type equality, inverted by `μ-writer`). `no-bare-recovery` + (via `no-section-of-collapsing-map`) is the comonad obstruction. Sharpens + R-2026-05-18 from "graded comonad withdrawn" to "decided against". Doc: + `docs/echo-types/variance-resolution.adoc`; paper Reframing-note + follow-up `F-2026-06-19`. DO NOT reopen: the verdict, or the + complement-storing-writer framing. + +2. **Veblen climb rungs 3–6 (#244–#247), Brouwer side.** + * `#244` `VeblenPhiNormal` — φ₁ a normal function; `next-ε-least` + (next-ε β is the LEAST ε-number above β). + * `#245` `VeblenBinary` — binary `φ : Ord → Ord → Ord` (the tractability + move: recursion on the FIRST arg returning `Ord → Ord`, second-arg + recursion inside the generic `deriv`; no `TERMINATING`); generic engine + `deriv`/`nextFix`/`commonStep`; `φ-cont`; `nextFix-fixed-{≤,≥}`; the + diagonal `Γ₀` defined. + * `#246` `VeblenBinaryNormal` — EVERY level a normal function (`φ-mono₂`, + `φ-infl`); the Veblen recurrence `φ-level-fixed-{≤,≥}` (φ_{α+1}(β) is a + fixed point of φ_α). + * `#247` `VeblenBinaryMono` — first-arg monotonicity (`φ-mono₁-step`, + `φ-mono₁-into-lim`); `commonStep` correctness; `Γ₀-prefixed` + (**Γ₀ ≤′ φ_Γ₀(0)**, one direction of the diagonal fixed point). + Reusable lesson: every `≤′-trans`/`≤′-lim`/`*-mono`/`≤′-zero` call pins + its implicit source explicitly — `_≤′_` is a reducing relation. + +3. **Ordinal-fidelity ladder PARKED (`D-2026-06-20`).** Owner decision: the + transfinite ladder is now CONSUMER-LESS — the Groove cleave (sole consumer + of ψ₀(Ω_ω) order-type fidelity) is resolved as a finite exact-round-trip + zipper needing well-foundedness only, and Groove RC-11 forbids ε₀+ in + cleave ranks. This is a PARK (resumable), NOT a kill/retraction — + fidelity was always flagged OPEN. **DO NOT open the Veblen mutual + fixed-point descent rung** (the gate to Γ₀-least). No postulate closed; + `D-2026-06-14` stands. Record: + `docs/echo-types/decisions/ordinal-fidelity-ladder-parked.adoc`. + * *Frontier for cold resume:* Γ₀-least OPEN; wall = reverse + `φ_Γ₀(0) ≤′ Γ₀` → "Γ₀ closed under every level below it" → general + first-arg monotonicity `φ_α x ≤′ φ_β x` → gated on the mutual + fixed-point descent (monotonicity + descent mutually recursive). + Downstream OPEN: the ψ collapsing function (produces `bh-height`), then + the two `Fidelity.agda` postulates `denotation` / `ordinal-upper-bound` + (gated on the collapse). + * *Disposition:* extraction to its own ordinal-notation repo (Löwe / + classical-order-type side, labelled OPEN) — cut FLAGGED, left to owner. + Firewall verified clean: `OmegaMarkers` (leaf) ← `Buchholz.Syntax` ← + `EchoOrdinal` STAY; everything else under `Ordinal/` MOVES. Supersedes + any "re-home into Groove" framing (RC-11 retired it). + +*Plan for the next Claude.* The ordinal ladder is PARKED — do not resume it +unless the consumer returns (then start at the mutual-descent rung per the +park record). The variance resolution is complete and consumed. Other +tracks (composition, establishment Pillar E, the EchoTypes.jl mirror) are +unaffected by the park. ### Session arc 2026-06-18 — EchoAggregation general/macro split + long-form prose relicense (read this first) diff --git a/docs/echo-types/decisions/ordinal-fidelity-ladder-parked.adoc b/docs/echo-types/decisions/ordinal-fidelity-ladder-parked.adoc new file mode 100644 index 0000000..f6500fa --- /dev/null +++ b/docs/echo-types/decisions/ordinal-fidelity-ladder-parked.adoc @@ -0,0 +1,158 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell += D-2026-06-20 — Ordinal-fidelity ladder PARKED (consumer removed) +:toc: macro +:toclevels: 2 +:sectnums: +:sectnumlevels: 2 +:icons: font + +[.lead] +Records, in the same dated idiom as `D-2026-06-14` (its parent) and the +retraction log's `R-2026-05-18`, the decision to *park* the transfinite +ordinal-fidelity ladder. This is a *PARK* — not a kill and not a +retraction. Nothing was over-claimed: order-type fidelity was always +flagged OPEN (`D-2026-06-14` stands, unchanged). The ladder is correct, +well-built, `--safe --without-K`, zero-postulate — and, as of this date, +*unconsumed*. It is frozen at a clean rung and is fully resumable. + +toc::[] + +== Status + +*Ordinal-fidelity ladder: PARKED, resumable.* The Brouwer-ordinal Veblen +climb (rungs 1–6) is frozen at its current rung. No further rung is to be +opened (in particular *not* the Veblen mutual fixed-point descent lemma — +see §"Frontier"). The doubled-ladder well-foundedness work and the +`Fidelity.agda` shape remain as they were. No postulate was closed by the +parking sweep. + +== Reason (the consumer was removed) + +The only consumer that ever required ψ₀(Ω_ω) *order-type fidelity* was the +Groove cleave. Two independent facts one layer up retire that need: + +. *Groove RC-11 (ordinal economy)* forbids ε₀ and above in cleave ranks. + The ladder is already past ε₀ at rung 2 (ε₀ is an ε-number); Γ₀ + (rung 4+) is far past it; ψ₀(Ω_ω) is unreachably beyond. So the ladder's + target is *outside the consumer's permitted range by construction*. +. *The cleave has resolved* to a finite *exact-round-trip zipper* that + needs *well-foundedness only* — no transfinite order-type fidelity at + all. + +Therefore the order-type-fidelity result is now *consumer-less*. The +project's own standing caveat — "steady honest progress up a long ladder, +not reaching the milestone" — becomes, in this light, the argument to +*stop*: the ladder is correct, well-built, and unconsumed. + +On the constructive/classical seam: every rung (the mutual-descent lemma +included) is structure on the *near side* of the open `denotation` map — +it builds the tower, it does not certify the tower is the claimed height. +Even if mutual-descent closed cleanly it reaches only Feferman–Schütte +(Γ₀), galaxies below target. The hard lemma does not reach the thing. + +== What is frozen (the artifact inventory) + +The ladder as it stands is a coherent, well-scoped artifact. Landed, +`--safe --without-K`, zero postulates, no `TERMINATING`, kernel-guard +PASS: + +[cols="1,3",options="header"] +|=== +| Module | Content + +| `Ordinal.Brouwer.OrdinalExp` +| `ω^^_` (ω to an ordinal power), `ε₀`, `ε₀-ε-number`, `ω^^-infl`. + +| `Ordinal.Brouwer.VeblenPhi` +| `next-ε`, `φ₁` (ε-number enumeration), `φ₁-ε-number`. + +| `Ordinal.Brouwer.VeblenPhiNormal` +| `ω^^-mono-≤′`; `next-ε-least` (next-ε β is the LEAST ε-number above β); + `φ₁` a normal function (`φ₁-mono` / `φ₁-strict-mono` / `φ₁-continuous`). + +| `Ordinal.Brouwer.VeblenBinary` +| Binary Veblen `φ : Ord → Ord → Ord` (generic fixed-point engine + `deriv` / `nextFix` / `commonStep`); `φ-cont`; engine correctness + `nextFix-fixed-{≤,≥}`; the diagonal `Γ₀` (Feferman–Schütte) defined. + +| `Ordinal.Brouwer.VeblenBinaryNormal` +| EVERY level a normal function (`φ-mono₂`, `φ-infl`); the Veblen + recurrence `φ-level-fixed-{≤,≥}` (φ_{α+1}(β) is a fixed point of φ_α). + +| `Ordinal.Brouwer.VeblenBinaryMono` +| First-argument monotonicity (`φ-mono₁-step`, `φ-mono₁-into-lim`); + `commonStep` correctness; `Γ₀-prefixed` (*Γ₀ ≤′ φ_Γ₀(0)* — one + direction of the diagonal fixed point). +|=== + +The Buchholz well-foundedness apparatus (`_<ᵇ_`, the sound doubled-ladder +`_<ᵇ²_` + `wf-<ᵇ²`, `RankBrouwer`, `BHTarget`) and the order-type-fidelity +*shape* (`Ordinal.Buchholz.Fidelity`, two open postulates) are unchanged. + +== Frontier (captured for cold resumption) + +If the consumer ever returns, resume here: + +. *Γ₀-least is OPEN.* `Γ₀ ≤′ φ_Γ₀(0)` is done (`Γ₀-prefixed`). The wall is + the *reverse* direction `φ_Γ₀(0) ≤′ Γ₀` (closure from above), which + reduces to *"Γ₀ is closed under every level `φ_α` below it"*. That needs + *general first-argument monotonicity* `φ_α x ≤′ φ_β x` for `α ≤′ β`, + which is *gated on the Veblen mutual fixed-point descent lemma*: "a + fixed point of `φ_β` is a fixed point of `φ_α` for `α ≤′ β`", with + monotonicity and descent *mutually recursive* over the level. The + adjacent (`φ-mono₁-step`) and below-a-limit (`φ-mono₁-into-lim`) cases + are already proved (rung 6); the general successor/successor case is the + intricate mutual induction that was deliberately *not* opened. +. *The ψ collapsing function* with fundamental sequences — the separate, + multi-session core that eventually produces `bh-height`. Unchanged and + OPEN. +. *The two `Fidelity.agda` postulates* `denotation` (order-reflecting, + height-preserving `⟦·⟧`) and `ordinal-upper-bound` — *gated on the + collapse existing*. Unchanged and OPEN. `denotation` canNOT be `rank2` + (height-collapsing). + +*No postulate closed. Order-type fidelity remains OPEN; `D-2026-06-14` +stands.* + +== Disposition / re-home (extraction FLAGGED, cut left to the owner) + +The transfinite ladder is now a *consumer-less, free-standing artifact*. +The clean ending is *extraction to its own ordinal-notation repository*, +parked on the *Löwe (classical order-type)* side of the constructive / +classical seam and labelled OPEN. This *supersedes* any earlier "re-home +into Groove" framing — RC-11 retired that. + +*The firewall is clean (verified 2026-06-20).* The three modules that +*STAY* in echo-types as the bridge form a self-contained subgraph that +does *not* depend on the transfinite ladder: + +* `Ordinal.OmegaMarkers` — a leaf (no ordinal-ladder imports); +* `Ordinal.Buchholz.Syntax` — imports only `Ordinal.OmegaMarkers`; +* `EchoOrdinal` — imports only `Ordinal.OmegaMarkers` + + `Ordinal.Buchholz.Syntax` (its *only* ordinal dependencies). + +So the cut is clean: *everything else* under `proofs/agda/Ordinal/` +(the Brouwer foundations `Brouwer` / `Phase13` / `OmegaPow` / `Arithmetic`, +the `OrdinalExp` + `Veblen*` ladder, the Buchholz `Order` / rank / +doubled-ladder / `Fidelity` / `BHTarget` machinery, `CNF` / `Closure` / +`PsiSimple` / `Base`) is the *consumer-less artifact* that MOVES; the three +bridge modules above STAY. + +*This entry FLAGS the extraction; it does not perform it.* The actual cut +is the owner's: it is a cross-repo operation (new repository creation + +moving a ~70-module dependency-entangled subtree + re-rooting its +`.agda-lib` include path) that must preserve, on *both* sides, the +build invariant `--safe --without-K` / zero postulates / no `TERMINATING` +/ kernel-guard PASS. The proposed cut-line above is the boundary; the +slice is left to the owner. + +== See also + +* `docs/echo-types/decisions/ordinal-bh-order-type-fidelity-open.adoc` + — `D-2026-06-14`, the parent open-problem record (stands, unchanged). +* `Fidelity-OPEN-postulates.md` — the two open `Fidelity.agda` postulates. +* `docs/echo-types/buchholz-rank-obstruction.adoc` — carrier soundness + + the doubled-ladder closure. +* `docs/bridges/buchholz-plan.adoc` — the E-stage matrix / BH staging. +* `roadmap.adoc` §Lane 3 — the ordinal-track items (now parked). diff --git a/docs/proof-debt.md b/docs/proof-debt.md index 8c259c1..b92a3b4 100644 --- a/docs/proof-debt.md +++ b/docs/proof-debt.md @@ -98,6 +98,14 @@ under one of (a) discharged / (b) budgeted / (c) necessary axiom / (d) debt. order-type fidelity OPEN". - **Citation**: `D-2026-06-14`; full per-postulate spec (statement / what closes it / owner) in `Fidelity-OPEN-postulates.md`. + - **PARKED (2026-06-20, `D-2026-06-20`)**: the transfinite ladder these + postulates sit atop is now *consumer-less* — the Groove cleave (the + only consumer of ψ₀(Ω_ω) order-type fidelity) is resolved as a finite + exact-round-trip zipper needing well-foundedness only, and RC-11 + forbids ε₀+ in cleave ranks. The debt is therefore *parked, + resumable*, not actively being closed. No postulate closed; + `D-2026-06-14` stands. See + `docs/echo-types/decisions/ordinal-fidelity-ladder-parked.adoc`. - **Guardrail status**: allow-listed in `tools/check-guardrails.sh` (`EXPLORATORY_EXEMPT`) and the inline `hypatia: allow` pragma at the module head. (`BHTarget` is NOT exempt — it is real kernel content diff --git a/roadmap.adoc b/roadmap.adoc index 3a5ea50..3d222bf 100644 --- a/roadmap.adoc +++ b/roadmap.adoc @@ -305,7 +305,20 @@ narrowed — no unique-mediator claim. Demand 4 ("parametricity") must be *consumer-side at the affine instance*, not full Reynolds. See respective §s in the synthesis doc. -=== Lane 3 [PARALLEL, NOT LOAD-BEARING] — Ordinal / Buchholz +=== Lane 3 [PARKED 2026-06-20, NOT LOAD-BEARING] — Ordinal / Buchholz + +*PARKED (`D-2026-06-20`).* The transfinite ordinal-fidelity ladder is +*parked, resumable* — the only consumer of ψ₀(Ω_ω) order-type fidelity +(the Groove cleave) is resolved as a finite exact-round-trip zipper +needing well-foundedness only (RC-11 forbids ε₀+ in cleave ranks), so the +ladder is consumer-less. The Veblen climb (rungs 1–6: `ω^^`/ε₀ → φ₁ normal +→ binary φ + Γ₀ → every level normal → first-arg monotonicity + +`Γ₀ ≤′ φ_Γ₀(0)`) is frozen at a clean rung; the next rung (Veblen mutual +fixed-point descent → Γ₀-least) is deliberately NOT opened. No postulate +closed; order-type fidelity REMAINS OPEN (`D-2026-06-14` stands). The +disposition is extraction to its own ordinal-notation repo (cut FLAGGED, +left to the owner). See +`docs/echo-types/decisions/ordinal-fidelity-ladder-parked.adoc`. *Echo Core does NOT depend on this lane.* This is a separate proof-theoretic research project that happens to share the