Scaffold E5 Buchholz modules with ν-indexed closure

Author: hyperpolymath

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

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

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

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 α

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ω = ω

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ν
+  )