agda: add first concrete Veblen-interface instantiation

Author: hyperpolymath

docs/buchholz-plan.adoc

@@ -107,6 +107,9 @@ The order / well-foundedness track now has an explicit staged split:
   pinning constructor-by-constructor decrease obligations and explicit
   deferred same-binder obligations (`dec-ψα`, `dec-+2`) for the Veblen
   follow-up.
+* WF-1.6 (`Ordinal.Buchholz.VeblenIdentityModel`): first concrete
+  instantiation of the interface (identity-measure bootstrap), keeping
+  `dec-ψα` and `dec-+2` as explicit assumptions.
 * WF-2 (in progress): explicit inversion lemmas for the still-open
   mixed head cases (`Ω/+`, `ψ/+`) and the newly admitted comparison
   bridge `bpsi ν α <ᵇ bOmega μ` under `ν ≤Ω μ`.

proofs/agda/All.agda

@@ -40,6 +40,7 @@ open import Ordinal.Buchholz.Examples
 open import Ordinal.Buchholz.WellFormed
 open import Ordinal.Buchholz.WellFounded
 open import Ordinal.Buchholz.VeblenInterface
+open import Ordinal.Buchholz.VeblenIdentityModel
 open import Ordinal.Buchholz.Smoke
 
 open import Smoke

proofs/agda/Ordinal/Buchholz/Smoke.agda

@@ -112,3 +112,8 @@ open import Ordinal.Buchholz.WellFormed using
 open import Ordinal.Buchholz.VeblenInterface using
   ( VeblenWFInterface
   )
+
+open import Ordinal.Buchholz.VeblenIdentityModel using
+  ( identity-interface
+  ; core-wf-from-identity
+  )

proofs/agda/Ordinal/Buchholz/VeblenIdentityModel.agda

@@ -0,0 +1,57 @@
+{-# OPTIONS --safe --without-K #-}
+
+-- Minimal concrete instantiation of the Veblen WF interface.
+--
+-- This uses the identity measure on BT as a bootstrap model to confirm
+-- interface coherence. The two same-binder obligations remain explicit
+-- parameters (`dec-ψα`, `dec-+2`), matching the currently deferred hard
+-- cases.
+
+module Ordinal.Buchholz.VeblenIdentityModel where
+
+open import Induction.WellFounded using (WellFounded)
+
+open import Ordinal.Buchholz.Syntax using (BT; bzero; bOmega; bplus; bpsi)
+open import Ordinal.Buchholz.Order using
+  ( _<ᵇ_
+  ; <ᵇ-0-Ω
+  ; <ᵇ-0-+
+  ; <ᵇ-0-ψ
+  ; <ᵇ-ΩΩ
+  ; <ᵇ-Ωψ
+  ; <ᵇ-ψΩ
+  ; <ᵇ-ψΩ≤
+  ; <ᵇ-+ω
+  ; <ᵇ-+ψω
+  ; <ᵇ-+1
+  )
+open import Ordinal.Buchholz.WellFounded using (wf-<ᵇ)
+open import Ordinal.Buchholz.VeblenInterface using (VeblenWFInterface)
+
+identity-interface :
+  (dec-ψα : ∀ {ν α β} → α <ᵇ β → bpsi ν α <ᵇ bpsi ν β) →
+  (dec-+2 : ∀ {x y₂ z₂} → y₂ <ᵇ z₂ → bplus x y₂ <ᵇ bplus x z₂) →
+  VeblenWFInterface BT _<ᵇ_
+identity-interface dec-ψα dec-+2 = record
+  { measure = λ x → x
+  ; ≺-wf = wf-<ᵇ
+  ; dec-0-Ω = <ᵇ-0-Ω
+  ; dec-0-+ = <ᵇ-0-+
+  ; dec-0-ψ = <ᵇ-0-ψ
+  ; dec-ΩΩ = <ᵇ-ΩΩ
+  ; dec-Ωψ = <ᵇ-Ωψ
+  ; dec-ψΩ = <ᵇ-ψΩ
+  ; dec-ψΩ≤ = <ᵇ-ψΩ≤
+  ; dec-+ω = <ᵇ-+ω
+  ; dec-+ψω = <ᵇ-+ψω
+  ; dec-+1 = <ᵇ-+1
+  ; dec-ψα = dec-ψα
+  ; dec-+2 = dec-+2
+  }
+
+core-wf-from-identity :
+  (dec-ψα : ∀ {ν α β} → α <ᵇ β → bpsi ν α <ᵇ bpsi ν β) →
+  (dec-+2 : ∀ {x y₂ z₂} → y₂ <ᵇ z₂ → bplus x y₂ <ᵇ bplus x z₂) →
+  WellFounded _<ᵇ_
+core-wf-from-identity dec-ψα dec-+2 =
+  VeblenWFInterface.core-wf (identity-interface dec-ψα dec-+2)

readme.adoc

@@ -81,6 +81,7 @@ Ordinal/Buchholz track status:
 ** `<ᵇ-+ω`, `<ᵇ-+ψω`
 ** `<ᵇ-inv-+Ωω`, `<ᵇ-inv-+ψω`
 * `Ordinal.Buchholz.VeblenInterface` now pins a measure-based WF interface with explicit constructor obligations and deferred same-binder obligations (`dec-ψα`, `dec-+2`) for the Veblen-route follow-up.
+* `Ordinal.Buchholz.VeblenIdentityModel` provides a first concrete instantiation of that interface (identity measure bootstrap), with `dec-ψα` / `dec-+2` kept as explicit parameters.
 * Open work remains for general `Ω/+` and `ψ/+` comparisons and for the shared-binder cases (`<ᵇ-ψα`, `<ᵇ-+2`) in a `--without-K`-compatible style.
 
 == External Bridge Targets (local workspace)