agda: add recursive Buchholz surface frontier

Author: hyperpolymath

proofs/agda/Ordinal/Buchholz/Smoke.agda

@@ -186,6 +186,14 @@ open import Ordinal.Buchholz.SurfaceOrder using
   ; <ᵇˢ⇒<ᵇ⁺
   ; wf-<ᵇˢ
   ; <ᵇˢ-irreflexive
+  ; SurfaceLiftInterface
+  ; _<ᵇʳ_
+  ; <ᵇʳ-core
+  ; <ᵇʳ-ψα
+  ; <ᵇʳ-+2
+  ; <ᵇʳ⇒<ᵇ⁺
+  ; wf-<ᵇʳ
+  ; <ᵇʳ-irreflexive
   )
 
 open import Ordinal.Buchholz.VeblenObligations using

proofs/agda/Ordinal/Buchholz/SurfaceOrder.agda

@@ -22,6 +22,7 @@ open import Ordinal.Buchholz.Order using (_<ᵇ_)
 open import Ordinal.Buchholz.ExtendedOrder using (_<ᵇ⁺_; <ᵇ⇒<ᵇ⁺; <ᵇ⁺-ψα; <ᵇ⁺-+2; wf-<ᵇ⁺)
 
 infix 4 _<ᵇˢ_
+infix 4 _<ᵇʳ_
 
 data _<ᵇˢ_ : BT → BT → Set where
   <ᵇˢ-core : ∀ {x y} → x <ᵇ y → x <ᵇˢ y
@@ -40,3 +41,33 @@ wf-<ᵇˢ =
 
 <ᵇˢ-irreflexive : ∀ {x} → ¬ (x <ᵇˢ x)
 <ᵇˢ-irreflexive {x} x<x = wf⇒asym wf-<ᵇˢ x<x x<x
+
+-- Exact remaining interface for a recursive direct surface:
+-- if the closed wrapper `_<ᵇ⁺_` can be shown stable under same-binder
+-- descent with `_<ᵇ⁺_` premises, then the genuinely recursive surface
+-- order below becomes available immediately.
+
+record SurfaceLiftInterface : Set where
+  field
+    lift-ψα⁺ : ∀ {ν α β} → α <ᵇ⁺ β → bpsi ν α <ᵇ⁺ bpsi ν β
+    lift-+2⁺ : ∀ {x y₂ z₂} → y₂ <ᵇ⁺ z₂ → bplus x y₂ <ᵇ⁺ bplus x z₂
+
+open SurfaceLiftInterface
+
+data _<ᵇʳ_ (L : SurfaceLiftInterface) : BT → BT → Set where
+  <ᵇʳ-core : ∀ {x y} → x <ᵇ y → _<ᵇʳ_ L x y
+  <ᵇʳ-ψα   : ∀ {ν α β} → _<ᵇʳ_ L α β → _<ᵇʳ_ L (bpsi ν α) (bpsi ν β)
+  <ᵇʳ-+2   : ∀ {x y₂ z₂} → _<ᵇʳ_ L y₂ z₂ → _<ᵇʳ_ L (bplus x y₂) (bplus x z₂)
+
+<ᵇʳ⇒<ᵇ⁺ : ∀ {L x y} → _<ᵇʳ_ L x y → x <ᵇ⁺ y
+<ᵇʳ⇒<ᵇ⁺ {L} (<ᵇʳ-core x<y) = <ᵇ⇒<ᵇ⁺ x<y
+<ᵇʳ⇒<ᵇ⁺ {L} (<ᵇʳ-ψα α<β)   = lift-ψα⁺ L (<ᵇʳ⇒<ᵇ⁺ α<β)
+<ᵇʳ⇒<ᵇ⁺ {L} (<ᵇʳ-+2 y<z)   = lift-+2⁺ L (<ᵇʳ⇒<ᵇ⁺ y<z)
+
+wf-<ᵇʳ : ∀ {L} → WellFounded (λ x y → _<ᵇʳ_ L x y)
+wf-<ᵇʳ {L} =
+  let module SR = Subrelation <ᵇʳ⇒<ᵇ⁺
+  in SR.wellFounded wf-<ᵇ⁺
+
+<ᵇʳ-irreflexive : ∀ {L x} → ¬ (_<ᵇʳ_ L x x)
+<ᵇʳ-irreflexive {L} {x} x<x = wf⇒asym (wf-<ᵇʳ {L}) x<x x<x