agda: iterate Buchholz wrapper construction

hyperpolymath · hyperpolymath · commit 01337078998e · 2026-04-23T21:14:25.000+01:00
diff --git a/README.md b/README.md
@@ -84,12 +84,14 @@ Ordinal/Buchholz track status:
 - `Ordinal.Buchholz.VeblenComparisonModel` is now the primary closed Veblen route: it instantiates the Veblen interface without deferred assumptions and exposes `core-wf-from-comparison : WellFounded _<ᵇ_`
 - `Ordinal.Buchholz.ExtendedOrder` now packages a closed comparison-induced extension `_ <ᵇ⁺ _` of `BT`: it contains the current core, exposes the historical same-binder principles as lemmas, and is transitive and well-founded
 - `Ordinal.Buchholz.LiftedExtendedOrder` now adds the next honest wrapper `_ <ᵇ⁺¹ _`: the blocked self-lift of `_ <ᵇ⁺ _` fails, but same-binder moves from `_ <ᵇ⁺ _` into `_ <ᵇ⁺¹ _` are derivable and `_ <ᵇ⁺¹ _` is well-founded
+- `Ordinal.Buchholz.IteratedExtendedOrder` now packages that repair as a finite iteration scheme: `LiftedOrder n` gives the `n`th wrapper layer, same-binder moves lift one level at a time, and exact finite same-binder depth is tracked by `SurfaceDepth n` with an embedding into `LiftedOrder (suc n)`
 - `Ordinal.Buchholz.SurfaceOrder` now adds a direct inductive surface `_ <ᵇˢ _` for the two historical same-binder shapes, with an embedding into `_ <ᵇ⁺ _` and inherited well-foundedness
-- the exact remaining recursive frontier is now explicit in code as a blocked self-lift: `SurfaceLiftInterface` is refuted by a concrete same-left `bplus` counterexample, but the new `_ <ᵇ⁺¹ _` wrapper shows the right next direction is wrapper iteration rather than self-stability
+- the exact remaining recursive frontier is now explicit in code as a blocked self-lift: `SurfaceLiftInterface` is refuted by a concrete same-left `bplus` counterexample, and the surviving route is finite wrapper iteration rather than self-stability
 - the Veblen comparison route is now closed for the current admitted constructor core
 - the new `_ <ᵇ⁺ _` wrapper advances the full-order line by giving a mediated closed relation on all terms
 - the new `_ <ᵇˢ _` surface is the first direct bridge candidate between the current core presentation and that mediated wrapper
-- this does not yet internalize the historically blocked shared-binder shapes as actual constructors of `_ <ᵇ _`; the full intended Buchholz order remains open at that step, and the recursive surface route is now known not to be the right intermediate theorem
+- the new `LiftedOrder n` / `SurfaceDepth n` family shows that arbitrary finite same-binder depth can already be handled by iterated mediated wrappers
+- this still does not internalize the historically blocked shared-binder shapes as actual constructors of `_ <ᵇ _`; the full intended Buchholz order remains open at that step
 - remaining live mathematical work is therefore not the current-core WF route, but the mediated internalization of the shared-binder cases back into the real order package
 
 ## External Bridge Targets (local workspace)
diff --git a/docs/buchholz-plan.adoc b/docs/buchholz-plan.adoc
@@ -148,6 +148,11 @@ The order / well-foundedness track now has an explicit staged split:
   well-founded wrapper `_ <ᵇ⁺¹ _` lifts same-binder moves out of
   `_ <ᵇ⁺ _` and proves the first nested example
   `ψν (x + y) < ψν (x + z)` from `y <ᵇ z`.
+* WF-1.88 (`Ordinal.Buchholz.IteratedExtendedOrder`): the one-step
+  repair now scales uniformly to finite depth. `LiftedOrder n`
+  iterates the wrapper construction over `ℕ`, `LiftedOrder-lift`
+  embeds each level into the next, and `SurfaceDepth n` records exact
+  same-binder depth with an embedding into `LiftedOrder (suc n)`.
 * WF-2 (completed for mixed-head cases): bridge layer now includes
   `bpsi ν α <ᵇ bOmega μ` (under `ν ≤Ω μ`), left-summand bridges into
   additive terms (`<ᵇ-Ω+`, `<ᵇ-ψ+`), and additive-target bridges
@@ -178,6 +183,10 @@ Current Veblen-route status after this update:
   well-founded wrapper `_ <ᵇ⁺¹ _`, showing that the surviving route is
   iterative wrapper lifting rather than a self-stability theorem for
   `_ <ᵇ⁺ _`.
+* `Ordinal.Buchholz.IteratedExtendedOrder` now packages that route at
+  arbitrary finite depth: the wrapper construction is iterated over
+  `ℕ`, and exact finite same-binder nesting is tracked by
+  `SurfaceDepth`.
 * It does *not* yet promote the historically blocked shared-binder
   shapes into actual constructors of `_ <ᵇ _`; that remains the
   missing step between the current core and the full intended
diff --git a/docs/echo-types/overview.md b/docs/echo-types/overview.md
@@ -97,8 +97,9 @@ maps can admit different echo types.
   parallel, syntactic development; its relationship to Echo Types
   via `EchoOrdinal.agda` is a bridge, not a reduction. At present,
   the current admitted Buchholz core has a closed well-foundedness
-  route, while the full intended order remains open at the
-  shared-binder internalization step.
+  route, and finite same-binder depth is now handled by iterated
+  mediated wrappers, while the full intended order remains open at
+  the shared-binder internalization step.
 - **Not a completed categorical semantics.** See
   `docs/assessment.adoc` for the current M5 verdict.
 
diff --git a/docs/echo-types/roadmap.md b/docs/echo-types/roadmap.md
@@ -11,7 +11,9 @@ For current cross-repo progress snapshots, see
   the historically blocked shared-binder shapes in `_<ᵇ_`.
   `wf-<ᵇ` is landed for the currently admitted core, but promoting
   those shapes back into the real order package still needs a
-  K-free mediated internalization.
+  K-free mediated internalization. Finite same-binder depth is now
+  handled by iterated mediated wrappers, but that does not yet close
+  the real order package itself.
 - **Bottleneck B2.** Tool-scope limitations on adjacent repos
   (`maa-framework/absolute-zero`, `januskey`,
   `tropical-resource-typing`). Blocks end-to-end bridge audits.
@@ -114,7 +116,8 @@ Paths marked **[unblocked]** can proceed today. Paths marked
 - **[gated on B1]** Internalize the missing shared-binder shapes as
   actual constructors/comparison principles of the real Buchholz
   order. The current route closes well-foundedness for the admitted
-  core, but not yet for the full intended constructor package.
+  core and handles arbitrary finite same-binder depth via iterated
+  wrappers, but not yet for the full intended constructor package.
 - **[gated on B1]** Re-close totality/inversion/transitivity and
   well-foundedness for the enlarged order after that internalization,
   including shared-binder cases such as `<ᵇ-ψα` and `<ᵇ-+2`.
diff --git a/proofs/agda/All.agda b/proofs/agda/All.agda
@@ -47,6 +47,7 @@ open import Ordinal.Buchholz.VeblenComparisonTarget
 open import Ordinal.Buchholz.VeblenComparisonModel
 open import Ordinal.Buchholz.ExtendedOrder
 open import Ordinal.Buchholz.LiftedExtendedOrder
+open import Ordinal.Buchholz.IteratedExtendedOrder
 open import Ordinal.Buchholz.SurfaceOrder
 open import Ordinal.Buchholz.VeblenObligations
 open import Ordinal.Buchholz.Smoke
diff --git a/proofs/agda/Ordinal/Buchholz/IteratedExtendedOrder.agda b/proofs/agda/Ordinal/Buchholz/IteratedExtendedOrder.agda
@@ -0,0 +1,180 @@
+{-# OPTIONS --safe --without-K #-}
+
+-- Systematic finite iteration of the comparison-induced wrapper.
+--
+-- The self-lift theorem for `_<ᵇ⁺_` is false, but the wrapper pattern
+-- itself survives finite iteration. This module packages that pattern
+-- through an explicit step operator on closed wrappers and a finite
+-- depth family of surface derivations embedding into the iterated
+-- wrappers.
+
+module Ordinal.Buchholz.IteratedExtendedOrder where
+
+open import Data.Nat.Base using (ℕ; zero; suc)
+open import Data.Product.Base using (_×_; _,_)
+open import Data.Product.Relation.Binary.Lex.Strict using (×-Lex; ×-wellFounded; ×-wellFounded')
+open import Data.Sum.Base using (inj₁; inj₂)
+open import Function.Base using (_on_)
+open import Induction.WellFounded using (WellFounded; wf⇒asym; module Subrelation)
+open import Relation.Binary.Construct.On as On using (wellFounded)
+open import Relation.Binary.Core using (Rel; _⇒_)
+open import Relation.Binary.Definitions using (Transitive)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
+open import Relation.Nullary using (¬_)
+
+open import Ordinal.Buchholz.Syntax using (BT; bzero; bplus; bpsi)
+open import Ordinal.Buchholz.Order using (_<ᵇ_; <ᵇ-trans)
+open import Ordinal.Buchholz.WellFounded using (wf-<ᵇ)
+open import Ordinal.Buchholz.VeblenComparisonTarget using
+  ( Payload
+  ; payload-neutral
+  ; payload-psi
+  ; payload-plus
+  ; _≈ᶜ_
+  ; ≈ᶜ-+
+  ; ≈ᶜ-ψ
+  ; ≈ᶜ-trans
+  ; <ᵇ-respʳ-≈ᶜ
+  ; <ᵇ-chain-≈ᶜ
+  )
+open import Ordinal.Buchholz.VeblenComparisonModel using (cmp-measure)
+
+record Wrapper : Set₁ where
+  field
+    rel   : Rel BT _
+    wf    : WellFounded rel
+    trans : Transitive rel
+
+open Wrapper
+
+coreWrapper : Wrapper
+coreWrapper = record
+  { rel   = _<ᵇ_
+  ; wf    = wf-<ᵇ
+  ; trans = <ᵇ-trans
+  }
+
+module Step (W : Wrapper) where
+  open Wrapper W renaming (rel to _<W_; wf to wfW; trans to transW)
+
+  data PayloadOrder : Payload → Payload → Set where
+    pPsiPsi   : ∀ {α β} → α <W β → PayloadOrder (payload-psi α) (payload-psi β)
+    pPsiPlus  : ∀ {α β y} → α <W β → PayloadOrder (payload-psi α) (payload-plus β y)
+    pPlusPlus : ∀ {a y z} → y <W z → PayloadOrder (payload-plus a y) (payload-plus a z)
+
+  payload-rank : Payload → BT × BT
+  payload-rank payload-neutral    = bzero , bzero
+  payload-rank (payload-psi α)    = α , bzero
+  payload-rank (payload-plus a y) = a , y
+
+  PayloadRankOrder : Rel (BT × BT) _
+  PayloadRankOrder = ×-Lex _≡_ _<W_ _<W_
+
+  payload-embed : PayloadOrder ⇒ (PayloadRankOrder on payload-rank)
+  payload-embed (pPsiPsi α<β)   = inj₁ α<β
+  payload-embed (pPsiPlus α<β)  = inj₁ α<β
+  payload-embed (pPlusPlus y<z) = inj₂ (refl , y<z)
+
+  payload-wf : WellFounded PayloadOrder
+  payload-wf =
+    let module SR = Subrelation payload-embed
+    in SR.wellFounded (wellFounded payload-rank (×-wellFounded wfW wfW))
+
+  payload-trans : Transitive PayloadOrder
+  payload-trans (pPsiPsi α<β)   (pPsiPsi β<γ)   = pPsiPsi (transW α<β β<γ)
+  payload-trans (pPsiPsi α<β)   (pPsiPlus β<γ)  = pPsiPlus (transW α<β β<γ)
+  payload-trans (pPsiPlus α<β)  (pPlusPlus _)   = pPsiPlus α<β
+  payload-trans (pPlusPlus y<z) (pPlusPlus z<w) = pPlusPlus (transW y<z z<w)
+
+  ComparisonOrder : Rel (BT × Payload) _
+  ComparisonOrder = ×-Lex _≈ᶜ_ _<ᵇ_ PayloadOrder
+
+  comparison-trans : Transitive ComparisonOrder
+  comparison-trans (inj₁ x<y)           (inj₁ y<z)            = inj₁ (<ᵇ-trans x<y y<z)
+  comparison-trans (inj₁ x<y)           (inj₂ (y≈z , _))      = inj₁ (<ᵇ-respʳ-≈ᶜ y≈z x<y)
+  comparison-trans (inj₂ (x≈y , _))     (inj₁ y<z)            = inj₁ (<ᵇ-chain-≈ᶜ x≈y y<z)
+  comparison-trans (inj₂ (x≈y , px<qy)) (inj₂ (y≈z , qy<rz)) =
+    inj₂ (≈ᶜ-trans x≈y y≈z , payload-trans px<qy qy<rz)
+
+  comparison-wf : WellFounded ComparisonOrder
+  comparison-wf = ×-wellFounded' ≈ᶜ-trans <ᵇ-respʳ-≈ᶜ wf-<ᵇ payload-wf
+
+  _<step_ : Rel BT _
+  _<step_ = ComparisonOrder on cmp-measure
+
+  wf-step : WellFounded _<step_
+  wf-step = On.wellFounded cmp-measure comparison-wf
+
+  ψ-step : ∀ {ν α β} → α <W β → bpsi ν α <step bpsi ν β
+  ψ-step α<β = inj₂ (≈ᶜ-ψ , pPsiPsi α<β)
+
+  +2-step : ∀ {x y z} → y <W z → bplus x y <step bplus x z
+  +2-step y<z = inj₂ (≈ᶜ-+ , pPlusPlus y<z)
+
+stepWrapper : Wrapper → Wrapper
+stepWrapper W =
+  let module S = Step W
+  in record
+    { rel   = S._<step_
+    ; wf    = S.wf-step
+    ; trans = S.comparison-trans
+    }
+
+IterWrapper : ℕ → Wrapper
+IterWrapper zero    = coreWrapper
+IterWrapper (suc n) = stepWrapper (IterWrapper n)
+
+LiftedOrder : ℕ → Rel BT _
+LiftedOrder n = rel (IterWrapper n)
+
+LiftedOrder-wf : (n : ℕ) → WellFounded (LiftedOrder n)
+LiftedOrder-wf n = wf (IterWrapper n)
+
+LiftedOrder-trans : (n : ℕ) → Transitive (LiftedOrder n)
+LiftedOrder-trans n = trans (IterWrapper n)
+
+mutual
+
+  payload-lift
+    : (n : ℕ)
+    → ∀ {p q}
+    → Step.PayloadOrder (IterWrapper n) p q
+    → Step.PayloadOrder (IterWrapper (suc n)) p q
+  payload-lift n (Step.pPsiPsi α<β)   = Step.pPsiPsi (LiftedOrder-lift n α<β)
+  payload-lift n (Step.pPsiPlus α<β)  = Step.pPsiPlus (LiftedOrder-lift n α<β)
+  payload-lift n (Step.pPlusPlus y<z) = Step.pPlusPlus (LiftedOrder-lift n y<z)
+
+  LiftedOrder-lift : (n : ℕ) → LiftedOrder n ⇒ LiftedOrder (suc n)
+  LiftedOrder-lift zero    x<y             = inj₁ x<y
+  LiftedOrder-lift (suc n) (inj₁ x<y)      = inj₁ x<y
+  LiftedOrder-lift (suc n) (inj₂ (x≈y , p)) = inj₂ (x≈y , payload-lift n p)
+
+lift-ψα : (n : ℕ) → ∀ {ν α β} → LiftedOrder n α β → LiftedOrder (suc n) (bpsi ν α) (bpsi ν β)
+lift-ψα n α<β =
+  let module S = Step (IterWrapper n)
+  in S.ψ-step α<β
+
+lift-+2 : (n : ℕ) → ∀ {x y z} → LiftedOrder n y z → LiftedOrder (suc n) (bplus x y) (bplus x z)
+lift-+2 n y<z =
+  let module S = Step (IterWrapper n)
+  in S.+2-step y<z
+
+lift-ψ+2 : (n : ℕ) → ∀ {ν x y z} → LiftedOrder n y z → LiftedOrder (suc (suc n)) (bpsi ν (bplus x y)) (bpsi ν (bplus x z))
+lift-ψ+2 n y<z = lift-ψα (suc n) (lift-+2 n y<z)
+
+LiftedOrder-irreflexive : (n : ℕ) → ∀ {x} → ¬ (LiftedOrder n x x)
+LiftedOrder-irreflexive n {x} x<x = wf⇒asym (LiftedOrder-wf n) x<x x<x
+
+-- Exact same-binder depth, measured above the current Buchholz core.
+data SurfaceDepth : ℕ → BT → BT → Set where
+  surf-core : ∀ {x y} → x <ᵇ y → SurfaceDepth zero x y
+  surf-ψα   : ∀ {n ν α β} → SurfaceDepth n α β → SurfaceDepth (suc n) (bpsi ν α) (bpsi ν β)
+  surf-+2   : ∀ {n x y z} → SurfaceDepth n y z → SurfaceDepth (suc n) (bplus x y) (bplus x z)
+
+surface⇒lifted : ∀ {n x y} → SurfaceDepth n x y → LiftedOrder (suc n) x y
+surface⇒lifted (surf-core x<y) = LiftedOrder-lift zero x<y
+surface⇒lifted {n = suc n} (surf-ψα p) = lift-ψα (suc n) (surface⇒lifted p)
+surface⇒lifted {n = suc n} (surf-+2 p) = lift-+2 (suc n) (surface⇒lifted p)
+
+SurfaceDepth-irreflexive : ∀ {n x} → ¬ (SurfaceDepth n x x)
+SurfaceDepth-irreflexive {n} {x} p = LiftedOrder-irreflexive (suc n) (surface⇒lifted p)
diff --git a/proofs/agda/Ordinal/Buchholz/Smoke.agda b/proofs/agda/Ordinal/Buchholz/Smoke.agda
@@ -188,6 +188,23 @@ open import Ordinal.Buchholz.LiftedExtendedOrder using
   ; <ᵇ⁺¹-irreflexive
   )
 
+open import Ordinal.Buchholz.IteratedExtendedOrder using
+  ( LiftedOrder
+  ; LiftedOrder-wf
+  ; LiftedOrder-trans
+  ; LiftedOrder-lift
+  ; lift-ψα
+  ; lift-+2
+  ; lift-ψ+2
+  ; LiftedOrder-irreflexive
+  ; SurfaceDepth
+  ; surf-core
+  ; surf-ψα
+  ; surf-+2
+  ; surface⇒lifted
+  ; SurfaceDepth-irreflexive
+  )
+
 open import Ordinal.Buchholz.SurfaceOrder using
   ( _<ᵇˢ_
   ; <ᵇˢ-core
diff --git a/readme.adoc b/readme.adoc
@@ -94,15 +94,17 @@ Ordinal/Buchholz track status:
 * `Ordinal.Buchholz.VeblenComparisonModel` is now the primary closed Veblen route: it packages that target into an assumption-free Veblen interface instantiation in which the original deferred obligations `dec-ψα` and `dec-+2`, and the lifted same-index `ψ`-to-`+` comparison, are all discharged internally.
 * `Ordinal.Buchholz.ExtendedOrder` now packages a closed comparison-induced extension `_ <ᵇ⁺ _` of `BT`: it contains the current core, exposes the historical same-binder principles as lemmas, and is transitive and well-founded.
 * `Ordinal.Buchholz.LiftedExtendedOrder` now adds the next honest wrapper `_ <ᵇ⁺¹ _`: the blocked self-lift of `_ <ᵇ⁺ _` fails, but same-binder moves from `_ <ᵇ⁺ _` into `_ <ᵇ⁺¹ _` are derivable and `_ <ᵇ⁺¹ _` is well-founded.
+* `Ordinal.Buchholz.IteratedExtendedOrder` now packages that repair as a finite iteration scheme: `LiftedOrder n` gives the `n`th wrapper layer, same-binder moves lift one level at a time, and exact finite same-binder depth is tracked by `SurfaceDepth n` with an embedding into `LiftedOrder (suc n)`.
 * `Ordinal.Buchholz.SurfaceOrder` now adds a direct inductive surface `_ <ᵇˢ _` for the two historical same-binder shapes, with an embedding into `_ <ᵇ⁺ _` and inherited well-foundedness.
-* The exact remaining recursive frontier is now explicit in code as a blocked self-lift: `SurfaceLiftInterface` is refuted by a concrete same-left `bplus` counterexample, but the new `_ <ᵇ⁺¹ _` wrapper shows the right next direction is wrapper iteration rather than self-stability.
+* The exact remaining recursive frontier is now explicit in code as a blocked self-lift: `SurfaceLiftInterface` is refuted by a concrete same-left `bplus` counterexample, and the surviving route is finite wrapper iteration rather than self-stability.
 * `Ordinal.Buchholz.VeblenObligations` advances the hard-obligation discharge track with concrete projection-model lemmas for both same-binder shapes:
 ** `dec-+2-plus-right`
 ** `dec-ψα-psi-arg`
 * The Veblen comparison route is now closed for the current admitted constructor core.
 * The new `_ <ᵇ⁺ _` wrapper advances the full-order line by giving a mediated closed relation on all terms.
 * The new `_ <ᵇˢ _` surface is the first direct bridge candidate between the current core presentation and that mediated wrapper.
-* This does not yet internalize the historically blocked shared-binder shapes as actual constructors of `_ <ᵇ _`; the full intended Buchholz order remains open at that step, and the recursive surface route is now known not to be the right intermediate theorem.
+* The new `LiftedOrder n` / `SurfaceDepth n` family shows that arbitrary finite same-binder depth can already be handled by iterated mediated wrappers.
+* This still does not internalize the historically blocked shared-binder shapes as actual constructors of `_ <ᵇ _`; the full intended Buchholz order remains open at that step.
 * The remaining live mathematical gap is therefore not current-core well-foundedness, but mediated internalization of the shared-binder cases back into the real order package.
 
 == External Bridge Targets (local workspace)
