|
| 1 | +{-# OPTIONS --without-K #-} |
| 2 | + |
| 3 | +-- hypatia: allow code_safety/agda_postulate -- order-type fidelity for the Buchholz notation (D-2026-06-14) is external mathematics; the three named postulates below are the explicit, documented trust boundary. This module is OUTSIDE the --safe kernel cone by design, is NOT imported by All.agda/Smoke.agda, and asserts NOTHING that the --safe core depends on. See Fidelity-OPEN-postulates.md. |
| 4 | + |
| 5 | +-- SPDX-License-Identifier: MPL-2.0 |
| 6 | +-- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> |
| 7 | + |
| 8 | +-- Order-type fidelity SCAFFOLD for the Bachmann–Howard milestone |
| 9 | +-- (open problem D-2026-06-14). 2026-06-14. |
| 10 | +-- |
| 11 | +-- ## What this module IS |
| 12 | +-- |
| 13 | +-- The *typed shape* of the order-type fidelity claim, with the hard |
| 14 | +-- content left as three explicitly-named `postulate`s. Its job is to |
| 15 | +-- make the absence of order-type fidelity VISIBLE and AUDITABLE — a |
| 16 | +-- `grep postulate` here returns the complete, honest list of trust |
| 17 | +-- boundaries — NOT to fabricate the proof. |
| 18 | +-- |
| 19 | +-- ## What this module is NOT (read before trusting anything here) |
| 20 | +-- |
| 21 | +-- * It does NOT prove that `_<ᵇ²_` has order type ψ₀(Ω_ω). That |
| 22 | +-- claim is OPEN (decision-log D-2026-06-14). Nothing here asserts |
| 23 | +-- it as established. |
| 24 | +-- * It does NOT touch, reuse, or "tighten" `rank2`. `rank2` is the |
| 25 | +-- deliberately HEIGHT-COLLAPSING termination measure (it maps the |
| 26 | +-- whole ν≤ω fragment below ω^(ω+2), is monotone but neither |
| 27 | +-- order-reflecting nor cofinal). It is sufficient for |
| 28 | +-- well-foundedness and USELESS for order-type fidelity. Fidelity |
| 29 | +-- needs a DIFFERENT object — the height-preserving denotation |
| 30 | +-- `⟦·⟧` postulated below — which this module never conflates with |
| 31 | +-- `rank2`. |
| 32 | +-- * It is OUTSIDE the `--safe` kernel cone (pragma `--without-K` |
| 33 | +-- only, matching `EchoImageFactorizationPropPostulated`). It is |
| 34 | +-- NOT wired into `All.agda` / `Smoke.agda`. A `--safe` module may |
| 35 | +-- not import it; the `--safe` core therefore depends on none of |
| 36 | +-- these postulates. |
| 37 | +-- |
| 38 | +-- ## The claim, quantified over the SOUND carrier only |
| 39 | +-- |
| 40 | +-- Fidelity is stated over `_<ᵇ²_` restricted to well-formed terms |
| 41 | +-- (`WfBT`) — the ordinally-sound carrier. NEVER over native `_<ᵇ_` |
| 42 | +-- (ordinally unsound; the `<ᵇ-+Ω` counterexample) nor any |
| 43 | +-- global-native surface. The same denotation extends to the |
| 44 | +-- congruence closures `_<ᵇʳᶠ²_` / `_<ᵇ⁺²_` (same carrier), but the |
| 45 | +-- order-type statement is made for `_<ᵇ²_`. |
| 46 | +-- |
| 47 | +-- ## The sandwich |
| 48 | +-- |
| 49 | +-- "order type ψ₀(Ω_ω)" is decomposed into a cofinal order-embedding |
| 50 | +-- of the sound carrier into a postulated Bachmann–Howard structure: |
| 51 | +-- |
| 52 | +-- upper half: no well-formed term denotes ABOVE the BH height |
| 53 | +-- (`ordinal-upper-bound`, ⟦·⟧-dependent ⇒ postulated; |
| 54 | +-- its grammar-level shadow `markers-≤ω` is proved for |
| 55 | +-- real below); |
| 56 | +-- lower half: the BH height IS attained, by the well-formed term |
| 57 | +-- `BH = ψ₀(Ω_ω)` itself (`fidelity-lower`, REAL given |
| 58 | +-- the postulated denotation's `pins-BH` field); |
| 59 | +-- embedding: `preserve` + `reflect` (faithfulness, from the |
| 60 | +-- postulated denotation). |
| 61 | +-- |
| 62 | +-- ## Trust boundary (grep `postulate`) |
| 63 | +-- |
| 64 | +-- * `bh-notation` — a CHECKED Bachmann–Howard order structure |
| 65 | +-- (external mathematics). |
| 66 | +-- * `denotation` — the height-preserving order-embedding |
| 67 | +-- `⟦·⟧` + its fidelity fields (the missing |
| 68 | +-- object). |
| 69 | +-- * `ordinal-upper-bound` — the ⟦·⟧-level upper bound (closable from |
| 70 | +-- `markers-≤ω` + a height calc through the |
| 71 | +-- real `⟦·⟧`, once `denotation` is real). |
| 72 | +-- |
| 73 | +-- See Fidelity-OPEN-postulates.md for each postulate's owner + what |
| 74 | +-- external mathematics discharges it. |
| 75 | + |
| 76 | +module Ordinal.Buchholz.Fidelity where |
| 77 | + |
| 78 | +open import Data.Unit using (⊤; tt) |
| 79 | +open import Data.Product using (Σ; _,_; _×_) |
| 80 | +open import Relation.Nullary using (¬_) |
| 81 | +open import Relation.Binary.PropositionalEquality using (_≡_) |
| 82 | +open import Induction.WellFounded using (WellFounded) |
| 83 | + |
| 84 | +open import Ordinal.OmegaMarkers using (OmegaIndex; fin; ω; _≤Ω_; fin≤ω; ω≤ω) |
| 85 | +open import Ordinal.Buchholz.Syntax using (BT; bzero; bOmega; bplus; bpsi) |
| 86 | +open import Ordinal.Buchholz.WellFormed using (WfBT; BH; BH-wf) |
| 87 | +open import Ordinal.Buchholz.RankDoubledLadderUmbrella using (_<ᵇ²_) |
| 88 | + |
| 89 | +---------------------------------------------------------------------- |
| 90 | +-- 1. Target-structure INTERFACE (not an implementation) |
| 91 | +---------------------------------------------------------------------- |
| 92 | + |
| 93 | +-- An abstract well-founded strict order with a distinguished element |
| 94 | +-- `bh-height` standing for the order type ψ₀(Ω_ω). The CONSTRUCTION of |
| 95 | +-- a concrete, checked instance is external mathematics — postulated |
| 96 | +-- below as the trust boundary, never built here. |
| 97 | +record BHNotation : Set₁ where |
| 98 | + field |
| 99 | + 𝒪 : Set |
| 100 | + _<𝒪_ : 𝒪 → 𝒪 → Set |
| 101 | + wf-<𝒪 : WellFounded _<𝒪_ |
| 102 | + bh-height : 𝒪 -- the element whose initial segment is ψ₀(Ω_ω) |
| 103 | + |
| 104 | +---------------------------------------------------------------------- |
| 105 | +-- 2. The denotation SPEC (interface-level; ⟦·⟧ is NOT implemented) |
| 106 | +---------------------------------------------------------------------- |
| 107 | + |
| 108 | +-- The height-preserving order-embedding the fidelity claim needs — the |
| 109 | +-- object `rank2` is NOT (rank2 collapses heights). Stated as a record |
| 110 | +-- of named fields; its inhabitant is postulated, not built. Defined |
| 111 | +-- before the top-level `open BHNotation bh-notation` so the record's |
| 112 | +-- own `open BHNotation N` is the only `𝒪` in its scope. |
| 113 | +record DenotesBH (N : BHNotation) : Set where |
| 114 | + open BHNotation N |
| 115 | + field |
| 116 | + ⟦_⟧ : BT → 𝒪 |
| 117 | + -- order-preserving (the upper-bound-supporting half) |
| 118 | + preserve : ∀ {s t} → WfBT s → WfBT t → s <ᵇ² t → ⟦ s ⟧ <𝒪 ⟦ t ⟧ |
| 119 | + -- order-reflecting (faithfulness; the lower-bound-supporting half) |
| 120 | + reflect : ∀ {s t} → WfBT s → WfBT t → ⟦ s ⟧ <𝒪 ⟦ t ⟧ → s <ᵇ² t |
| 121 | + -- cofinality: the image is unbounded in 𝒪 |
| 122 | + cofinal : (o : 𝒪) → Σ BT (λ t → WfBT t × (o <𝒪 ⟦ t ⟧)) |
| 123 | + -- the BH term denotes exactly the BH height |
| 124 | + pins-BH : ⟦ BH ⟧ ≡ bh-height |
| 125 | + |
| 126 | +-- TRUST BOUNDARY #1. Supplying a checked Bachmann–Howard structure is |
| 127 | +-- external mathematics (owner / external). This postulate is the |
| 128 | +-- assumption that such a structure exists; nothing here constructs it. |
| 129 | +postulate |
| 130 | + bh-notation : BHNotation |
| 131 | + |
| 132 | +open BHNotation bh-notation |
| 133 | + |
| 134 | +-- TRUST BOUNDARY #2. The faithful, height-preserving denotation is the |
| 135 | +-- missing object. This postulate assumes it exists; this module makes |
| 136 | +-- its absence typed, not filled. |
| 137 | +postulate |
| 138 | + denotation : DenotesBH bh-notation |
| 139 | + |
| 140 | +open DenotesBH denotation |
| 141 | + |
| 142 | +---------------------------------------------------------------------- |
| 143 | +-- 3a. The lower-bound half — REAL (plumbs the postulated `pins-BH`) |
| 144 | +---------------------------------------------------------------------- |
| 145 | + |
| 146 | +-- The BH height is attained by a well-formed carrier element, namely |
| 147 | +-- `BH = ψ₀(Ω_ω)` itself. This is a genuine term (no postulate of its |
| 148 | +-- own) — it assembles `BH`, `BH-wf`, and the `pins-BH` field of the |
| 149 | +-- postulated denotation. It does NOT independently establish fidelity; |
| 150 | +-- it is the lower half CONDITIONAL on `denotation`. |
| 151 | +fidelity-lower : Σ BT (λ t → WfBT t × (⟦ t ⟧ ≡ bh-height)) |
| 152 | +fidelity-lower = BH , (BH-wf , pins-BH) |
| 153 | + |
| 154 | +---------------------------------------------------------------------- |
| 155 | +-- 3b. The upper-bound half — ⟦·⟧-DEPENDENT ⇒ postulated |
| 156 | +---------------------------------------------------------------------- |
| 157 | + |
| 158 | +-- TRUST BOUNDARY #3. "No well-formed carrier element denotes above the |
| 159 | +-- BH height." This quantifies over the postulated `⟦·⟧`, so it cannot |
| 160 | +-- be a real term here. Its GRAMMAR-LEVEL shadow (`markers-≤ω`, §5) is |
| 161 | +-- proved for real; the step from that shadow to this ⟦·⟧-level bound |
| 162 | +-- is the height calculation through a real `⟦·⟧`, available once |
| 163 | +-- `denotation` is discharged. |
| 164 | +postulate |
| 165 | + ordinal-upper-bound : ∀ {t} → WfBT t → ¬ (bh-height <𝒪 ⟦ t ⟧) |
| 166 | + |
| 167 | +---------------------------------------------------------------------- |
| 168 | +-- 4. The sandwich theorem — STATED + assembled from the two halves |
| 169 | +---------------------------------------------------------------------- |
| 170 | + |
| 171 | +-- "_<ᵇ²_ on well-formed terms has order type ψ₀(Ω_ω)", as a cofinal |
| 172 | +-- order-embedding into `bh-notation` with the BH term pinned to the |
| 173 | +-- height. The TYPE is mechanised and auditable; the CONTENT is the |
| 174 | +-- three postulates above plus the real `fidelity-lower`. |
| 175 | +record OrderTypeBH : Set where |
| 176 | + field |
| 177 | + upper : ∀ {t} → WfBT t → ¬ (bh-height <𝒪 ⟦ t ⟧) |
| 178 | + lower : Σ BT (λ t → WfBT t × (⟦ t ⟧ ≡ bh-height)) |
| 179 | + embeds-preserve : ∀ {s t} → WfBT s → WfBT t → s <ᵇ² t → ⟦ s ⟧ <𝒪 ⟦ t ⟧ |
| 180 | + embeds-reflect : ∀ {s t} → WfBT s → WfBT t → ⟦ s ⟧ <𝒪 ⟦ t ⟧ → s <ᵇ² t |
| 181 | + |
| 182 | +-- The assembly is honest plumbing of the (postulated) parts into the |
| 183 | +-- conclusion type — NOT an independent proof. `fidelity` is only as |
| 184 | +-- strong as its three postulates; with them OPEN, this asserts the |
| 185 | +-- SHAPE of fidelity, not fidelity. |
| 186 | +fidelity : OrderTypeBH |
| 187 | +fidelity = record |
| 188 | + { upper = ordinal-upper-bound |
| 189 | + ; lower = fidelity-lower |
| 190 | + ; embeds-preserve = preserve |
| 191 | + ; embeds-reflect = reflect |
| 192 | + } |
| 193 | + |
| 194 | +---------------------------------------------------------------------- |
| 195 | +-- 5. The one thing proved FOR REAL: the grammar-level upper shadow |
| 196 | +---------------------------------------------------------------------- |
| 197 | + |
| 198 | +-- Every Ω-marker occurring in a Buchholz term is ≤Ω ω. This follows |
| 199 | +-- cheaply from the constructor shapes (OmegaIndex is exactly |
| 200 | +-- `fin n | ω`, so ω is the top). It is the honest, postulate-free |
| 201 | +-- content of "the carrier lives in the ν≤ω fragment" — i.e. the |
| 202 | +-- notation never names a marker above Ω_ω. It is the STRUCTURAL |
| 203 | +-- PRECONDITION of `ordinal-upper-bound`, NOT that ⟦·⟧-level bound |
| 204 | +-- itself (which needs the postulated denotation). |
| 205 | + |
| 206 | +AllMarkers≤ω : BT → Set |
| 207 | +AllMarkers≤ω bzero = ⊤ |
| 208 | +AllMarkers≤ω (bOmega ν) = ν ≤Ω ω |
| 209 | +AllMarkers≤ω (bplus x y) = AllMarkers≤ω x × AllMarkers≤ω y |
| 210 | +AllMarkers≤ω (bpsi ν α) = (ν ≤Ω ω) × AllMarkers≤ω α |
| 211 | + |
| 212 | +marker-≤ω : (ν : OmegaIndex) → ν ≤Ω ω |
| 213 | +marker-≤ω (fin n) = fin≤ω |
| 214 | +marker-≤ω ω = ω≤ω |
| 215 | + |
| 216 | +markers-≤ω : (t : BT) → AllMarkers≤ω t |
| 217 | +markers-≤ω bzero = tt |
| 218 | +markers-≤ω (bOmega ν) = marker-≤ω ν |
| 219 | +markers-≤ω (bplus x y) = markers-≤ω x , markers-≤ω y |
| 220 | +markers-≤ω (bpsi ν α) = marker-≤ω ν , markers-≤ω α |
0 commit comments