Merge branch 'main' into experimental/echo-additive-r2-r3

Author: hyperpolymath

.github/workflows/codeql.yml

@@ -31,11 +31,10 @@ jobs:
       fail-fast: false
       matrix:
         include:
-          - language: javascript-typescript
-            build-mode: none
-          # Also analyse the GitHub Actions workflows themselves
-          # (CodeQL `actions` language) — directly relevant given the
-          # workflow-hardening in this PR, and closes the Hypatia
+          # CodeQL `actions` language scans the GitHub Actions workflow
+          # files (present in every repo). The repo has no JS/TS source,
+          # so the prior JS/TS matrix entry recorded zero results /
+          # failed "no source files"; closes the Hypatia
           # `codeql_missing_actions_language` finding.
           - language: actions
             build-mode: none

.machine_readable/agent_instructions/debt.a2ml

@@ -11,41 +11,68 @@
 
 [metadata]
 version = "1.0.0"
-last-updated = "2026-06-12"
+last-updated = "2026-06-14"
+
+# ============================================================================
+# OUTSTANDING PROOFS — the live frontier (single inventory, 2026-06-14)
+#
+# Status legend:
+#   OPEN-EXTERNAL  — mechanisable, but needs new external mathematics
+#                    (no in-repo route exists yet).
+#   WALLED         — proven not closable on the current object under
+#                    --safe --without-K; close-out is a falsifiable verdict.
+#   OPEN-DESIGN    — closable, but gated on a substantial design decision
+#                    (e.g. truncation / Cubical).
+#   MECHANICAL     — closable now, bounded, no new ideas needed.
+#
+# 2026-06-14 progress note: the two long-standing ordinal "should"
+# items (unbudgeted _<ᵇʳᶠ_; K-limited shared-binder; surface-route WF)
+# are now DONE in their ACHIEVABLE (sound-carrier) form — wf-<ᵇ²,
+# wf-<ᵇʳᶠ², wf-<ᵇ⁺² (PRs #208/#212/#214). What remains of them is the
+# native-order form, which is WALLED. All four paper.adoc [EXPAND]
+# tags are cleared (#215). The genuine remaining ordinal frontier is
+# now order-type fidelity (D-2026-06-14).
+# ============================================================================
 
 # ============================================================================
 # SHOULD — would fix next wave
 # ============================================================================
 
 [[debt.should]]
-component = "ordinal-track / Ordinal.Buchholz"
-issue = "Unbudgeted _<ᵇʳᶠ_ global WF: eliminate the explicit ℕ budget from wf-<ᵇʳᶠᵇ without leaving --safe --without-K."
+component = "ordinal-track / Bachmann-Howard order-type fidelity"
+issue = "Order-type fidelity: prove the well-formed Buchholz notation IS the Bachmann-Howard ordinal order, not merely well-founded. Either (a) a verified order-preserving denotation ‖·‖ : BT → 𝒪 of height ψ₀(Ω_ω) with s <ᵇ t iff ‖s‖ < ‖t‖ on the well-formed fragment, or (b) a direct order-type computation (fundamental sequences / collapsing-function correctness)."
+status = "OPEN-EXTERNAL"
 effort = "hard"
 impact = "high"
-discovered = "2026-05-20"
-note = "Solo, not swarmable; the named next bottleneck toward Bachmann-Howard."
+discovered = "2026-06-14"
+note = "Decision-log D-2026-06-14 (decisions/ordinal-bh-order-type-fidelity-open.adoc). The genuine remaining ordinal-strength frontier; WF (done, sound-carrier) is the prerequisite, not the result. Gates the Pillar E ordinal appendix's strong reading (the WF-milestone appendix is already written, #215)."
 
 [[debt.should]]
-component = "ordinal-track / Order.agda"
-issue = "Push the surface-route WF back into Order.agda's main _<ᵇ_ package; close the K-limited shared-binder cases (<ᵇ-ψα, <ᵇ-+2)."
+component = "ordinal-track / Order.agda (native _<ᵇ_)"
+issue = "Global-native well-foundedness: unbudgeted wf-<ᵇʳᶠ AND the K-limited shared-binder cases (<ᵇ-ψα, <ᵇ-+2) over NATIVE _<ᵇ_ (not the sound carrier)."
+status = "WALLED"
 effort = "hard"
-impact = "high"
+impact = "low"
 discovered = "2026-04-28"
+note = "Native _<ᵇ_ is ordinally unsound (the <ᵇ-+Ω counterexample); all five rank/direct/lex/tower/inverse-image routes are walled (RankBrouwer.agda preamble + buchholz-rank-obstruction.adoc), and rank2 does not escape it. The ACHIEVABLE (sound-carrier) forms are DONE: wf-<ᵇ² / wf-<ᵇʳᶠ² / wf-<ᵇ⁺². Realistic close-out for the native form is a FALSIFIABLE VERDICT, not a positive proof — write it when this item is next picked up."
 
 [[debt.should]]
-component = "establishment-track / docs/echo-types/paper.adoc"
-issue = "Clear remaining [EXPAND] tags (related work; evaluation; ordinal consumer-evidence appendix)."
-effort = "medium"
-impact = "medium"
-discovered = "2026-05-17"
-note = "Author-driven; the ordinal appendix is gated on the Bachmann-Howard milestone. Do NOT auto-run outreach / Zenodo / packaging."
-
-[[debt.should]]
-component = "establishment-track / EchoImageFactorization"
-issue = "Image factorisation (epi, mono) earn-back requires propositional truncation (Cubical Agda, or a postulated ∥_∥ interface with scoped honest-scope). Substantial design decision."
+component = "establishment-track / EchoImageFactorization (epi, mono)"
+issue = "Image factorisation (epi, mono) earn-back requires propositional truncation. The postulated-interface placeholder lives in EchoImageFactorizationPropPostulated.agda (the tree's ONLY postulate; not in All.agda)."
+status = "OPEN-DESIGN"
 effort = "hard"
 impact = "medium"
 discovered = "2026-05-27"
+note = "Cubical Agda (different --safe flag profile) OR a postulated ∥_∥ interface with scoped honest-scope. Substantial design decision; the (equivalence, projection) upper form is already done (Tier 1 + F5)."
+
+[[debt.should]]
+component = "earn-back-track / examples/Transport.agda (Gate-3)"
+issue = "Two disclosed open items in the transport/Gate-3 example, pending a K-free reformulation (coe-cong-R ∘ sym push). Stated in-file as precise OPENs."
+status = "OPEN-DESIGN"
+effort = "medium"
+impact = "low"
+discovered = "2026-05-20"
+note = "See earn-back-plan.adoc; nothing is postulated — the items are honestly-stated gaps awaiting a K-free route."
 
 # ============================================================================
 # COULD — would fix eventually
@@ -54,16 +81,19 @@ discovered = "2026-05-27"
 [[debt.could]]
 component = "establishment-track / decoration zoo"
 issue = "Wire the remaining decoration modules (Cost / Search / Indexed / Epistemic) as ResidueForm / DecorationStructure instances; mechanical per-module work."
+status = "MECHANICAL"
 effort = "medium"
 impact = "low"
 discovered = "2026-05-27"
 
 [[debt.could]]
 component = "establishment-track / Q2.1 truncation generalisation"
 issue = "Generalise echo-not-prop: for non-injective f with two distinct preimages of y, is-prop (Echo f y) → ⊥. High-leverage for the truncation distinctness argument but currently low-priority."
+status = "OPEN-DESIGN"
 effort = "medium"
 impact = "medium"
 discovered = "2026-04-29"
+note = "Shares the propositional-truncation design decision with the (epi, mono) earn-back; resolving one likely informs the other."
 
 [[debt.could]]
 component = "rsr-conformance (root Intentfile)"

CLAUDE.md

@@ -206,9 +206,109 @@ 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-13)
-
-### Session arc 2026-06-13 Deniability track — EchoDeniability + wiki (read this first)
+## Current rung state (2026-06-14)
+
+### Session arc 2026-06-14 Ordinal track — doubled-ladder Gate 1 closure (read this first)
+
+*Where we started:* Gate 1's residual was the EQUAL-Ω boundary
+`bpsi ν α <ᵇ bOmega ν` (ψ_ν(α) < Ω_ν at the SAME marker). The
+single ω-power ladder gives ψ and Ω the same exponent block, so
+`rank-pow` collapses them (can't order `<ᵇ-ψΩ≤`) and `rank-adm`
+inverts `<ᵇ-Ωψ`. A doubled-ladder design (ψ_ν ↦ ω^(2ν+1),
+Ω_ν ↦ ω^(2ν+2)) had its arithmetic spine + `rank2` + the equal-Ω
+discharge landed (PRs #202/#203); the WfAdm→rank2 bridge was the
+next piece.
+
+*Where we ended:* the doubled-ladder programme is COMPLETE — Gate 1
+closed for the sound carrier. Six PRs (#204-#209), all
+`--safe --without-K`, zero postulates, structural recursion (no
+`TERMINATING`):
+
+* `#204` — `rank2-bounded : WfAdm t → rank-pow t <′ ω-rank-pow μ →
+  rank2 t <′ ω-rank-pow (double μ)`, the scale-transfer bridge.
+  NOT a plain map: `rank-pow (bpsi ν _) = ω-rank-pow ν` collapses the
+  ψ-argument α that `rank2` keeps, so the WfAdm `wf-adm-bpsi` field
+  supplies the per-ψ admissibility bound the bpsi case recurses on.
+* `#205` — 4 atomic-boundary primitives (`RankDoubledLadderMono`):
+  `rank2-mono-{ΩΩ,Ωψ,ψΩ,ψΩ≤}`. The `<ᵇ-ψΩ≤` equal-Ω boundary splits
+  `ν ≤Ω μ` via `≤Ω-split`.
+* `#206` — 5 bzero/via-left primitives (`RankDoubledLadderMonoPlus`):
+  `rank2-pos-{bOmega,bpsi}`, `rank2-mono-{0-+,Ω+,ψ+}`.
+* `#207` — 3 bplus-on-left primitives. `RankDoubledLadderAddPrincipal`
+  adds Ω-block additive principality (`additive-principal-base` — the
+  OmegaPow proof re-stated over an arbitrary base, for the ω-marker
+  target `ω-rank-pow-succ ω = olim (λ n → ω-rank-pow ω ·ℕ n)`) +
+  `rank2-mono-+Ω`; `RankDoubledLadderMonoPlus2` adds `rank2-mono-+ψ`
+  (ψ-block additive principality) + `rank2-mono-+1` (joint-bplus,
+  ⊕-left-weakening).
+* `#208` — THE CAPSTONE (`RankDoubledLadderUmbrella`): the
+  rank2-soundness-ready relation `_<ᵇ²_` over all 12 core
+  constructors (WfAdm witnesses + the `<ᵇ-+ψ` leading-power bound
+  `rank-pow x <′ ω-rank-pow ν` + WfCNF tail bounds `y ≤ᵇ² x` baked
+  in), the umbrella `rank2-mono-<ᵇ² : s <ᵇ² t → rank2 s <′ rank2 t`
+  (structural recursion dispatching to the 12 primitives), the
+  `≤ᵇ²` companion, and `wf-<ᵇ² : WellFounded _<ᵇ²_` via the standard
+  `Subrelation` + `On.wellFounded rank2 wf-<′` transport.
+* `#209` — doc consolidation in `buchholz-rank-obstruction.adoc`.
+
+*Key honest-scope insight (DO NOT reopen as "incomplete").* `_<ᵇ²_`
+is a SOUND CARRIER, exactly like the existing `_<ᵇ⁰_` / `_<ᵇᵘ_`.
+It excludes the ordinally-unsound native witnesses (the `<ᵇ-+Ω`
+counterexample `bplus bzero (bOmega (fin 1)) <ᵇ bOmega (fin 0)` is
+NOT an `_<ᵇ²_` derivation — its tail bound `y ≤ᵇ² x` fails). There is
+NO faithful projection `<ᵇ → <ᵇ²` and that is not a gap: native
+`_<ᵇ_` is ordinally unsound, so no rank embedding maps it, and its
+well-foundedness is ALREADY proved directly in
+`WellFounded.wf-<ᵇ` (structural, no rank). The doubled ladder's
+contribution is a STRICTLY STRONGER sound carrier than the
+single-ladder union `_<ᵇᵘ_`: it closes the equal-Ω boundary
+`<ᵇ-ψΩ≤` and the bplus-target `<ᵇ-+1` (the single-ladder Gate 1's
+open blocker) with ONE ordinally-sound scalar rank.
+
+*Follow-on (PR #212): the recursive-surface budget eliminated on the
+sound carrier.* `Ordinal.Buchholz.RecursiveSurfaceSound` lands
+`_<ᵇʳᶠ²_` (= `_<ᵇ²_` core + the two same-binder congruences `ψα`/`+2`)
+and its UNBUDGETED `wf-<ᵇʳᶠ²` via the `rank2` embedding: `<ᵇʳᶠ²-core`
+→ `rank2-mono-<ᵇ²`, the two congruences → `⊕-mono-<-right`. This is
+roadmap open-item #1 ("eliminate the ℕ budget from `wf-<ᵇʳᶠᵇ`") in its
+ACHIEVABLE form. The budget was an artefact of native `_<ᵇ_`'s
+unsoundness, not of the same-binder recursion. DO NOT reopen the
+GLOBAL unbudgeted `wf-<ᵇʳᶠ` over native `_<ᵇ_`: all five routes are
+walled (`RankBrouwer.agda` preamble) and `rank2` does NOT escape the
+`<ᵇ-+Ω` counterexample — its realistic close-out is the falsifiable
+"cannot close under `--safe --without-K`" verdict, not a positive
+proof.
+
+*The `<ᵇ-+ψ` leading-power subtlety (load-bearing).* `rank2-mono-+ψ`
+needs the source pieces below the ψ-block's LEADING power
+`ω-rank-pow (double ν)` — strictly stronger than "below the whole
+ψ-rank" (which is all plain recursion gives, and `ω-rank-pow(double ν)
+⊕ rank2 α` is NOT additive principal). So `<ᵇ²-+ψ` carries
+`WfAdm x` + `rank-pow x <′ ω-rank-pow ν`, and the umbrella transfers
+it via `rank2-bounded`. Do not try to reformulate `rank2-mono-+ψ`
+with whole-ψ-rank premises — it is mathematically insufficient.
+
+*Module map (all under `proofs/agda/Ordinal/Buchholz/`):*
+`RankDoubledLadder` (rank2 + spine + bridge), `…Mono` (4 atomic),
+`…MonoPlus` (5 bzero/via-left), `…AddPrincipal` (+Ω + base-generic
+additive principality), `…MonoPlus2` (+ψ, +1), `…Umbrella`
+(`_<ᵇ²_`, umbrella, `wf-<ᵇ²`). All wired into `All.agda` +
+pinned in `Ordinal/Buchholz/Smoke.agda`.
+
+*Plan for the next Claude.* The doubled-ladder programme is closed.
+Genuinely-open ordinal-track frontier (separate, larger scope):
+(1) unbudgeted `_<ᵇʳᶠ_` global WF — eliminate the ℕ budget from
+`wf-<ᵇʳᶠᵇ` under `--safe --without-K`; (2) the single-ladder Gate 1
+`<ᵇ-+1` cross-head rank-equal sub-case, IF one wants it closed on the
+ORIGINAL `rank-pow`/union umbrella rather than via the doubled
+ladder (the doubled ladder already closes `<ᵇ-+1` on its own carrier);
+(3) Pillar E paper `[EXPAND]` ordinal consumer-evidence appendix,
+gated on the Bachmann–Howard milestone. DO NOT reopen: the doubled
+ladder design (rank2/double/the 12 primitives/the `_<ᵇ²_` carrier
+shape are correct); the honest-scope verdict above; the `<ᵇ-+ψ`
+leading-power formulation.
+
+### Session arc 2026-06-13 Deniability track — EchoDeniability + wiki
 
 *Where we started:* user pasted `Deniability.agda` (standalone exploration: perfect
 deniability via constant production, `refl` proof) and asked for a `DeniabilityPartial.agda`

Fidelity-OPEN-postulates.md

@@ -0,0 +1,63 @@
+<!--
+SPDX-License-Identifier: MPL-2.0
+SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+-->
+
+# Fidelity — open postulates (trust boundaries)
+
+Companion to `proofs/agda/Ordinal/Buchholz/Fidelity.agda`. Open problem
+**`D-2026-06-14`** (`docs/echo-types/decisions/ordinal-bh-order-type-fidelity-open.adoc`).
+
+## Plain-language summary
+
+**What is now mechanised.** Only the *shape* of the order-type
+fidelity claim, plus one genuinely-proved structural fact:
+
+- The **theorem shape** is typed and auditable: `Fidelity.agda` states
+  "the sound carrier `_<ᵇ²_` (on well-formed terms `WfBT`) has order
+  type ψ₀(Ω_ω)" as a cofinal order-embedding into a Bachmann–Howard
+  structure (`OrderTypeBH`, assembled in `fidelity`). The statement is
+  quantified over the **sound carrier only** — never native `_<ᵇ_`.
+- The **lower-bound half** (`fidelity-lower`) is a real term *given the
+  postulated denotation*: the BH height is attained by the well-formed
+  carrier term `BH = ψ₀(Ω_ω)` itself (it plumbs `BH`, `BH-wf`, and the
+  denotation's `pins-BH` field — no postulate of its own).
+- The **grammar-level upper shadow** (`marker-≤ω`, `markers-≤ω`) is
+  proved **for real, postulate-free**: every Ω-marker in any Buchholz
+  term is `≤Ω ω` (the carrier lives in the ν ≤ ω fragment; the notation
+  never names a marker above Ω_ω). This is the structural precondition
+  of the upper bound, *not* the upper bound itself.
+
+**What remains genuinely open.** The two pieces of real content — the
+**order-reflecting, height-preserving denotation** `⟦·⟧` and its
+**cofinality** — are postulated, together with the existence of a
+checked Bachmann–Howard target structure. These are the missing
+*objects*, not missing *plumbing*.
+
+**Explicit non-claim.** *Nothing in this module asserts that order type
+ψ₀(Ω_ω) is proven.* `fidelity` is only as strong as the three
+postulates below; with them open, it asserts the **shape** of fidelity,
+not fidelity. `rank2` (the height-collapsing termination measure) is
+**not** reused, extended, or tightened toward this claim — fidelity
+needs the separate, height-preserving `⟦·⟧`. The status surfaces
+(appendix, decision log, roadmap) continue to read **"written at WF
+milestone; order-type fidelity OPEN"** and were *not* edited by this
+commit.
+
+## The postulates (complete list — `grep postulate Fidelity.agda`)
+
+| # | Name | Statement (in words) | What closes it | Owner |
+|---|------|----------------------|----------------|-------|
+| 1 | `bh-notation : BHNotation` | A checked well-founded strict order `(𝒪, _<𝒪_)` with a distinguished element `bh-height` whose initial segment is the Bachmann–Howard ordinal ψ₀(Ω_ω). | Construct (or import) a verified Bachmann–Howard ordinal structure in Agda — e.g. a checked ordinal-notation library, or a Cantor/Veblen normal-form development carried to ψ₀(Ω_ω). | **External mathematics** (owner / external) |
+| 2 | `denotation : DenotesBH bh-notation` | A denotation `⟦·⟧ : BT → 𝒪` that is **order-preserving** (`s <ᵇ² t → ⟦s⟧ <𝒪 ⟦t⟧`), **order-reflecting** (`⟦s⟧ <𝒪 ⟦t⟧ → s <ᵇ² t`), **cofinal** (image unbounded in `𝒪`), and **pins BH** (`⟦BH⟧ ≡ bh-height`). The height-preserving embedding `rank2` is *not*. | Define `⟦·⟧` mapping each ψ_ν / Ω_ν / + to its genuine ordinal height (not the collapsed ω-power blocks of `rank2`) and prove the four fields. This is the core order-type-correctness work (a denotational semantics for the notation faithful to `_<ᵇ²_`). | **External mathematics** (owner / external); the design route is option (a) in `D-2026-06-14`. |
+| 3 | `ordinal-upper-bound : ∀ {t} → WfBT t → ¬ (bh-height <𝒪 ⟦ t ⟧)` | No well-formed carrier term denotes strictly above the BH height (the ⟦·⟧-level upper half of the sandwich). | Cheap *given* postulate #2: combine the real `markers-≤ω` (every marker `≤Ω ω`) with a height calculation through the real `⟦·⟧` (markers `≤ ω` ⇒ denotation `≤ ψ₀(Ω_ω)`). It is postulated only because it quantifies over the not-yet-real `⟦·⟧`; it is **not** independent external mathematics beyond #2. | Discharged alongside / just after #2 (in-repo, once `⟦·⟧` is real). |
+
+## Discharge order
+
+`bh-notation` (#1) and `denotation` (#2) are the genuine external
+content and are independent of each other only up to #2 referencing
+#1's `𝒪`. `ordinal-upper-bound` (#3) is downstream of #2 and in-repo
+once #2 lands. When all three are real, `fidelity : OrderTypeBH`
+becomes an unconditional theorem and a **human** may then update the
+appendix / decision-log / roadmap from "OPEN" to discharged — per the
+hard rule, this commit does not pre-empt that sign-off.