agda: add one-level lifted Buchholz wrapper

Author: hyperpolymath

README.md

@@ -83,8 +83,9 @@ Ordinal/Buchholz track status:
 - `Ordinal.Buchholz.VeblenComparisonTarget` adds a second concrete target: a lexicographic order on `BT × Payload` with recursive `ψ`-compatibility on the first coordinate and tagged payload descent for the same-binder follow-up cases
 - `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.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 candidate: `SurfaceLiftInterface` is refuted by a concrete same-left `bplus` counterexample, so the genuinely recursive surface order `_ <ᵇʳ _` does not follow from the current wrapper
+- 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 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

docs/buchholz-plan.adoc

@@ -143,6 +143,11 @@ The order / well-foundedness track now has an explicit staged split:
   recursive surface route is not the right intermediate theorem.
   The direct surface bridge `_ <ᵇˢ _` remains the proved bridge
   candidate.
+* WF-1.87 (`Ordinal.Buchholz.LiftedExtendedOrder`): the next honest
+  step is wrapper iteration rather than wrapper self-lift. A new
+  well-founded wrapper `_ <ᵇ⁺¹ _` lifts same-binder moves out of
+  `_ <ᵇ⁺ _` and proves the first nested example
+  `ψν (x + y) < ψν (x + z)` from `y <ᵇ z`.
 * WF-2 (completed for mixed-head cases): bridge layer now includes
   `bpsi ν α <ᵇ bOmega μ` (under `ν ≤Ω μ`), left-summand bridges into
   additive terms (`<ᵇ-Ω+`, `<ᵇ-ψ+`), and additive-target bridges
@@ -169,6 +174,10 @@ Current Veblen-route status after this update:
 * The attempted recursive surface lift is now explicitly blocked by a
   counterexample theorem in `Ordinal.Buchholz.SurfaceOrder`; the
   proved bridge remains `_ <ᵇˢ _`.
+* `Ordinal.Buchholz.LiftedExtendedOrder` now supplies the next
+  well-founded wrapper `_ <ᵇ⁺¹ _`, showing that the surviving route is
+  iterative wrapper lifting rather than a self-stability theorem for
+  `_ <ᵇ⁺ _`.
 * 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

proofs/agda/All.agda

@@ -46,6 +46,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.LiftedExtendedOrder
 open import Ordinal.Buchholz.SurfaceOrder
 open import Ordinal.Buchholz.VeblenObligations
 open import Ordinal.Buchholz.Smoke

proofs/agda/Ordinal/Buchholz/LiftedExtendedOrder.agda

@@ -0,0 +1,123 @@
+{-# OPTIONS --safe --without-K #-}
+
+-- One-level lift of the closed comparison wrapper.
+--
+-- `_<ᵇ⁺_` is too weak to be stable under the recursive same-binder
+-- lifts needed for a self-contained surface recursion. This module
+-- records the next honest step: lift those same-binder moves from the
+-- current wrapper into a new well-founded wrapper one level up.
+
+module Ordinal.Buchholz.LiftedExtendedOrder where
+
+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.Nullary using (¬_)
+open import Relation.Binary.Core using (Rel; _⇒_)
+open import Relation.Binary.Construct.On as On using (wellFounded)
+open import Relation.Binary.Definitions using (Transitive)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
+
+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.ExtendedOrder using
+  ( _<ᵇ⁺_
+  ; <ᵇ⇒<ᵇ⁺
+  ; <ᵇ⁺-+2
+  ; <ᵇ⁺-trans
+  ; wf-<ᵇ⁺
+  )
+open import Ordinal.Buchholz.VeblenComparisonTarget using
+  ( Payload
+  ; payload-neutral
+  ; payload-psi
+  ; payload-plus
+  ; _≈ᶜ_
+  ; _≺P_
+  ; pPsiPsi
+  ; pPsiPlus
+  ; pPlusPlus
+  ; ≈ᶜ-+
+  ; ≈ᶜ-ψ
+  ; ≈ᶜ-trans
+  ; <ᵇ-respʳ-≈ᶜ
+  ; <ᵇ-chain-≈ᶜ
+  )
+open import Ordinal.Buchholz.VeblenComparisonModel using (cmp-measure)
+
+infix 4 _≺P⁺¹_ _≺C⁺¹_ _<ᵇ⁺¹_
+
+data _≺P⁺¹_ : Payload → Payload → Set where
+  pPsiPsi⁺¹   : ∀ {α β} → α <ᵇ⁺ β → payload-psi α ≺P⁺¹ payload-psi β
+  pPsiPlus⁺¹  : ∀ {α β y} → α <ᵇ⁺ β → payload-psi α ≺P⁺¹ payload-plus β y
+  pPlusPlus⁺¹ : ∀ {a y z} → y <ᵇ⁺ z → payload-plus a y ≺P⁺¹ 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
+
+_≺PL⁺¹_ : Rel (BT × BT) _
+_≺PL⁺¹_ = ×-Lex _≡_ _<ᵇ⁺_ _<ᵇ⁺_
+
+payload-embed⁺¹ : _≺P⁺¹_ ⇒ (_≺PL⁺¹_ on payload-rank)
+payload-embed⁺¹ (pPsiPsi⁺¹ α<β)   = inj₁ α<β
+payload-embed⁺¹ (pPsiPlus⁺¹ α<β)  = inj₁ α<β
+payload-embed⁺¹ (pPlusPlus⁺¹ y<z) = inj₂ (refl , y<z)
+
+≺PL⁺¹-wf : WellFounded _≺PL⁺¹_
+≺PL⁺¹-wf = ×-wellFounded wf-<ᵇ⁺ wf-<ᵇ⁺
+
+≺P⁺¹-wf : WellFounded _≺P⁺¹_
+≺P⁺¹-wf =
+  let module SR = Subrelation payload-embed⁺¹
+  in SR.wellFounded (wellFounded payload-rank ≺PL⁺¹-wf)
+
+≺P⁺¹-trans : Transitive _≺P⁺¹_
+≺P⁺¹-trans (pPsiPsi⁺¹ α<β)   (pPsiPsi⁺¹ β<γ)   = pPsiPsi⁺¹ (<ᵇ⁺-trans α<β β<γ)
+≺P⁺¹-trans (pPsiPsi⁺¹ α<β)   (pPsiPlus⁺¹ β<γ)  = pPsiPlus⁺¹ (<ᵇ⁺-trans α<β β<γ)
+≺P⁺¹-trans (pPsiPlus⁺¹ α<β)  (pPlusPlus⁺¹ _)   = pPsiPlus⁺¹ α<β
+≺P⁺¹-trans (pPlusPlus⁺¹ y<z) (pPlusPlus⁺¹ z<w) = pPlusPlus⁺¹ (<ᵇ⁺-trans y<z z<w)
+
+_≺C⁺¹_ : Rel (BT × Payload) _
+_≺C⁺¹_ = ×-Lex _≈ᶜ_ _<ᵇ_ _≺P⁺¹_
+
+≺C⁺¹-trans : Transitive _≺C⁺¹_
+≺C⁺¹-trans (inj₁ x<y)           (inj₁ y<z)            = inj₁ (<ᵇ-trans x<y y<z)
+≺C⁺¹-trans (inj₁ x<y)           (inj₂ (y≈z , _))      = inj₁ (<ᵇ-respʳ-≈ᶜ y≈z x<y)
+≺C⁺¹-trans (inj₂ (x≈y , _))     (inj₁ y<z)            = inj₁ (<ᵇ-chain-≈ᶜ x≈y y<z)
+≺C⁺¹-trans (inj₂ (x≈y , px<qy)) (inj₂ (y≈z , qy<rz)) =
+  inj₂ (≈ᶜ-trans x≈y y≈z , ≺P⁺¹-trans px<qy qy<rz)
+
+≺C⁺¹-wf : WellFounded _≺C⁺¹_
+≺C⁺¹-wf = ×-wellFounded' ≈ᶜ-trans <ᵇ-respʳ-≈ᶜ wf-<ᵇ ≺P⁺¹-wf
+
+_<ᵇ⁺¹_ : Rel BT _
+_<ᵇ⁺¹_ = _≺C⁺¹_ on cmp-measure
+
+payload-lift⁺¹ : _≺P_ ⇒ _≺P⁺¹_
+payload-lift⁺¹ (pPsiPsi α<β)   = pPsiPsi⁺¹ (<ᵇ⇒<ᵇ⁺ α<β)
+payload-lift⁺¹ (pPsiPlus α<β)  = pPsiPlus⁺¹ (<ᵇ⇒<ᵇ⁺ α<β)
+payload-lift⁺¹ (pPlusPlus y<z) = pPlusPlus⁺¹ (<ᵇ⇒<ᵇ⁺ y<z)
+
+<ᵇ⁺⇒<ᵇ⁺¹ : _<ᵇ⁺_ ⇒ _<ᵇ⁺¹_
+<ᵇ⁺⇒<ᵇ⁺¹ (inj₁ x<y)       = inj₁ x<y
+<ᵇ⁺⇒<ᵇ⁺¹ (inj₂ (x≈y , p)) = inj₂ (x≈y , payload-lift⁺¹ p)
+
+<ᵇ⁺¹-ψα : ∀ {ν α β} → α <ᵇ⁺ β → bpsi ν α <ᵇ⁺¹ bpsi ν β
+<ᵇ⁺¹-ψα α<β = inj₂ (≈ᶜ-ψ , pPsiPsi⁺¹ α<β)
+
+<ᵇ⁺¹-+2 : ∀ {x y z} → y <ᵇ⁺ z → bplus x y <ᵇ⁺¹ bplus x z
+<ᵇ⁺¹-+2 y<z = inj₂ (≈ᶜ-+ , pPlusPlus⁺¹ y<z)
+
+<ᵇ⁺¹-ψ+2 : ∀ {ν x y z} → y <ᵇ z → bpsi ν (bplus x y) <ᵇ⁺¹ bpsi ν (bplus x z)
+<ᵇ⁺¹-ψ+2 y<z = <ᵇ⁺¹-ψα (<ᵇ⁺-+2 y<z)
+
+wf-<ᵇ⁺¹ : WellFounded _<ᵇ⁺¹_
+wf-<ᵇ⁺¹ = On.wellFounded cmp-measure ≺C⁺¹-wf
+
+<ᵇ⁺¹-irreflexive : ∀ {x} → ¬ (x <ᵇ⁺¹ x)
+<ᵇ⁺¹-irreflexive {x} x<x = wf⇒asym wf-<ᵇ⁺¹ x<x x<x

proofs/agda/Ordinal/Buchholz/Smoke.agda

@@ -178,6 +178,16 @@ open import Ordinal.Buchholz.ExtendedOrder using
   ; <ᵇ⁺-irreflexive
   )
 
+open import Ordinal.Buchholz.LiftedExtendedOrder using
+  ( _<ᵇ⁺¹_
+  ; <ᵇ⁺⇒<ᵇ⁺¹
+  ; <ᵇ⁺¹-ψα
+  ; <ᵇ⁺¹-+2
+  ; <ᵇ⁺¹-ψ+2
+  ; wf-<ᵇ⁺¹
+  ; <ᵇ⁺¹-irreflexive
+  )
+
 open import Ordinal.Buchholz.SurfaceOrder using
   ( _<ᵇˢ_
   ; <ᵇˢ-core

readme.adoc

@@ -93,8 +93,9 @@ Ordinal/Buchholz track status:
 * `Ordinal.Buchholz.VeblenComparisonTarget` adds a second concrete target: a lexicographic order on `BT × Payload` whose first coordinate is relaxed by recursive `ψ`-compatibility, and whose tagged payload order handles the same-binder descent cases without introducing unstable extra comparisons.
 * `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.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 candidate: `SurfaceLiftInterface` is refuted by a concrete same-left `bplus` counterexample, so the genuinely recursive surface order `_ <ᵇʳ _` does not follow from the current wrapper.
+* 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.
 * `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`