proof(ordinal): reduce Fidelity trust boundary 3→2 — construct BH target in --safe kernel

Build the Bachmann–Howard order-type target structure for real instead of postulating it. New --safe --without-K module Ordinal.Buchholz.BHTarget defines the BHNotation interface plus a postulate-free bh-notation-from : Ord → BHNotation wiring the repo's existing Brouwer order (Ord / _<′_ / wf-<′). The target order AND its well-foundedness are now proved, not assumed.

Fidelity.agda is refactored to consume BHTarget and take the candidate BH height as an explicit module parameter (AtHeight) rather than an opaque whole-structure postulate. This drops Fidelity's postulate count from three to two (denotation, ordinal-upper-bound). Order-type fidelity ITSELF remains OPEN (D-2026-06-14) — a trust-boundary reduction, not a discharge of the milestone.

Wired BHTarget into All.agda + Ordinal/Buchholz/Smoke.agda; updated docs/proof-debt.md (a)+(d) and Fidelity-OPEN-postulates.md. Verified: agda All.agda + Fidelity.agda exit 0; check-guardrails (189 modules) + kernel-guard both PASS.

https://claude.ai/code/session_01GJatEm2TVFSTBEkKXmserJ

Author: claude

Fidelity-OPEN-postulates.md

@@ -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.

docs/proof-debt.md

@@ -19,6 +19,20 @@ under one of (a) discharged / (b) budgeted / (c) necessary axiom / (d) debt.
   `prop-factor-left-mere-surjective` (epi). This realises the axiom
   the `--without-K` demo under (c) only assumes — see (c).
 
+- **Bachmann–Howard target structure (`BHNotation` + its
+  well-foundedness)** — discharged 2026-06-15 in the `--safe --without-K`
+  kernel by `proofs/agda/Ordinal/Buchholz/BHTarget.agda` (zero
+  postulates; wired into `All.agda`, pinned in
+  `Ordinal/Buchholz/Smoke.agda`). The abstract `BHNotation` interface and
+  a concrete `bh-notation-from : Ord → BHNotation` are CONSTRUCTED from
+  the repo's existing Brouwer order (`Ord` / `_<′_` / `wf-<′`), so the
+  fidelity target's order AND its well-foundedness are now proved, not
+  assumed. This reduces the order-type fidelity trust boundary under (d)
+  from three postulates to two; the candidate BH HEIGHT (which `Ord`
+  value is ψ₀(Ω_ω)) is now an explicit module parameter
+  (`Fidelity.AtHeight`), not a postulate. Order-type fidelity ITSELF
+  remains OPEN — see (d).
+
 ## (b) Budgeted — tested with refutation budget
 
 - (none)
@@ -52,30 +66,39 @@ under one of (a) discharged / (b) budgeted / (c) necessary axiom / (d) debt.
 
 ## (d) DEBT — actively to be closed
 
-- `proofs/agda/Ordinal/Buchholz/Fidelity.agda` — three top-level
-  `postulate`s forming the trust boundary of the **order-type fidelity
-  scaffold** (open problem `D-2026-06-14`,
+- `proofs/agda/Ordinal/Buchholz/Fidelity.agda` — **two** top-level
+  `postulate`s (reduced from three on 2026-06-15; see (a)) forming the
+  trust boundary of the **order-type fidelity scaffold** (open problem
+  `D-2026-06-14`,
   `docs/echo-types/decisions/ordinal-bh-order-type-fidelity-open.adoc`):
-  - `bh-notation` — assumed checked Bachmann–Howard order structure.
   - `denotation` — assumed faithful, height-preserving order-embedding
-    `⟦·⟧ : BT → 𝒪` (the missing object; **not** `rank2`, which
-    deliberately collapses heights and is a termination measure only).
+    `⟦·⟧ : BT → 𝒪` into the (now-real) Brouwer target (the missing
+    object; **not** `rank2`, which deliberately collapses heights and is
+    a termination measure only).
   - `ordinal-upper-bound` — the `⟦·⟧`-level upper half of the sandwich
     (downstream of `denotation`).
+  - **Discharged (2026-06-15)**: the former `bh-notation` postulate (an
+    opaque whole BH structure) is gone — the `BHNotation` interface and a
+    real `bh-notation-from` instance now live in the `--safe` kernel
+    module `Ordinal.Buchholz.BHTarget`, so the target order and its
+    well-foundedness (Brouwer `_<′_` / `wf-<′`) are proved, not assumed.
+    The candidate BH height is an explicit parameter to
+    `Fidelity.AtHeight`, not a postulate. See (a).
   - **Classification**: DEBT, to be discharged when order-type fidelity
     is proved — these are *not* permanently-accepted axioms. Each is
     annotated inline with an `AXIOM:` leading comment.
   - **Justification / scope**: the module is quarantined — `--without-K`
     only, NOT imported by `All.agda` / `Smoke.agda` — so the `--safe`
-    kernel cone depends on none of these. Nothing in the module asserts
-    that order type ψ₀(Ω_ω) is *proven*; the status surfaces (appendix,
-    decision log, roadmap) read "written at WF milestone; order-type
-    fidelity OPEN".
+    kernel cone depends on neither postulate. Nothing in the module
+    asserts that order type ψ₀(Ω_ω) is *proven*; the status surfaces
+    (appendix, decision log, roadmap) read "written at WF milestone;
+    order-type fidelity OPEN".
   - **Citation**: `D-2026-06-14`; full per-postulate spec (statement /
     what closes it / owner) in `Fidelity-OPEN-postulates.md`.
   - **Guardrail status**: allow-listed in `tools/check-guardrails.sh`
     (`EXPLORATORY_EXEMPT`) and the inline `hypatia: allow` pragma at the
-    module head.
+    module head. (`BHTarget` is NOT exempt — it is real kernel content
+    and passes the guardrail.)
 
 ## Notes
 

proofs/agda/All.agda

@@ -159,6 +159,7 @@ open import Ordinal.Buchholz.RankDoubledLadderMonoPlus
 open import Ordinal.Buchholz.RankDoubledLadderAddPrincipal
 open import Ordinal.Buchholz.RankDoubledLadderMonoPlus2
 open import Ordinal.Buchholz.RankDoubledLadderUmbrella
+open import Ordinal.Buchholz.BHTarget
 open import Ordinal.Buchholz.RankMonoUmbrella
 open import Ordinal.Buchholz.RankMonoUmbrellaSlice3
 open import Ordinal.Buchholz.RankMonoUmbrellaSlice4

proofs/agda/Ordinal/Buchholz/BHTarget.agda

@@ -0,0 +1,81 @@
+{-# OPTIONS --safe --without-K #-}
+-- SPDX-License-Identifier: MPL-2.0
+-- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+
+-- Bachmann–Howard TARGET STRUCTURE — the real, postulate-free part of
+-- the order-type fidelity target (open problem D-2026-06-14). 2026-06-15.
+--
+-- ## What this module IS
+--
+-- The `BHNotation` interface (an abstract well-founded strict order with
+-- a distinguished element) TOGETHER WITH a concrete, postulate-free
+-- constructor `bh-notation-from` that builds a genuine instance from the
+-- repo's existing Brouwer ordinal order:
+--
+--   𝒪         := Ord                (Ordinal.Brouwer)
+--   _<𝒪_      := _<′_               (Ordinal.Brouwer.Phase13)
+--   wf-<𝒪     := wf-<′              (PROVED, postulate-free, --safe)
+--   bh-height := the supplied Ord   (the only free choice)
+--
+-- ## Why this matters (trust-boundary reduction)
+--
+-- `Fidelity.agda` previously postulated the WHOLE `bh-notation :
+-- BHNotation` opaquely — assuming a Set, an order, ITS WELL-FOUNDEDNESS,
+-- and a distinguished element. This module discharges three of those
+-- four obligations FOR REAL inside the --safe kernel: the target order
+-- and its well-foundedness are now the genuine Brouwer `_<′_` / `wf-<′`,
+-- not assumptions. Only the distinguished `bh-height` (i.e. WHICH `Ord`
+-- value is ψ₀(Ω_ω)) remains a free input — handed to `Fidelity` as an
+-- explicit module parameter, with its ψ₀(Ω_ω)-meaning pinned downstream
+-- by the (still-open) `denotation.pins-BH` field, not by fiat. See
+-- Fidelity-OPEN-postulates.md.
+--
+-- ## What this module is NOT
+--
+--   * It does NOT claim the Brouwer order `_<′_` HAS order type ψ₀(Ω_ω),
+--     nor that any particular `Ord` value IS ψ₀(Ω_ω). Brouwer ordinals
+--     reach far past ψ₀(Ω_ω); identifying the right value and proving the
+--     initial-segment order type is exactly the faithful `denotation`
+--     work that remains OPEN (D-2026-06-14).
+--   * It does NOT reuse `rank2`. The faithful denotation must be
+--     height-preserving; `rank2` collapses heights. `bh-notation-from`
+--     fixes only the ORDER, not the embedding, so it does not prejudge
+--     `denotation`.
+
+module Ordinal.Buchholz.BHTarget where
+
+open import Induction.WellFounded using (WellFounded)
+
+open import Ordinal.Brouwer using (Ord)
+open import Ordinal.Brouwer.Phase13 using (_<′_; wf-<′)
+
+----------------------------------------------------------------------
+-- The Bachmann–Howard target INTERFACE
+----------------------------------------------------------------------
+
+-- An abstract well-founded strict order with a distinguished element
+-- `bh-height` standing for the order type ψ₀(Ω_ω). (Whether a given
+-- instance's `bh-height` REALLY has that initial segment is the content
+-- of the fidelity embedding, not of this interface.)
+record BHNotation : Set₁ where
+  field
+    𝒪         : Set
+    _<𝒪_      : 𝒪 → 𝒪 → Set
+    wf-<𝒪     : WellFounded _<𝒪_
+    bh-height : 𝒪
+
+----------------------------------------------------------------------
+-- A concrete, postulate-free instance from the Brouwer order
+----------------------------------------------------------------------
+
+-- Given any `Ord` value as the candidate BH height, the Brouwer order
+-- `(Ord, _<′_, wf-<′)` furnishes a genuine `BHNotation`. The order and
+-- its well-foundedness are REAL (no postulate); only the height is the
+-- caller's choice.
+bh-notation-from : Ord → BHNotation
+bh-notation-from h = record
+  { 𝒪         = Ord
+  ; _<𝒪_      = _<′_
+  ; wf-<𝒪     = wf-<′
+  ; bh-height = h
+  }