From c76f8bc492bc2378cb699ff5464726ca8bc15def Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Mon, 18 May 2026 10:58:05 +0100 Subject: [PATCH] =?UTF-8?q?earn-back:=20Buchholz=20ledger=20item=20B=20(K-?= =?UTF-8?q?attributed)=20=E2=80=94=20OrderExtendedDirect?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit #57 reduced to its sole content not already in main: the new module proofs/agda/Ordinal/Buchholz/OrderExtendedDirect.agda (225 lines) + Smoke pins + All.agda registration. F1/F4/F2 spikes and the doc reframes from the original branch were superseded by #54/#55/#56/#58/#60 (present in main, byte-identical) and the Nix-flake commit dropped (Guix-primary policy). Typechecks --safe --without-K, zero postulates; full All.agda + Smoke + characteristic + examples suites green. Co-Authored-By: Claude Opus 4.7 (1M context) --- proofs/agda/All.agda | 1 + .../Ordinal/Buchholz/OrderExtendedDirect.agda | 225 ++++++++++++++++++ proofs/agda/Ordinal/Buchholz/Smoke.agda | 12 + 3 files changed, 238 insertions(+) create mode 100644 proofs/agda/Ordinal/Buchholz/OrderExtendedDirect.agda diff --git a/proofs/agda/All.agda b/proofs/agda/All.agda index 6d00e4f..0ff91a6 100644 --- a/proofs/agda/All.agda +++ b/proofs/agda/All.agda @@ -79,6 +79,7 @@ open import Ordinal.Buchholz.VeblenProjectionMeasure open import Ordinal.Buchholz.VeblenComparisonTarget open import Ordinal.Buchholz.VeblenComparisonModel open import Ordinal.Buchholz.ExtendedOrder +open import Ordinal.Buchholz.OrderExtendedDirect open import Ordinal.Buchholz.LiftedExtendedOrder open import Ordinal.Buchholz.IteratedExtendedOrder open import Ordinal.Buchholz.RankBrouwer diff --git a/proofs/agda/Ordinal/Buchholz/OrderExtendedDirect.agda b/proofs/agda/Ordinal/Buchholz/OrderExtendedDirect.agda new file mode 100644 index 0000000..1fa9113 --- /dev/null +++ b/proofs/agda/Ordinal/Buchholz/OrderExtendedDirect.agda @@ -0,0 +1,225 @@ +{-# OPTIONS --safe --without-K #-} + +-- Earn-back of proof-debt ledger item B (Buchholz order), K-attributed +-- part. See `docs/echo-types/earn-back-plan.adoc` (ledger item B) and +-- `docs/retractions.adoc` (follow-up F-2026-05-18b). +-- +-- Item B's standing claim was: the two same-binder Buchholz-order +-- sub-cases +-- +-- * `bpsi ν α <ᵇ bpsi ν β` with `α <ᵇ β` (same Ω-index ν) +-- * `bplus x y₂ <ᵇ bplus x z₂` with `y₂ <ᵇ z₂` (same left summand) +-- +-- are "not constructible pending a K-free reformulation", because the +-- *naive* `<ᵇ-irrefl : x <ᵇ x → ⊥` pattern-matches `x <ᵇ x`, and the +-- shared binder (`ν`, resp. `x`) forces the unifier through a +-- reflexive equation `ν =?= ν` whose elimination is the K-restricted +-- *deletion* rule — rejected under `--without-K` (reconfirmed on +-- Agda 2.8; the Order.agda comment cited 2.6.3). +-- +-- This module discharges that claim *positively*. The same-binder +-- constructors ARE constructible directly, and the core strict-order +-- metatheory (irreflexivity, transitivity) is proved K-free, with +-- *zero postulates and zero escape pragmas*, by: +-- +-- * proving the generalised `<ᵇ⇒≢ : x <ᵇ y → x ≡ y → ⊥` by +-- induction on the *derivation* (indices `x`,`y` distinct — no +-- shared-binder unification ever arises), then +-- * discharging the explicit equation with no-confusion built only +-- from `cong` of total projections and the K-free *conflict* rule +-- (absurd patterns on equations between distinct constructors). +-- `refl` is never matched, so the K-restricted deletion rule is +-- never invoked. +-- +-- Conservativity. `Ordinal.Buchholz.Order._<ᵇ_` (the K-free core) +-- embeds faithfully into this relation (`embed` below); this is a +-- strict extension, not a redefinition. +-- +-- Scope / what is NOT claimed here. Well-foundedness of the *direct* +-- relation is a termination-checker matter (Routes A/B of +-- `docs/echo-types/buchholz-extended-wf.md`), orthogonal to K, and +-- remains delivered via the comparison *measure* +-- `Ordinal.Buchholz.ExtendedOrder._<ᵇ⁺_`, which stays load-bearing. +-- Trichotomy/totality is likewise out of scope here. This module +-- earns back exactly the K-attributed sub-claim of item B and no more. + +module Ordinal.Buchholz.OrderExtendedDirect where + +open import Data.Empty using (⊥) +open import Relation.Binary.PropositionalEquality + using (_≡_; refl; sym; cong; subst) + +open import Ordinal.OmegaMarkers using + ( OmegaIndex ; ω ; _≤Ω_ ; _<Ω_ ; <Ω-irrefl + ; <Ω-trans ; <Ω→≤Ω ; ≤Ω-trans ; ≤Ω-<Ω-trans ; <Ω-≤Ω-trans ) +open import Ordinal.Buchholz.Syntax using (BT; bzero; bOmega; bplus; bpsi) +open import Ordinal.Buchholz.Order as Core using () + +---------------------------------------------------------------------- +-- The extended direct relation: the K-free core constructors plus the +-- two same-binder constructors item B deferred. +---------------------------------------------------------------------- + +data _<ᵇᵈ_ : BT → BT → Set where + <ᵇ-0-Ω : ∀ {μ} → bzero <ᵇᵈ bOmega μ + <ᵇ-0-+ : ∀ {x y} → bzero <ᵇᵈ bplus x y + <ᵇ-0-ψ : ∀ {ν α} → bzero <ᵇᵈ bpsi ν α + <ᵇ-ΩΩ : ∀ {μ ν} → μ <Ω ν → bOmega μ <ᵇᵈ bOmega ν + <ᵇ-Ωψ : ∀ {μ ν α} → μ <Ω ν → bOmega μ <ᵇᵈ bpsi ν α + <ᵇ-ψΩ : ∀ {μ ν α β} → μ <Ω ν → bpsi μ α <ᵇᵈ bpsi ν β + <ᵇ-ψΩ≤ : ∀ {ν μ α} → ν ≤Ω μ → bpsi ν α <ᵇᵈ bOmega μ + <ᵇ-Ω+ : ∀ {μ x y} → bOmega μ <ᵇᵈ x → bOmega μ <ᵇᵈ bplus x y + <ᵇ-ψ+ : ∀ {ν α x y} → bpsi ν α <ᵇᵈ x → bpsi ν α <ᵇᵈ bplus x y + <ᵇ-+Ω : ∀ {x y μ} → x <ᵇᵈ bOmega μ → bplus x y <ᵇᵈ bOmega μ + <ᵇ-+ψ : ∀ {x y ν α} → x <ᵇᵈ bpsi ν α → bplus x y <ᵇᵈ bpsi ν α + <ᵇ-+1 : ∀ {x₁ x₂ y₁ y₂} → x₁ <ᵇᵈ y₁ → bplus x₁ x₂ <ᵇᵈ bplus y₁ y₂ + -- The two constructors item B reported "unconstructible pending a + -- K-free reformulation" — directly constructible here: + <ᵇ-ψα : ∀ {ν α β} → α <ᵇᵈ β → bpsi ν α <ᵇᵈ bpsi ν β + <ᵇ-+2 : ∀ {x y₂ z₂} → y₂ <ᵇᵈ z₂ → bplus x y₂ <ᵇᵈ bplus x z₂ + +infix 4 _<ᵇᵈ_ + +---------------------------------------------------------------------- +-- K-free no-confusion for BT: `cong` of total projections, plus the +-- conflict rule. No `refl` is matched anywhere below. +---------------------------------------------------------------------- + +unΩ : BT → OmegaIndex +unΩ (bOmega μ) = μ +unΩ (bpsi ν _) = ν +unΩ _ = ω + +unArg : BT → BT +unArg (bpsi _ α) = α +unArg (bplus _ y) = y +unArg _ = bzero + +unLeft : BT → BT +unLeft (bplus x _) = x +unLeft _ = bzero + +bOmega-inj : ∀ {μ ν} → bOmega μ ≡ bOmega ν → μ ≡ ν +bOmega-inj e = cong unΩ e + +bpsi-injΩ : ∀ {μ ν α β} → bpsi μ α ≡ bpsi ν β → μ ≡ ν +bpsi-injΩ e = cong unΩ e + +bpsi-injArg : ∀ {μ ν α β} → bpsi μ α ≡ bpsi ν β → α ≡ β +bpsi-injArg e = cong unArg e + +bplus-injL : ∀ {x₁ x₂ y₁ y₂} → bplus x₁ x₂ ≡ bplus y₁ y₂ → x₁ ≡ y₁ +bplus-injL e = cong unLeft e + +bplus-injR : ∀ {x₁ x₂ y₁ y₂} → bplus x₁ x₂ ≡ bplus y₁ y₂ → x₂ ≡ y₂ +bplus-injR e = cong unArg e + +---------------------------------------------------------------------- +-- Irreflexivity, K-free. The generalised form keeps `x`,`y` distinct +-- so the constructor match never produces a shared-binder equation; +-- the supplied `x ≡ y` is discharged without ever matching `refl`. +---------------------------------------------------------------------- + +<ᵇ⇒≢ : ∀ {x y} → x <ᵇᵈ y → x ≡ y → ⊥ +-- distinct-head constructors: K-free conflict rule. +<ᵇ⇒≢ <ᵇ-0-Ω () +<ᵇ⇒≢ <ᵇ-0-+ () +<ᵇ⇒≢ <ᵇ-0-ψ () +<ᵇ⇒≢ (<ᵇ-Ωψ _) () +<ᵇ⇒≢ (<ᵇ-ψΩ≤ _) () +<ᵇ⇒≢ (<ᵇ-Ω+ _) () +<ᵇ⇒≢ (<ᵇ-ψ+ _) () +<ᵇ⇒≢ (<ᵇ-+Ω _) () +<ᵇ⇒≢ (<ᵇ-+ψ _) () +-- same-head constructors: cong-injectivity + subst, no refl-match. +<ᵇ⇒≢ (<ᵇ-ΩΩ p) e = <Ω-irrefl (subst (_ <Ω_) (sym (bOmega-inj e)) p) +<ᵇ⇒≢ (<ᵇ-ψΩ p) e = <Ω-irrefl (subst (_ <Ω_) (sym (bpsi-injΩ e)) p) +<ᵇ⇒≢ (<ᵇ-+1 p) e = <ᵇ⇒≢ p (bplus-injL e) +<ᵇ⇒≢ (<ᵇ-ψα p) e = <ᵇ⇒≢ p (bpsi-injArg e) +<ᵇ⇒≢ (<ᵇ-+2 p) e = <ᵇ⇒≢ p (bplus-injR e) + +<ᵇ-irrefl : ∀ {x} → x <ᵇᵈ x → ⊥ +<ᵇ-irrefl p = <ᵇ⇒≢ p refl + +---------------------------------------------------------------------- +-- Transitivity, K-free. `<ᵇ-trans` matches `x <ᵇᵈ y` / `y <ᵇᵈ z` +-- (distinct indices), so the shared-binder deletion never arises; +-- the two new constructors only add ordinary constructor-pair clauses. +---------------------------------------------------------------------- + +<ᵇ-trans : ∀ {x y z} → x <ᵇᵈ y → y <ᵇᵈ z → x <ᵇᵈ z +-- core legs (mirrors `Ordinal.Buchholz.Order.<ᵇ-trans`): +<ᵇ-trans <ᵇ-0-Ω (<ᵇ-ΩΩ _) = <ᵇ-0-Ω +<ᵇ-trans <ᵇ-0-Ω (<ᵇ-Ωψ _) = <ᵇ-0-ψ +<ᵇ-trans <ᵇ-0-Ω (<ᵇ-Ω+ _) = <ᵇ-0-+ +<ᵇ-trans <ᵇ-0-+ (<ᵇ-+1 _) = <ᵇ-0-+ +<ᵇ-trans <ᵇ-0-+ (<ᵇ-+Ω _) = <ᵇ-0-Ω +<ᵇ-trans <ᵇ-0-+ (<ᵇ-+ψ _) = <ᵇ-0-ψ +<ᵇ-trans <ᵇ-0-ψ (<ᵇ-ψΩ _) = <ᵇ-0-ψ +<ᵇ-trans <ᵇ-0-ψ (<ᵇ-ψ+ _) = <ᵇ-0-+ +<ᵇ-trans (<ᵇ-ΩΩ p) (<ᵇ-ΩΩ q) = <ᵇ-ΩΩ (<Ω-trans p q) +<ᵇ-trans (<ᵇ-ΩΩ p) (<ᵇ-Ωψ q) = <ᵇ-Ωψ (<Ω-trans p q) +<ᵇ-trans (<ᵇ-ΩΩ p) (<ᵇ-Ω+ q) = <ᵇ-Ω+ (<ᵇ-trans (<ᵇ-ΩΩ p) q) +<ᵇ-trans (<ᵇ-Ωψ p) (<ᵇ-ψΩ q) = <ᵇ-Ωψ (<Ω-trans p q) +<ᵇ-trans (<ᵇ-Ωψ p) (<ᵇ-ψ+ q) = <ᵇ-Ω+ (<ᵇ-trans (<ᵇ-Ωψ p) q) +<ᵇ-trans (<ᵇ-ψΩ p) (<ᵇ-ψΩ q) = <ᵇ-ψΩ (<Ω-trans p q) +<ᵇ-trans (<ᵇ-ψΩ p) (<ᵇ-ψΩ≤ q) = <ᵇ-ψΩ≤ (≤Ω-trans (<Ω→≤Ω p) q) +<ᵇ-trans (<ᵇ-ψΩ p) (<ᵇ-ψ+ q) = <ᵇ-ψ+ (<ᵇ-trans (<ᵇ-ψΩ p) q) +<ᵇ-trans (<ᵇ-ψΩ≤ p) (<ᵇ-ΩΩ q) = <ᵇ-ψΩ≤ (≤Ω-trans p (<Ω→≤Ω q)) +<ᵇ-trans (<ᵇ-ψΩ≤ p) (<ᵇ-Ωψ q) = <ᵇ-ψΩ (≤Ω-<Ω-trans p q) +<ᵇ-trans (<ᵇ-ψΩ≤ p) (<ᵇ-Ω+ q) = <ᵇ-ψ+ (<ᵇ-trans (<ᵇ-ψΩ≤ p) q) +<ᵇ-trans (<ᵇ-+1 p) (<ᵇ-+1 q) = <ᵇ-+1 (<ᵇ-trans p q) +<ᵇ-trans (<ᵇ-+1 p) (<ᵇ-+Ω q) = <ᵇ-+Ω (<ᵇ-trans p q) +<ᵇ-trans (<ᵇ-+1 p) (<ᵇ-+ψ q) = <ᵇ-+ψ (<ᵇ-trans p q) +<ᵇ-trans (<ᵇ-Ω+ p) (<ᵇ-+1 q) = <ᵇ-Ω+ (<ᵇ-trans p q) +<ᵇ-trans (<ᵇ-Ω+ p) (<ᵇ-+Ω q) = <ᵇ-trans p q +<ᵇ-trans (<ᵇ-Ω+ p) (<ᵇ-+ψ q) = <ᵇ-trans p q +<ᵇ-trans (<ᵇ-ψ+ p) (<ᵇ-+1 q) = <ᵇ-ψ+ (<ᵇ-trans p q) +<ᵇ-trans (<ᵇ-ψ+ p) (<ᵇ-+Ω q) = <ᵇ-trans p q +<ᵇ-trans (<ᵇ-ψ+ p) (<ᵇ-+ψ q) = <ᵇ-trans p q +<ᵇ-trans (<ᵇ-+Ω p) (<ᵇ-ΩΩ q) = <ᵇ-+Ω (<ᵇ-trans p (<ᵇ-ΩΩ q)) +<ᵇ-trans (<ᵇ-+Ω p) (<ᵇ-Ωψ q) = <ᵇ-+ψ (<ᵇ-trans p (<ᵇ-Ωψ q)) +<ᵇ-trans (<ᵇ-+Ω p) (<ᵇ-Ω+ q) = <ᵇ-+1 (<ᵇ-trans p q) +<ᵇ-trans (<ᵇ-+ψ p) (<ᵇ-ψΩ q) = <ᵇ-+ψ (<ᵇ-trans p (<ᵇ-ψΩ q)) +<ᵇ-trans (<ᵇ-+ψ p) (<ᵇ-ψΩ≤ q) = <ᵇ-+Ω (<ᵇ-trans p (<ᵇ-ψΩ≤ q)) +<ᵇ-trans (<ᵇ-+ψ p) (<ᵇ-ψ+ q) = <ᵇ-+1 (<ᵇ-trans p q) +<ᵇ-trans <ᵇ-0-ψ (<ᵇ-ψΩ≤ _) = <ᵇ-0-Ω +<ᵇ-trans (<ᵇ-Ωψ p) (<ᵇ-ψΩ≤ q) = <ᵇ-ΩΩ (<Ω-≤Ω-trans p q) +-- `<ᵇ-ψα` as LEFT leg: +<ᵇ-trans (<ᵇ-ψα p) (<ᵇ-ψα q) = <ᵇ-ψα (<ᵇ-trans p q) +<ᵇ-trans (<ᵇ-ψα _) (<ᵇ-ψΩ q) = <ᵇ-ψΩ q +<ᵇ-trans (<ᵇ-ψα _) (<ᵇ-ψΩ≤ q) = <ᵇ-ψΩ≤ q +<ᵇ-trans (<ᵇ-ψα p) (<ᵇ-ψ+ q) = <ᵇ-ψ+ (<ᵇ-trans (<ᵇ-ψα p) q) +-- `<ᵇ-ψα` as RIGHT leg (left-leg head must land in `bpsi ν _`): +<ᵇ-trans <ᵇ-0-ψ (<ᵇ-ψα _) = <ᵇ-0-ψ +<ᵇ-trans (<ᵇ-Ωψ p) (<ᵇ-ψα _) = <ᵇ-Ωψ p +<ᵇ-trans (<ᵇ-ψΩ p) (<ᵇ-ψα _) = <ᵇ-ψΩ p +<ᵇ-trans (<ᵇ-+ψ p) (<ᵇ-ψα q) = <ᵇ-+ψ (<ᵇ-trans p (<ᵇ-ψα q)) +-- `<ᵇ-+2` as LEFT leg: +<ᵇ-trans (<ᵇ-+2 p) (<ᵇ-+2 q) = <ᵇ-+2 (<ᵇ-trans p q) +<ᵇ-trans (<ᵇ-+2 _) (<ᵇ-+1 q) = <ᵇ-+1 q +<ᵇ-trans (<ᵇ-+2 _) (<ᵇ-+Ω q) = <ᵇ-+Ω q +<ᵇ-trans (<ᵇ-+2 _) (<ᵇ-+ψ q) = <ᵇ-+ψ q +-- `<ᵇ-+2` as RIGHT leg (left-leg head must land in `bplus x _`): +<ᵇ-trans <ᵇ-0-+ (<ᵇ-+2 _) = <ᵇ-0-+ +<ᵇ-trans (<ᵇ-Ω+ p) (<ᵇ-+2 _) = <ᵇ-Ω+ p +<ᵇ-trans (<ᵇ-ψ+ p) (<ᵇ-+2 _) = <ᵇ-ψ+ p +<ᵇ-trans (<ᵇ-+1 p) (<ᵇ-+2 _) = <ᵇ-+1 p + +---------------------------------------------------------------------- +-- Conservativity: the K-free core embeds faithfully (not redefined). +---------------------------------------------------------------------- + +embed : ∀ {x y} → x Core.<ᵇ y → x <ᵇᵈ y +embed Core.<ᵇ-0-Ω = <ᵇ-0-Ω +embed Core.<ᵇ-0-+ = <ᵇ-0-+ +embed Core.<ᵇ-0-ψ = <ᵇ-0-ψ +embed (Core.<ᵇ-ΩΩ p) = <ᵇ-ΩΩ p +embed (Core.<ᵇ-Ωψ p) = <ᵇ-Ωψ p +embed (Core.<ᵇ-ψΩ p) = <ᵇ-ψΩ p +embed (Core.<ᵇ-ψΩ≤ p) = <ᵇ-ψΩ≤ p +embed (Core.<ᵇ-Ω+ p) = <ᵇ-Ω+ (embed p) +embed (Core.<ᵇ-ψ+ p) = <ᵇ-ψ+ (embed p) +embed (Core.<ᵇ-+Ω p) = <ᵇ-+Ω (embed p) +embed (Core.<ᵇ-+ψ p) = <ᵇ-+ψ (embed p) +embed (Core.<ᵇ-+1 p) = <ᵇ-+1 (embed p) diff --git a/proofs/agda/Ordinal/Buchholz/Smoke.agda b/proofs/agda/Ordinal/Buchholz/Smoke.agda index 52feae3..e51a377 100644 --- a/proofs/agda/Ordinal/Buchholz/Smoke.agda +++ b/proofs/agda/Ordinal/Buchholz/Smoke.agda @@ -74,6 +74,18 @@ open import Ordinal.Buchholz.Order using ; <ᵇ-inv-+ψω ) +-- Earn-back item B (K-attributed part): same-binder constructors +-- usable directly; irreflexivity + transitivity K-free. See +-- docs/echo-types/earn-back-plan.adoc item B, F-2026-05-18b. +open import Ordinal.Buchholz.OrderExtendedDirect using + ( _<ᵇᵈ_ + ; <ᵇ-ψα -- same Ω-index lex (was "unconstructible pending K-free") + ; <ᵇ-+2 -- same left-summand lex (idem) + ; <ᵇ-irrefl + ; <ᵇ-trans + ; embed -- conservativity: core `Order._<ᵇ_` ↪ `_<ᵇᵈ_` + ) + open import Ordinal.Buchholz.Psi using ( psiν-notin-Cν ; psiν-stage-lb