From 4ee86b679c1359063fd8fcf5df65eb0511484dae Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Wed, 22 Apr 2026 13:39:07 +0100
Subject: [PATCH] =?UTF-8?q?Scaffold=20E5=20Buchholz=20modules=20with=20?=
 =?UTF-8?q?=CE=BD-indexed=20closure?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 proofs/agda/All.agda                      |  4 +++
 proofs/agda/Ordinal/Buchholz/Closure.agda | 30 ++++++++++++++++++++++
 proofs/agda/Ordinal/Buchholz/Psi.agda     | 25 ++++++++++++++++++
 proofs/agda/Ordinal/Buchholz/Syntax.agda  | 22 ++++++++++++++++
 proofs/agda/Ordinal/OmegaMarkers.agda     | 24 ++++++++++++++++++
 proofs/agda/Smoke.agda                    | 31 +++++++++++++++++++++++
 6 files changed, 136 insertions(+)
 create mode 100644 proofs/agda/Ordinal/Buchholz/Closure.agda
 create mode 100644 proofs/agda/Ordinal/Buchholz/Psi.agda
 create mode 100644 proofs/agda/Ordinal/Buchholz/Syntax.agda
 create mode 100644 proofs/agda/Ordinal/OmegaMarkers.agda

diff --git a/proofs/agda/All.agda b/proofs/agda/All.agda
index 251ff94..9f12024 100644
--- a/proofs/agda/All.agda
+++ b/proofs/agda/All.agda
@@ -24,5 +24,9 @@ open import Ordinal.Base
 open import Ordinal.Closure
 open import Ordinal.CNF
 open import Ordinal.PsiSimple
+open import Ordinal.OmegaMarkers
+open import Ordinal.Buchholz.Syntax
+open import Ordinal.Buchholz.Closure
+open import Ordinal.Buchholz.Psi
 
 open import Smoke
diff --git a/proofs/agda/Ordinal/Buchholz/Closure.agda b/proofs/agda/Ordinal/Buchholz/Closure.agda
new file mode 100644
index 0000000..60d4574
--- /dev/null
+++ b/proofs/agda/Ordinal/Buchholz/Closure.agda
@@ -0,0 +1,30 @@
+{-# OPTIONS --safe --without-K #-}
+
+-- Stage S1/S2 scaffolding for docs/buchholz-plan.adoc.
+--
+-- `Cν ν m t` is the ν-indexed closure family at stage `m` for term
+-- `t`. This is the Buchholz-shaped generalisation of Ordinal.Closure:
+-- closure is still staged by ℕ while carrying an explicit Ω-index
+-- parameter `ν` for future side conditions.
+
+module Ordinal.Buchholz.Closure where
+
+open import Data.Nat.Base using (ℕ; _≤_; _<_)
+open import Data.Nat.Properties using (≤-trans)
+
+open import Ordinal.OmegaMarkers using (OmegaIndex)
+open import Ordinal.Buchholz.Syntax using (BT; bzero; bOmega; bplus; bpsi)
+
+data Cν (ν : OmegaIndex) : ℕ → BT → Set where
+  cν-zero  : ∀ {m} → Cν ν m bzero
+  cν-omega : ∀ {m μ} → Cν ν m (bOmega μ)
+  cν-plus  : ∀ {m x y} → Cν ν m x → Cν ν m y → Cν ν m (bplus x y)
+  cν-psi   : ∀ {m k μ β} → k < m → Cν ν k β → Cν ν m (bpsi μ β)
+
+-- Headline E5 structural lemma: raising the stage keeps derivability.
+
+Cν-monotone : ∀ {ν m n t} → m ≤ n → Cν ν m t → Cν ν n t
+Cν-monotone _   cν-zero          = cν-zero
+Cν-monotone _   cν-omega         = cν-omega
+Cν-monotone m≤n (cν-plus cx cy)  = cν-plus (Cν-monotone m≤n cx) (Cν-monotone m≤n cy)
+Cν-monotone m≤n (cν-psi k<m ck)  = cν-psi (≤-trans k<m m≤n) ck
diff --git a/proofs/agda/Ordinal/Buchholz/Psi.agda b/proofs/agda/Ordinal/Buchholz/Psi.agda
new file mode 100644
index 0000000..9a14482
--- /dev/null
+++ b/proofs/agda/Ordinal/Buchholz/Psi.agda
@@ -0,0 +1,25 @@
+{-# OPTIONS --safe --without-K #-}
+
+-- Stage S1/S2 scaffolding for docs/buchholz-plan.adoc.
+--
+-- First ψ_ν-side exclusion statement over the ν-indexed closure:
+-- no ψ-term can be generated at stage 0 because `cν-psi` requires
+-- a strictly earlier stage witness.
+
+module Ordinal.Buchholz.Psi where
+
+open import Data.Nat.Base using (_≤_; z≤n; s≤s)
+open import Data.Nat.Properties using (≤-trans)
+open import Relation.Nullary using (¬_)
+
+open import Ordinal.OmegaMarkers using (OmegaIndex)
+open import Ordinal.Buchholz.Syntax using (BT; bpsi)
+open import Ordinal.Buchholz.Closure using (Cν; cν-psi)
+
+psiν-notin-Cν : ∀ {ν μ β} → ¬ Cν ν 0 (bpsi μ β)
+psiν-notin-Cν (cν-psi () _)
+
+-- Useful companion: any derivation of `ψ_μ β` lives at stage at least 1.
+
+psiν-stage-lb : ∀ {ν μ β m} → Cν ν m (bpsi μ β) → 1 ≤ m
+psiν-stage-lb (cν-psi k<m _) = ≤-trans (s≤s z≤n) k<m
diff --git a/proofs/agda/Ordinal/Buchholz/Syntax.agda b/proofs/agda/Ordinal/Buchholz/Syntax.agda
new file mode 100644
index 0000000..9d786c6
--- /dev/null
+++ b/proofs/agda/Ordinal/Buchholz/Syntax.agda
@@ -0,0 +1,22 @@
+{-# OPTIONS --safe --without-K #-}
+
+-- Stage S1/S2 scaffolding for docs/buchholz-plan.adoc.
+--
+-- Pure Buchholz-style term syntax over Ω-indices. This module is only
+-- structural syntax; ordering, normal forms, and semantics are staged
+-- in later milestones.
+
+module Ordinal.Buchholz.Syntax where
+
+open import Ordinal.OmegaMarkers using (OmegaIndex; Omega0)
+
+data BT : Set where
+  bzero  : BT
+  bOmega : OmegaIndex → BT
+  bplus  : BT → BT → BT
+  bpsi   : OmegaIndex → BT → BT
+
+-- The common ψ₀ abbreviation.
+
+psi0 : BT → BT
+psi0 α = bpsi Omega0 α
diff --git a/proofs/agda/Ordinal/OmegaMarkers.agda b/proofs/agda/Ordinal/OmegaMarkers.agda
new file mode 100644
index 0000000..e1e984c
--- /dev/null
+++ b/proofs/agda/Ordinal/OmegaMarkers.agda
@@ -0,0 +1,24 @@
+{-# OPTIONS --safe --without-K #-}
+
+-- Stage S1/S2 scaffolding for docs/buchholz-plan.adoc.
+--
+-- Formal Ω-index markers only; no ordinal semantics is claimed here.
+-- Finite markers are represented by `fin n`, and `ω` is the first
+-- limit marker used later by Buchholz syntax.
+
+module Ordinal.OmegaMarkers where
+
+open import Data.Nat.Base using (ℕ; zero; suc)
+
+data OmegaIndex : Set where
+  fin : ℕ → OmegaIndex
+  ω   : OmegaIndex
+
+Omega0 : OmegaIndex
+Omega0 = fin zero
+
+Omega1 : OmegaIndex
+Omega1 = fin (suc zero)
+
+Omegaω : OmegaIndex
+Omegaω = ω
diff --git a/proofs/agda/Smoke.agda b/proofs/agda/Smoke.agda
index 63b9f63..0ccba49 100644
--- a/proofs/agda/Smoke.agda
+++ b/proofs/agda/Smoke.agda
@@ -97,3 +97,34 @@ open import Ordinal.PsiSimple using
   ( psi-notin-C
   ; psi-least
   )
+
+open import Ordinal.OmegaMarkers using
+  ( OmegaIndex
+  ; fin
+  ; ω
+  ; Omega0
+  ; Omega1
+  ; Omegaω
+  )
+
+open import Ordinal.Buchholz.Syntax using
+  ( BT
+  ; bzero
+  ; bOmega
+  ; bplus
+  ; bpsi
+  ; psi0
+  )
+
+open import Ordinal.Buchholz.Closure using
+  ( Cν
+  ; cν-zero
+  ; cν-omega
+  ; cν-plus
+  ; cν-psi
+  ; Cν-monotone
+  )
+
+open import Ordinal.Buchholz.Psi using
+  ( psiν-notin-Cν
+  )