Strengthen E5 closure lemmas and add psi0(Omega1) witness path

Author: hyperpolymath

proofs/agda/Ordinal/Buchholz/Closure.agda

@@ -10,9 +10,10 @@
 module Ordinal.Buchholz.Closure where
 
 open import Data.Nat.Base using (ℕ; _≤_; _<_)
+open import Data.Product.Base using (Σ; _,_; _×_)
 open import Data.Nat.Properties using (≤-trans)
 
-open import Ordinal.OmegaMarkers using (OmegaIndex; _≤Ω_)
+open import Ordinal.OmegaMarkers using (OmegaIndex; _≤Ω_; ≤Ω-trans)
 open import Ordinal.Buchholz.Syntax using (BT; bzero; bOmega; bplus; bpsi)
 
 data Cν (ν : OmegaIndex) : ℕ → BT → Set where
@@ -28,3 +29,27 @@ 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
+
+-- Monotonicity in the Ω-index parameter.
+
+Cν-index-monotone : ∀ {ν ν' m t} → ν ≤Ω ν' → Cν ν m t → Cν ν' m t
+Cν-index-monotone _     cν-zero              = cν-zero
+Cν-index-monotone ν≤ν' (cν-omega μ≤ν)        = cν-omega (≤Ω-trans μ≤ν ν≤ν')
+Cν-index-monotone ν≤ν' (cν-plus cx cy)       = cν-plus (Cν-index-monotone ν≤ν' cx) (Cν-index-monotone ν≤ν' cy)
+Cν-index-monotone ν≤ν' (cν-psi μ≤ν k<m ck)   = cν-psi (≤Ω-trans μ≤ν ν≤ν') k<m (Cν-index-monotone ν≤ν' ck)
+
+-- Combined monotonicity in index and stage.
+
+Cν-monotone-both : ∀ {ν ν' m n t} → ν ≤Ω ν' → m ≤ n → Cν ν m t → Cν ν' n t
+Cν-monotone-both ν≤ν' m≤n ct = Cν-monotone m≤n (Cν-index-monotone ν≤ν' ct)
+
+-- Structural inversion helpers for the indexed constructors.
+
+cν-omega-index : ∀ {ν m μ} → Cν ν m (bOmega μ) → μ ≤Ω ν
+cν-omega-index (cν-omega μ≤ν) = μ≤ν
+
+cν-psi-index : ∀ {ν m μ β} → Cν ν m (bpsi μ β) → μ ≤Ω ν
+cν-psi-index (cν-psi μ≤ν _ _) = μ≤ν
+
+cν-psi-decompose : ∀ {ν m μ β} → Cν ν m (bpsi μ β) → Σ ℕ (λ k → (k < m) × Cν ν k β)
+cν-psi-decompose (cν-psi {k = k} _ k<m ck) = k , (k<m , ck)

proofs/agda/Ordinal/Buchholz/Examples.agda

@@ -7,14 +7,21 @@
 
 module Ordinal.Buchholz.Examples where
 
-open import Data.Nat.Base using (z≤n; s≤s)
+open import Data.Nat.Base using (_≤_; z≤n; s≤s)
 open import Relation.Binary.PropositionalEquality using (_≡_; refl)
 open import Relation.Nullary using (¬_)
 
-open import Ordinal.OmegaMarkers using (Omega0; Omega1; Omegaω; fin≤ω)
+open import Ordinal.OmegaMarkers using
+  ( Omega0
+  ; Omega1
+  ; Omegaω
+  ; ≤Ω-refl
+  ; Omega0≤Omega1
+  ; Omega1≤Omegaω
+  )
 open import Ordinal.Buchholz.Syntax using (BT; bOmega; bpsi; psi0)
-open import Ordinal.Buchholz.Closure using (Cν; cν-omega; cν-psi)
-open import Ordinal.Buchholz.Psi using (psiν-notin-Cν)
+open import Ordinal.Buchholz.Closure using (Cν; cν-omega; cν-psi; Cν-index-monotone)
+open import Ordinal.Buchholz.Psi using (psiν-notin-Cν; psiν-stage-lb)
 
 bh-psi0-omega1 : BT
 bh-psi0-omega1 = bpsi Omega0 (bOmega Omega1)
@@ -25,11 +32,26 @@ bh-psi0-omegaω = bpsi Omega0 (bOmega Omegaω)
 psi0-expands : psi0 (bOmega Omega1) ≡ bh-psi0-omega1
 psi0-expands = refl
 
+psi0-Omega1-target : BT
+psi0-Omega1-target = bh-psi0-omega1
+
+omega1-in-C1-at-0 : Cν Omega1 0 (bOmega Omega1)
+omega1-in-C1-at-0 = cν-omega ≤Ω-refl
+
+psi0-omega1-at-1-in-C1 : Cν Omega1 1 bh-psi0-omega1
+psi0-omega1-at-1-in-C1 = cν-psi Omega0≤Omega1 (s≤s z≤n) omega1-in-C1-at-0
+
+psi0-omega1-not-at-0-in-C1 : ¬ Cν Omega1 0 bh-psi0-omega1
+psi0-omega1-not-at-0-in-C1 = psiν-notin-Cν
+
+psi0-omega1-stage-lb-in-C1 : ∀ {m} → Cν Omega1 m bh-psi0-omega1 → 1 ≤ m
+psi0-omega1-stage-lb-in-C1 = psiν-stage-lb
+
 omega1-in-Cω-at-0 : Cν Omegaω 0 (bOmega Omega1)
-omega1-in-Cω-at-0 = cν-omega fin≤ω
+omega1-in-Cω-at-0 = Cν-index-monotone Omega1≤Omegaω omega1-in-C1-at-0
 
 psi0-omega1-at-1 : Cν Omegaω 1 bh-psi0-omega1
-psi0-omega1-at-1 = cν-psi fin≤ω (s≤s z≤n) omega1-in-Cω-at-0
+psi0-omega1-at-1 = Cν-index-monotone Omega1≤Omegaω psi0-omega1-at-1-in-C1
 
 psi0-omega1-not-at-0 : ¬ Cν Omegaω 0 bh-psi0-omega1
 psi0-omega1-not-at-0 = psiν-notin-Cν

proofs/agda/Ordinal/Buchholz/Psi.agda

@@ -12,9 +12,9 @@ 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.OmegaMarkers using (OmegaIndex; _≤Ω_)
 open import Ordinal.Buchholz.Syntax using (BT; bpsi)
-open import Ordinal.Buchholz.Closure using (Cν; cν-psi)
+open import Ordinal.Buchholz.Closure using (Cν; cν-psi; cν-psi-index)
 
 psiν-notin-Cν : ∀ {ν μ β} → ¬ Cν ν 0 (bpsi μ β)
 psiν-notin-Cν (cν-psi _ () _)
@@ -23,3 +23,6 @@ psiν-notin-Cν (cν-psi _ () _)
 
 psiν-stage-lb : ∀ {ν μ β m} → Cν ν m (bpsi μ β) → 1 ≤ m
 psiν-stage-lb (cν-psi _ k<m _) = ≤-trans (s≤s z≤n) k<m
+
+psiν-index-bound : ∀ {ν μ β m} → Cν ν m (bpsi μ β) → μ ≤Ω ν
+psiν-index-bound = cν-psi-index

proofs/agda/Ordinal/Buchholz/Smoke.agda

@@ -18,6 +18,9 @@ open import Ordinal.OmegaMarkers using
   ; Omega0
   ; Omega1
   ; Omegaω
+  ; Omega0≤Omega1
+  ; Omega0≤Omegaω
+  ; Omega1≤Omegaω
   )
 
 open import Ordinal.Buchholz.Syntax using
@@ -36,17 +39,28 @@ open import Ordinal.Buchholz.Closure using
   ; cν-plus
   ; cν-psi
   ; Cν-monotone
+  ; Cν-index-monotone
+  ; Cν-monotone-both
+  ; cν-omega-index
+  ; cν-psi-index
+  ; cν-psi-decompose
   )
 
 open import Ordinal.Buchholz.Psi using
   ( psiν-notin-Cν
   ; psiν-stage-lb
+  ; psiν-index-bound
   )
 
 open import Ordinal.Buchholz.Examples using
   ( bh-psi0-omega1
   ; bh-psi0-omegaω
   ; psi0-expands
+  ; psi0-Omega1-target
+  ; omega1-in-C1-at-0
+  ; psi0-omega1-at-1-in-C1
+  ; psi0-omega1-not-at-0-in-C1
+  ; psi0-omega1-stage-lb-in-C1
   ; omega1-in-Cω-at-0
   ; psi0-omega1-at-1
   ; psi0-omega1-not-at-0

proofs/agda/Ordinal/OmegaMarkers.agda

@@ -8,7 +8,7 @@
 
 module Ordinal.OmegaMarkers where
 
-open import Data.Nat.Base using (ℕ; _≤_; zero; suc)
+open import Data.Nat.Base using (ℕ; _≤_; z≤n; s≤s; zero; suc)
 open import Data.Nat.Properties using (≤-refl; ≤-trans)
 
 data OmegaIndex : Set where
@@ -44,3 +44,12 @@ Omega1 = fin (suc zero)
 
 Omegaω : OmegaIndex
 Omegaω = ω
+
+Omega0≤Omega1 : Omega0 ≤Ω Omega1
+Omega0≤Omega1 = fin≤fin z≤n
+
+Omega0≤Omegaω : Omega0 ≤Ω Omegaω
+Omega0≤Omegaω = fin≤ω
+
+Omega1≤Omegaω : Omega1 ≤Ω Omegaω
+Omega1≤Omegaω = fin≤ω

proofs/agda/Smoke.agda

@@ -111,6 +111,9 @@ open import Ordinal.OmegaMarkers using
   ; Omega0
   ; Omega1
   ; Omegaω
+  ; Omega0≤Omega1
+  ; Omega0≤Omegaω
+  ; Omega1≤Omegaω
   )
 
 open import Ordinal.Buchholz.Syntax using
@@ -129,16 +132,28 @@ open import Ordinal.Buchholz.Closure using
   ; cν-plus
   ; cν-psi
   ; Cν-monotone
+  ; Cν-index-monotone
+  ; Cν-monotone-both
+  ; cν-omega-index
+  ; cν-psi-index
+  ; cν-psi-decompose
   )
 
 open import Ordinal.Buchholz.Psi using
   ( psiν-notin-Cν
+  ; psiν-stage-lb
+  ; psiν-index-bound
   )
 
 open import Ordinal.Buchholz.Examples using
   ( bh-psi0-omega1
   ; bh-psi0-omegaω
   ; psi0-expands
+  ; psi0-Omega1-target
+  ; omega1-in-C1-at-0
+  ; psi0-omega1-at-1-in-C1
+  ; psi0-omega1-not-at-0-in-C1
+  ; psi0-omega1-stage-lb-in-C1
   ; omega1-in-Cω-at-0
   ; psi0-omega1-at-1
   ; psi0-omega1-not-at-0