docs(state): refresh 6a2 STATE/META to current ordinal-track reality

claude · hyperpolymath · commit 01271d997086 · 2026-06-05T15:54:03.000+01:00
Reframe STATE.a2ml away from the narrow EI-2 termination identity (last-updated ~2026-04-29) to current reality (2026-06-05). The primary landed workstream is now the Buchholz/Ordinal rank-mono + well-foundedness track (Slice 3+4 Route A arc, PRs #165-#171/#178): RankMonoUnion._<ᵇᵘ_ umbrella, its WfCNF wrap (#169), and well-foundedness wf-<ᵇᵘ via rank-embedding transport (#170, Gate 2). Add the ephapax L3 bridge (EchoEphapaxBridge.agda, #161-#163) and arghda-core subtree extraction (#160) as supporting work. EI-2 preserved as history, not document identity. version-target left at 0.1.1 (CHANGELOG still [Unreleased]; no new tag minted). META.a2ml: bump last-updated to 2026-06-05; add adr-010 (ordinal-track WF via rank-embedding transport) and adr-011 (ephapax NARROW-stub bridge). Source of truth: CHANGELOG.md + git log. SPDX MPL-2.0 headers preserved. https://claude.ai/code/session_01BwV2DWsjkBiNP3oscimMLV
diff --git a/.machine_readable/6a2/META.a2ml b/.machine_readable/6a2/META.a2ml
@@ -6,6 +6,8 @@
 ;;; Schema reference:
 ;;;   github.com/hyperpolymath/standards/blob/main/meta-a2ml/spec/abnf/meta.abnf
 ;;;
+;;; last-updated: 2026-06-05
+;;;
 ;;; SPDX-License-Identifier: MPL-2.0
 ;;; SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell
 
@@ -98,6 +100,28 @@
      (context . "R-2026-05-18 retracted five claims and reframed the project around what the Agda actually shows (thin-poset reindexing modality, not graded comonad; pointwise mediator, not terminal cone; carrier-parametricity, not model-independence; postulate-free build as evidence, not conservativity metatheorem; no funext anywhere, not 'quarantined'). The earn-back plan in docs/echo-types/earn-back-plan.adoc was the falsifiable program for converting the retracted claims back into theorems — or confirming, on the project's own gate discipline, that they cannot be earned at their original strength.")
      (decision . "All four gates have now passed at the strictly-bounded strength the earn-back plan asked for: F4 (terminal-cone UP as a function of an explicit funext parameter, never a postulate); F2 (genuine second model of the bare Echo functor on a non-graph StepND relation); F1 (genuine graded comonad on iterated-residue carrier with Echo as grade-unit object); F3 (the F1 construction is instantiable at non-isomorphic grade monoids). Each is exactly as strong as the gate specified; nothing is overclaimed. The conservativity metatheorem retraction (R-2026-05-18 finding 5) stays retracted with no gate attempting to earn it back — that one was a meta-statement over all propositions, not discharged by typechecking. The 'not two models for EchoGraded/GCLaws' finding 3 also stays retracted; the F3 earn-back is about the different F1 interface.")
      (consequences . "The retraction discipline is validated AS A METHODOLOGY: a retraction is not a failure but the mechanism by which claims become falsifiable. Four of five retracted claims were earned back at honest strength, one stays retracted, none was silently re-inflated. paper.adoc / types-abstract.adoc / conservativity.adoc are NOT moved by this ADR — those documents are about EchoGraded's thin-poset structure, which the F1+F3 side-construction does not change. Whether to add a bounded 'new contribution' paragraph is owner-gated.")
+     (supersedes . none))
+
+    (adr-010
+     (title . "Ordinal-track well-foundedness via rank-embedding transport")
+     (status . accepted)
+     (date . "2026-05-30")
+     (context . "Lane 3 (Buchholz/Ordinal) needed well-foundedness of the rank-mono union relation _<ᵇᵘ_ (= _<ᵇ¹_ ⊎ _<ᵇ⁺²_) under the WfCNF restriction. Proving WellFounded directly on a Buchholz term relation is hard; the unbudgeted global WF for the unrestricted surface route remains genuinely out of reach under --safe --without-K.")
+     (decision . "Derive WellFounded _<ᵇᵘ_ by TRANSPORTING well-foundedness along the rank embedding rank-pow : BT → Ord, rather than by direct structural well-founded recursion. RankMonoUnionWF.wf-<ᵇᵘ composes stdlib's Induction.WellFounded Subrelation.wellFounded + On.wellFounded against wf-<′ (well-foundedness of the Brouwer-ordinal order _<′_). The union umbrella RankMonoUnion._<ᵇᵘ_ is built from source-rule extensions via Sum + [_,_] mediator (PR #168) so that new source-rule extensions ship as separate modules and union in with two mechanical edits, with the WfCNF wrap (RankMonoUnionWfCNF._<ᵇᵘⁿ_, PR #169) propagating automatically.")
+     (consequences . "Gate 2 (well-foundedness of the union) CLOSED in PR #170 under --safe --without-K with zero new postulates. Gate 1 (tail-rank-equality discharge for the cross-head rank-equal case) stays OPEN — a structural blocker whose two pre-identified unblock routes were CHECKED-REFUTED in PR #146. Gate 3 (further source-rule extensions, Path-4+) stays OPEN but mechanical via the documented union recipe. The rank-embedding transport is the architectural pattern future source-rule extensions inherit.")
+     (modules . ("proofs/agda/Ordinal/Buchholz/RankMonoUnion.agda"
+                 "proofs/agda/Ordinal/Buchholz/RankMonoUnionWfCNF.agda"
+                 "proofs/agda/Ordinal/Buchholz/RankMonoUnionWF.agda"))
+     (supersedes . none))
+
+    (adr-011
+     (title . "echo↔ephapax cross-repo bridge as a NARROW definitional stub")
+     (status . accepted)
+     (date . "2026-05-30")
+     (context . "The hyperpolymath ecosystem wanted a named correspondence between echo-types' L3 layer (weaken : LEcho linear → LEcho affine; no-section-collapse-to-residue) and ephapax-affine's L3 layer. A full mechanised bridge across all of ephapax-affine's layers (L1/L2/L4) would be a large, speculative undertaking.")
+     (decision . "Ship proofs/agda/EchoEphapaxBridge.agda as a NARROW stub: two definitional refl-renames plus a docstring catalogue (ephapax-L3-weaken, ephapax-L3-no-section-collapse). Honest scope is L3 ONLY; ephapax-affine itself and L1/L2/L4 are explicitly NOT mirrored. Package layout documented in docs/bridges/EchoBridges.md.")
+     (consequences . "Closes echo-types#126. Establishes the bridge naming convention without overclaiming a deep correspondence. Extending to further ephapax layers is separate future work, not unfinished bridge business. Landed across PRs #161/#162/#163.")
+     (module . "proofs/agda/EchoEphapaxBridge.agda")
      (supersedes . none))))
 
 ;;; ============================================================
diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml
@@ -1,5 +1,5 @@
 ;;; ============================================================
-;;; STATE.a2ml — echo-types EI-2 termination capture
+;;; STATE.a2ml — echo-types project state
 ;;; ============================================================
 ;;;
 ;;; Format: state-a2ml (S-expression, SRFI-30 conventions)
@@ -8,15 +8,21 @@
 ;;; Sibling reference (cached pattern):
 ;;;   github.com/hyperpolymath/standards/blob/main/meta-a2ml/spec/abnf/meta.abnf
 ;;;
-;;; Purpose: prevent EI-2 from being re-investigated. The investigation
-;;; concluded; the verdict is negative; the documentation cascade has been
-;;; applied; the recipe is no longer a candidate locus of distinctness.
+;;; last-updated: 2026-06-05
+;;;
+;;; Purpose: machine-readable current project state. The PRIMARY landed
+;;; workstream is now the Buchholz/Ordinal rank-monotonicity +
+;;; well-foundedness track (Slice 3+4 Route A arc). The EI-2 termination
+;;; capture (April 2026) is preserved below as history — it prevents
+;;; EI-2 from being re-investigated, but it is no longer the whole
+;;; document identity.
 ;;;
 ;;; SPDX-License-Identifier: MPL-2.0
 ;;; SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell
 
-(define-module (echo-types ei-2 state)
+(define-module (echo-types state)
   #:export (project
+            current-workstream
             session
             terminated-questions
             standing-decisions
@@ -35,12 +41,74 @@
     (repository     . "github.com/hyperpolymath/echo-types")
     (canonical-host . github)                ; per current forge workflow
     (mirrors        . (gitlab codeberg))
-    (version-target . "0.1.1")
+    (version-target . "0.1.1")               ; CHANGELOG still [Unreleased] over
+                                             ; [0.1.0+integration-pending]; no new
+                                             ; release tag minted as of 2026-06-05
     (license        . "MPL-2.0")))
 
 ;;; ============================================================
-;;; Session header
+;;; Current workstream (primary landed work as of 2026-06-05)
+;;; ============================================================
+;;;
+;;; The active centre of gravity is the Lane 3 ordinal track. The April
+;;; 2026 EI-2 closure (recorded below under `session` /
+;;; `terminated-questions`) remains valid history but is no longer the
+;;; live work. Source of truth for the entries below: CHANGELOG.md
+;;; (current to 2026-05-30) + git log.
+
+(define current-workstream
+  '((as-of . "2026-06-05")
+    (primary
+     ((id . ordinal-rank-mono-wf)
+      (title . "Buchholz/Ordinal rank-monotonicity + well-foundedness — Slice 3+4 Route A arc")
+      (status . landed)
+      (date-range . "2026-05-30")
+      (prs . (#165 #166 #167 #168 #169 #170 #171))
+      (summary . "Rank-mono union umbrella over source-rule extensions. RankMonoUnion._<ᵇᵘ_ = _<ᵇ¹_ ⊎ _<ᵇ⁺²_ via Sum + [_,_] mediator (#168); RankMonoUnionWfCNF._<ᵇᵘⁿ_ bundles the canonical-form invariant alongside the rank-relation (#169 WfCNF wrap); RankMonoUnionWF.wf-<ᵇᵘ derives WellFounded _<ᵇᵘ_ via Subrelation.wellFounded + On.wellFounded rank-embedding transport from wf-<′ (#170, Gate 2 of the arc closed). Path-3 prototype RankMonoSameLeft._<ᵇ⁺²_ adds a literal-same-left source-rule extension closing in one line via rank-pow-bplus-right-mono (#167).")
+      (modules
+       . ("proofs/agda/Ordinal/Buchholz/RankMonoUnion.agda"
+          "proofs/agda/Ordinal/Buchholz/RankMonoUnionWfCNF.agda"
+          "proofs/agda/Ordinal/Buchholz/RankMonoUnionWF.agda"))
+      (gates
+       ((gate-1 . "tail-rank-equality discharge for cross-head rank-equal case — OPEN (structural blocker; both pre-identified unblock routes CHECKED-REFUTED in PR #146)")
+        (gate-2 . "well-foundedness of the union — CLOSED in #170")
+        (gate-3 . "Path-4+ further source-rule extensions — OPEN but mechanical via the documented recipe")))
+      (invariants . "163 modules at arc close; all --safe --without-K; zero new postulates; no funext.")))
+    (supporting
+     (((id . ephapax-bridge)
+       (title . "Cross-repo echo↔ephapax L3 bridge — EchoEphapaxBridge.agda NARROW stub")
+       (status . landed)
+       (date . "2026-05-30")
+       (prs . (#161 #162 #163))
+       (module . "proofs/agda/EchoEphapaxBridge.agda")
+       (summary . "Two definitional refl-renames + a docstring catalogue (ephapax-L3-weaken, ephapax-L3-no-section-collapse) establishing the named correspondence between echo-types L3 (weaken : LEcho linear → LEcho affine; no-section-collapse-to-residue) and ephapax-affine's L3 layer. Honest scope: L3 ONLY; ephapax-affine + L1/L2/L4 NOT mirrored. Closes #126. Package layout in docs/bridges/EchoBridges.md.")
+       (note . "NARROW-stub by design — definitional renames + catalogue, not a deep mechanised bridge."))
+      ((id . arghda-core-extraction)
+       (title . "arghda-core subtree extraction")
+       (status . landed)
+       (date . "2026-05-30")
+       (pr . #160)
+       (summary . "Removed arghda-core/ from this repo's tree; it now lives as a standalone repo (hyperpolymath/arghda-core) per the umbrella in #159. Reduces echo-types' surface area to the propositional/proof-theoretic core.")
+       (umbrella-issue . 159))))
+    (proof-debt
+     ((status . enumerated)
+      (pr . #172)
+      (doc . "docs/proof-debt.md")
+      (summary . "echo-types' sole soundness-relevant escape hatch — the four propositional-truncation postulates in proofs/agda/EchoImageFactorizationPropPostulated.agda — enumerated under Disposition (c) NECESSARY AXIOM. Clears the recurring governance/Trusted-base-reduction-policy red check (standards#211).")))
+    (recent-ci
+     ((id . hypatia-hardening)
+      (pr . #178)
+      (date . "2026-05-30")
+      (summary . "Hardened CI workflows + resolved Hypatia findings at source. Most recent commit on the branch as of this state refresh.")))))
+
+;;; ============================================================
+;;; Session header (HISTORICAL — EI-2 termination, April 2026)
 ;;; ============================================================
+;;;
+;;; The EI-2 record below is retained as history. EI-2 closed negatively
+;;; in April 2026; it must not be re-investigated (see do-not-redo and
+;;; forbidden-rebrandings). It is NOT the current workstream — see
+;;; `current-workstream` above for the live ordinal-track work.
 
 (define session
   '((investigation-id   . "EI-2")
@@ -269,10 +337,10 @@
 
     ((id . ordinal-track-path-1)
      (title . "Ordinal track Path-1 — Brouwer rank-mono into _<ᵇ⁻_")
-     (status . in-flight)
-     (relevance . "Brouwer arithmetic + rank-mono for _<ᵇ⁻_ are in a parallel-session worktree; this echo-types session stays clear of `proofs/agda/Ordinal/**` per `feedback_parallel_session_branch_drift` discipline.")
+     (status . substantially-landed)
+     (relevance . "Substantially advanced by the Slice 3+4 Route A arc (PRs #165-#171, 2026-05-30) — see current-workstream. The rank-mono union umbrella RankMonoUnion._<ᵇᵘ_ + its WfCNF wrap landed, and well-foundedness wf-<ᵇᵘ via rank-embedding transport closed Gate 2 (#170).")
      (priority . high)
-     (owner . other-session))
+     (remaining . "Gate 1 (tail-rank-equality discharge for the cross-head rank-equal case) remains OPEN — structural blocker, both pre-identified unblock routes CHECKED-REFUTED in PR #146. Gate 3 (Path-4+ further source-rule extensions) is OPEN but mechanical via the documented recipe."))
 
     ((id . v0-2-recipe-extension)
      (title . "Recipe extension exploration (parked)")
