Merge branch 'main' into claude/ecstatic-wright-OBEvx

Author: hyperpolymath

.machine_readable/agent_instructions/README.adoc

@@ -1,5 +1,5 @@
 // SPDX-License-Identifier: MPL-2.0
-// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <6759885+hyperpolymath@users.noreply.github.com>
+// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 = Agent Instructions (echo-types)
 :toc: preamble
 

.machine_readable/agent_instructions/coverage.a2ml

@@ -1,5 +1,5 @@
 # SPDX-License-Identifier: MPL-2.0
-# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <6759885+hyperpolymath@users.noreply.github.com>
+# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 #
 # coverage.a2ml — Session coverage tracking (echo-types)
 # Updated at the end of each AI agent session.

.machine_readable/agent_instructions/debt.a2ml

@@ -1,5 +1,5 @@
 # SPDX-License-Identifier: MPL-2.0
-# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <6759885+hyperpolymath@users.noreply.github.com>
+# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 #
 # debt.a2ml — Meander debt list (echo-types)
 # Proof obligations and chores found but not discharged. Carried between

.machine_readable/agent_instructions/methodology.a2ml

@@ -1,5 +1,5 @@
 # SPDX-License-Identifier: MPL-2.0
-# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <6759885+hyperpolymath@users.noreply.github.com>
+# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 #
 # methodology.a2ml — AI agent methodology configuration (echo-types)
 # Declares how agents should approach work in this Agda proof library.

.machine_readable/anchors/ANCHOR.a2ml

@@ -1,5 +1,5 @@
 # SPDX-License-Identifier: MPL-2.0
-# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <6759885+hyperpolymath@users.noreply.github.com>
+# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 #
 # ANCHOR.a2ml - authoritative anchor for the echo-types repository.
 # Canonical identity + policy boundaries for downstream/satellite repos.

.machine_readable/svc/k9/methodology-guard.k9.ncl

@@ -1,5 +1,5 @@
 # SPDX-License-Identifier: MPL-2.0
-# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <6759885+hyperpolymath@users.noreply.github.com>
+# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 #
 # K9 Validator: Methodology Guard (echo-types)
 # Checks that agent work respects the methodology constraints declared in

AFFIRMATION.adoc

@@ -27,12 +27,19 @@ fidelity claim, plus one genuinely-proved structural fact:
   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.
+- The **target structure** `(𝒪, _<𝒪_, wf-<𝒪)` is now **real,
+  postulate-free** (2026-06-15): `Ordinal.Buchholz.BHTarget` constructs
+  it from the Brouwer order (`Ord` / `_<′_` / `wf-<′`) via
+  `bh-notation-from`, inside the `--safe` kernel (wired into `All.agda`,
+  pinned in `Ordinal/Buchholz/Smoke.agda`). Only the candidate BH
+  *height* remains a free input — an explicit `Fidelity.AtHeight`
+  module parameter.
 
 **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*.
+**cofinality** — are postulated. (The checked Bachmann–Howard target
+*structure* is no longer assumed — see the last bullet above.) 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
@@ -46,18 +53,25 @@ commit.
 
 ## The postulates (complete list — `grep postulate Fidelity.agda`)
 
+As of 2026-06-15 there are **two** (reduced from three). The former
+`bh-notation` postulate is **discharged**: the target structure is now
+constructed for real in the `--safe` module `Ordinal.Buchholz.BHTarget`
+(`bh-notation-from` over the Brouwer order `Ord` / `_<′_` / `wf-<′`), and
+the candidate BH height is an explicit `Fidelity.AtHeight` module
+parameter rather than an axiom.
+
 | # | 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). |
+| 1 | `denotation : DenotesBH bh-notation` | A denotation `⟦·⟧ : BT → 𝒪` (with `𝒪 = Ord`, `_<𝒪_ = _<′_`) that is **order-preserving** (`s <ᵇ² t → ⟦s⟧ <′ ⟦t⟧`), **order-reflecting** (`⟦s⟧ <′ ⟦t⟧ → s <ᵇ² t`), **cofinal** (image unbounded in `Ord`), 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`. |
+| 2 | `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 #1: 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 #1. | Discharged alongside / just after #1 (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.
+`denotation` (#1) is the genuine external content — the faithful
+height-preserving embedding into the now-real Brouwer target.
+`ordinal-upper-bound` (#2) is downstream of #1 and in-repo once #1
+lands. When both are real, `fidelity : OrderTypeBH` becomes an
+unconditional theorem (for the supplied `AtHeight` height) 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.

Fidelity-OPEN-postulates.md

@@ -164,6 +164,14 @@ in the Pillar F4 template style.
   INJ ⇒ projection-unique; SURJ ⇒ every fibre inhabited; CONST ⇒
   section from the entire domain. K-free skeletons across all four.
   `proofs/agda/EchoLossTaxonomy.agda`.
+* *Displayed-type packaging* `[REAL]` — `Displayed` / `DispHom` /
+  `idDispHom` / `fromHomOver`: the displayed-type / fibration packaging
+  of the categorical base, a faithful Agda mirror of typed-wasm's Idris
+  `Echo.idr`, with four closed laws (identity displayed morphism acts
+  as identity; `fromHomOver` well-defined = `map-over` by construction;
+  compatibility with `map-over-id` and `map-over-comp`). Purely the
+  fibration packaging — no variance / graded-comonad / universal-property
+  claim (R-2026-05-18). `proofs/agda/EchoDisplayed.agda`.
 * *Residue taxonomy* (residue-side) — `record ResidueForm f R`
   packaging the per-output residue carrier + lowering shared by the
   eight decoration modules. Eight instances (as of 2026-05-28):

docs/echo-types/MAP.adoc

@@ -65,13 +65,16 @@ kernel** — the boundary is real and lives outside this core.
   `EchoFiberBridge`, `EchoFiberCount`, `EchoFiberTriangulation`,
   `EchoIndexed`, `EchoRelational`, `EchoTruncation`,
   `EchoJanusBridge`, `EchoTropical`, `EchoSeparating`,
-  `EchoTotalCompletion`
+  `EchoTotalCompletion`, `EchoDisplayed`
 | One hop off the kernel. `EchoJanusBridge`/`EchoTropical` are
   *Directions* (see MAP). `EchoFiberTriangulation` is the external
   stdlib triangulation hardening item. `EchoSeparating` carries
   retracted prose framing (below). `EchoTotalCompletion` is the
   `A ↔ Σ Echo` encode/decode pair anchoring the F5 canonical-
-  identity cohort (Tier 2 below).
+  identity cohort (Tier 2 below). `EchoDisplayed` is the
+  displayed-type / `DispHom` / `fromHomOver` fibration packaging of
+  the categorical base (faithful mirror of typed-wasm's Idris
+  `Echo.idr`; no variance / graded-comonad claim, per R-2026-05-18).
 
 | *Derived — Tier 2* +
 (depend on Tier-1 `Echo*`)