agda: record blocked recursive surface lift

Author: hyperpolymath

README.md

@@ -84,11 +84,11 @@ 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.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 `SurfaceLiftInterface`: if `_ <ᵇ⁺ _` is shown stable under same-binder descent with `_ <ᵇ⁺ _` premises, a genuinely recursive surface order `_ <ᵇʳ _` follows immediately
+- 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 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
+- 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
 - 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)

docs/buchholz-plan.adoc

@@ -137,10 +137,12 @@ The order / well-foundedness track now has an explicit staged split:
   constructors over current-core premises; embeds into `_ <ᵇ⁺ _` and
   therefore inherits well-foundedness immediately.
 * WF-1.86 (`SurfaceLiftInterface` / recursive `_ <ᵇʳ _` skeleton in
-  `Ordinal.Buchholz.SurfaceOrder`): the exact remaining frontier is
-  now formalized as two lifted same-binder closure obligations over
-  `_ <ᵇ⁺ _`; if those are discharged, a genuinely recursive surface
-  relation follows by subrelation into the closed wrapper.
+  `Ordinal.Buchholz.SurfaceOrder`): this candidate was tested and
+  blocked. A concrete same-left `bplus` counterexample refutes the
+  required lifted `ψ`-stability against the current wrapper, so the
+  recursive surface route is not the right intermediate theorem.
+  The direct surface bridge `_ <ᵇˢ _` remains the proved bridge
+  candidate.
 * WF-2 (completed for mixed-head cases): bridge layer now includes
   `bpsi ν α <ᵇ bOmega μ` (under `ν ≤Ω μ`), left-summand bridges into
   additive terms (`<ᵇ-Ω+`, `<ᵇ-ψ+`), and additive-target bridges
@@ -164,6 +166,9 @@ Current Veblen-route status after this update:
   constructor-level bridge candidate: the same-binder shapes exist as
   constructors there, but still over current-core premises, and the
   closure argument runs by embedding into `_ <ᵇ⁺ _`.
+* The attempted recursive surface lift is now explicitly blocked by a
+  counterexample theorem in `Ordinal.Buchholz.SurfaceOrder`; the
+  proved bridge remains `_ <ᵇˢ _`.
 * 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/Ordinal/Buchholz/Smoke.agda

@@ -194,6 +194,9 @@ open import Ordinal.Buchholz.SurfaceOrder using
   ; <ᵇʳ⇒<ᵇ⁺
   ; wf-<ᵇʳ
   ; <ᵇʳ-irreflexive
+  ; <ᵇ⁺-no-ψ-bzero-plus
+  ; surfaceLiftPremise
+  ; surfaceLiftBlocked
   )
 
 open import Ordinal.Buchholz.VeblenObligations using

proofs/agda/Ordinal/Buchholz/SurfaceOrder.agda

@@ -16,10 +16,24 @@ module Ordinal.Buchholz.SurfaceOrder where
 open import Relation.Nullary using (¬_)
 open import Relation.Binary.Core using (_⇒_)
 open import Induction.WellFounded using (WellFounded; wf⇒asym; module Subrelation)
-
-open import Ordinal.Buchholz.Syntax using (BT; bplus; bpsi)
-open import Ordinal.Buchholz.Order using (_<ᵇ_)
+open import Data.Empty using (⊥)
+open import Data.Product.Base using (_×_; proj₂)
+open import Data.Sum.Base using (inj₁; inj₂)
+
+open import Ordinal.OmegaMarkers using (Omega0; _<Ω_; <Ω-irrefl)
+open import Ordinal.Buchholz.Syntax using (BT; bzero; bplus; bpsi)
+open import Ordinal.Buchholz.Order using (_<ᵇ_; <ᵇ-irrefl; <ᵇ-0-+; <ᵇ-ψΩ)
+  renaming (<ᵇ-+1 to plus1)
 open import Ordinal.Buchholz.ExtendedOrder using (_<ᵇ⁺_; <ᵇ⇒<ᵇ⁺; <ᵇ⁺-ψα; <ᵇ⁺-+2; wf-<ᵇ⁺)
+open import Ordinal.Buchholz.VeblenComparisonTarget using
+  ( by-second
+  ; ≈ᶜ-+
+  ; by-payload-++
+  ; _≈ᶜ_
+  ; payload-psi
+  ; _≺P_
+  ; pPsiPsi
+  )
 
 infix 4 _<ᵇˢ_
 infix 4 _<ᵇʳ_
@@ -71,3 +85,32 @@ wf-<ᵇʳ {L} =
 
 <ᵇʳ-irreflexive : ∀ {L x} → ¬ (_<ᵇʳ_ L x x)
 <ᵇʳ-irreflexive {L} {x} x<x = wf⇒asym (wf-<ᵇʳ {L}) x<x x<x
+
+-- The recursive frontier is not merely unfilled: the current wrapper
+-- does not support the required same-binder lifting. A same-left plus
+-- witness gives a concrete counterexample to `lift-ψα⁺`.
+
+<ᵇ-same-left-plus-impossible : ∀ {x y z} → ¬ (bplus x y <ᵇ bplus x z)
+<ᵇ-same-left-plus-impossible {x} {y} {z} p with p
+... | plus1 x<x = <ᵇ-irrefl x<x
+
+<ᵇ⁺-no-ψ-bzero-plus :
+  ∀ {ν} →
+  ¬ (bpsi ν (bplus bzero bzero) <ᵇ⁺ bpsi ν (bplus bzero (bplus bzero bzero)))
+<ᵇ⁺-no-ψ-bzero-plus-helper :
+  payload-psi (bplus bzero bzero) ≺P
+  payload-psi (bplus bzero (bplus bzero bzero)) →
+  ⊥
+<ᵇ⁺-no-ψ-bzero-plus-helper (pPsiPsi y<z) = <ᵇ-same-left-plus-impossible y<z
+
+<ᵇ⁺-no-ψ-bzero-plus p with p
+... | inj₁ (<ᵇ-ψΩ ν<ν) = <Ω-irrefl ν<ν
+... | inj₂ q = <ᵇ⁺-no-ψ-bzero-plus-helper (proj₂ q)
+
+surfaceLiftPremise : bplus bzero bzero <ᵇ⁺ bplus bzero (bplus bzero bzero)
+surfaceLiftPremise = by-second ≈ᶜ-+ (by-payload-++ <ᵇ-0-+)
+
+surfaceLiftBlocked : ¬ SurfaceLiftInterface
+surfaceLiftBlocked L =
+  <ᵇ⁺-no-ψ-bzero-plus {ν = Omega0}
+    (lift-ψα⁺ L {ν = Omega0} surfaceLiftPremise)

readme.adoc

@@ -94,14 +94,14 @@ 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.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 `SurfaceLiftInterface`: if `_ <ᵇ⁺ _` can be shown stable under same-binder descent with `_ <ᵇ⁺ _` premises, then a genuinely recursive surface order `_ <ᵇʳ _` follows immediately.
+* 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.
 * `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.
+* 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 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)