From 6547ea8b6a8f30eb1421e5cc517eb9e8e199b46e Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Sat, 30 May 2026 15:59:17 +0100 Subject: [PATCH] =?UTF-8?q?proof:=20well-foundedness=20of=20`=5F<=E1=B5=87?= =?UTF-8?q?=E1=B5=98=5F`=20via=20rank-embedding=20transport?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Closes Gate 2 of the Slice 3+4 Route A session arc. Derives `WellFounded _<ᵇᵘ_` mechanically from `rank-pow-mono-<ᵇᵘ` (PR #168) and the existing `wf-<′` via the standard Subrelation + InverseImage transport pattern documented in `Ordinal.Buchholz.RankBrouwer`'s preamble. Zero new proof obligations; purely structural. `--safe --without-K`, no postulates, no funext. ## The rank-embedding recipe ```agda wf-rank-pow-pullback : WellFounded (λ x y → rank-pow x <′ rank-pow y) wf-rank-pow-pullback = On.wellFounded rank-pow wf-<′ wf-<ᵇᵘ : WellFounded _<ᵇᵘ_ wf-<ᵇᵘ = Subrelation.wellFounded rank-pow-mono-<ᵇᵘ wf-rank-pow-pullback ``` Two steps: 1. `On.wellFounded` (= `InverseImage.wellFounded`) lifts well- foundedness of `_<′_` on `Ord` to the pullback `_<′_ on rank-pow` on `BT`. 2. `Subrelation.wellFounded` transports well-foundedness from the pullback to `_<ᵇᵘ_`, consuming `rank-pow-mono-<ᵇᵘ` as the witness that `_<ᵇᵘ_` is a sub-relation of the pullback. The recipe is documented in `RankBrouwer.agda:55-56`: > wf-<ᵇʳᶠ = Subrelation.wellFounded rank-mono > (InverseImage.wellFounded rank wf-<′) `On.wellFounded` is the modern (non-deprecated) alias for `InverseImage.wellFounded`. ## Slice 3+4 Route A gate status after this PR | Gate | Status | |---|---| | 1 — tail-rank-equality discharge (cross-head rank-equal case) | open (structural blocker) | | **2 — well-foundedness of `_<ᵇᵘ_`** | **CLOSED HERE** | | 3 — Path-4 + further source-rule extensions | open (future-work, mechanical) | ## What this does NOT do - Does NOT prove well-foundedness of the WfCNF-narrowed `_<ᵇᵘⁿ_` (PR #169) separately — follows by the same Subrelation transport from `wf-<ᵇᵘ` via the canonical `<ᵇᵘⁿ → <ᵇᵘ` projection. Left for a thin follow-on if specifically needed. - Does NOT add a Brouwer-rank embedding stronger than `rank-pow` — `rank-pow` is K-free + lands in `Ord` + already discharges the WF transport. Nothing more sophisticated is needed. ## Local verification - All four Agda lanes typecheck clean, exit 0. - `bash tools/check-guardrails.sh proofs/agda` — 163 modules pass. - `sh scripts/kernel-guard.sh` — PASS. Two new names pinned in `Ordinal/Buchholz/Smoke.agda`: `wf-rank-pow-pullback`, `wf-<ᵇᵘ`. Co-Authored-By: Claude Opus 4.7 (1M context) --- proofs/agda/All.agda | 1 + .../Ordinal/Buchholz/RankMonoUnionWF.agda | 95 +++++++++++++++++++ proofs/agda/Ordinal/Buchholz/Smoke.agda | 14 +++ 3 files changed, 110 insertions(+) create mode 100644 proofs/agda/Ordinal/Buchholz/RankMonoUnionWF.agda diff --git a/proofs/agda/All.agda b/proofs/agda/All.agda index 1c98f55..410ab44 100644 --- a/proofs/agda/All.agda +++ b/proofs/agda/All.agda @@ -151,6 +151,7 @@ open import Ordinal.Buchholz.RankMonoUmbrellaSlice3 open import Ordinal.Buchholz.RankMonoUmbrellaSlice4 open import Ordinal.Buchholz.RankMonoSameLeft open import Ordinal.Buchholz.RankMonoUnion +open import Ordinal.Buchholz.RankMonoUnionWF open import Ordinal.Buchholz.RecursiveSurfaceOrder open import Ordinal.Buchholz.RecursiveSurfaceBudget open import Ordinal.Buchholz.SurfaceOrder diff --git a/proofs/agda/Ordinal/Buchholz/RankMonoUnionWF.agda b/proofs/agda/Ordinal/Buchholz/RankMonoUnionWF.agda new file mode 100644 index 0000000..8b65412 --- /dev/null +++ b/proofs/agda/Ordinal/Buchholz/RankMonoUnionWF.agda @@ -0,0 +1,95 @@ +{-# OPTIONS --safe --without-K #-} +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell + +-- Well-foundedness of the union rank-mono umbrella (2026-05-30). +-- +-- ## What this lands +-- +-- `wf-<ᵇᵘ : WellFounded _<ᵇᵘ_` — every union-derivation chain +-- terminates. Derived mechanically from `rank-pow-mono-<ᵇᵘ` +-- (PR #168) and the well-foundedness of Brouwer's `_<′_` (already +-- proved in `Ordinal.Brouwer.Phase13.wf-<′`) via the standard +-- Subrelation + InverseImage combinators from +-- `Induction.WellFounded` / `Relation.Binary.Construct.On`. +-- +-- ## The rank-embedding recipe +-- +-- This is the standard rank-WF transport pattern documented in +-- `Ordinal.Buchholz.RankBrouwer`'s preamble: +-- +-- wf-<ᵇᵘ = Subrelation.wellFounded rank-pow-mono-<ᵇᵘ +-- (On.wellFounded rank-pow wf-<′) +-- +-- 1. `On.wellFounded rank-pow wf-<′` lifts well-foundedness of +-- `_<′_` on `Ord` to the pullback `_<′_ on rank-pow` on `BT` +-- — InverseImage transport. +-- 2. `Subrelation.wellFounded rank-pow-mono-<ᵇᵘ` then transports +-- well-foundedness from the pullback to `_<ᵇᵘ_` itself, +-- consuming `rank-pow-mono-<ᵇᵘ : x <ᵇᵘ y → rank-pow x <′ rank-pow y` +-- as the witness that `_<ᵇᵘ_` is a sub-relation of the pullback. +-- +-- The recipe is purely structural: zero new proof obligations. +-- Closure follows from the existing `rank-pow-mono-<ᵇᵘ` (#168) +-- + the existing `wf-<′` (`Phase13`). +-- +-- ## Slice 3+4 Route A gate 2 closure +-- +-- Per #168's closing note, three gates remained open at the +-- architectural-realisation moment. This module discharges +-- **Gate 2** (well-foundedness of `_<ᵇᵘ_`) via the rank-embedding +-- transport, leaving: +-- +-- * Gate 1 — tail-rank-equality discharge for the cross-head +-- rank-equal case (structural ordinal-arithmetic blocker). +-- * Gate 3 — Path-4 + further source-rule extensions +-- (future-work, mechanical per the extension recipe). +-- +-- ## What this does NOT do +-- +-- * Does NOT prove well-foundedness of the WfCNF-narrowed +-- `_<ᵇᵘⁿ_` (PR #169) separately — it follows by the same +-- Subrelation transport from `wf-<ᵇᵘ` via the canonical +-- `<ᵇᵘⁿ → <ᵇᵘ` projection. Left for a thin follow-on if a +-- consumer needs the WfCNF-bundled form's WF specifically. +-- * Does NOT add a Brouwer-rank embedding stronger than +-- `rank-pow` — `rank-pow` is K-free + lands in `Ord` (Brouwer +-- ordinals) + already discharges the WF transport. Nothing +-- more sophisticated is needed for this consumer. + +module Ordinal.Buchholz.RankMonoUnionWF where + +open import Induction.WellFounded using + ( WellFounded + ; module Subrelation + ) +open import Relation.Binary.Construct.On as On using (wellFounded) + +open import Ordinal.Brouwer using (Ord) +open import Ordinal.Brouwer.Phase13 using (_<′_; wf-<′) +open import Ordinal.Buchholz.Syntax using (BT) +open import Ordinal.Buchholz.RankPow using (rank-pow) +open import Ordinal.Buchholz.RankMonoUnion using + ( _<ᵇᵘ_ + ; rank-pow-mono-<ᵇᵘ + ) + +---------------------------------------------------------------------- +-- Well-foundedness of `_<ᵇᵘ_` +---------------------------------------------------------------------- + +-- Step 1 — InverseImage transport: well-foundedness of `_<′_` on +-- `Ord` lifts to well-foundedness of `_<′_ on rank-pow` on `BT`. +-- Note that the pullback relation has the same shape as +-- `rank-pow x <′ rank-pow y` but is named `_<′_ on rank-pow`. + +wf-rank-pow-pullback : WellFounded (λ x y → rank-pow x <′ rank-pow y) +wf-rank-pow-pullback = On.wellFounded rank-pow wf-<′ + +-- Step 2 — Subrelation transport: any sub-relation of a well- +-- founded relation is well-founded. `rank-pow-mono-<ᵇᵘ` is the +-- witness that `_<ᵇᵘ_` is a sub-relation of `_<′_ on rank-pow`, +-- so `_<ᵇᵘ_` inherits well-foundedness. + +wf-<ᵇᵘ : WellFounded _<ᵇᵘ_ +wf-<ᵇᵘ = Subrelation.wellFounded rank-pow-mono-<ᵇᵘ wf-rank-pow-pullback diff --git a/proofs/agda/Ordinal/Buchholz/Smoke.agda b/proofs/agda/Ordinal/Buchholz/Smoke.agda index 7a216a5..0c7af78 100644 --- a/proofs/agda/Ordinal/Buchholz/Smoke.agda +++ b/proofs/agda/Ordinal/Buchholz/Smoke.agda @@ -603,3 +603,17 @@ open import Ordinal.Buchholz.RankMonoUnion using ; <ᵇᵘ-from-<ᵇ⁰ ; <ᵇᵘ-from-<ᵇ⁰-via-<ᵇ⁺² ) + +-- Union umbrella well-foundedness 2026-05-30 (own block per +-- CLAUDE.md Working rules): closes Gate 2 of the Slice 3+4 Route +-- A session arc. `wf-<ᵇᵘ` derives WellFounded `_<ᵇᵘ_` via the +-- standard Subrelation + InverseImage rank-embedding transport +-- (rank-pow ∘ wf-<′). Zero new proof obligations; purely +-- structural. Together with the WfCNF wrap (PR #169) this +-- equips downstream Buchholz consumers with both the +-- canonical-form invariant AND termination of union-derivation +-- chains. +open import Ordinal.Buchholz.RankMonoUnionWF using + ( wf-rank-pow-pullback + ; wf-<ᵇᵘ + )