agda: add psiν-at-succ + psiν-least-gap, closing E5

Lands the two missing Buchholz-ν analogues of `psi-at-1` / `psi-least`
from `Ordinal.PsiSimple`:

* `psiν-at-succ {ν μ β k} : μ ≤Ω ν → Cν ν k β → Cν ν (suc k) (bpsi μ β)`
  — constructive entry: once `β` is generable at stage `k` with the
  Ω-index side-condition met, `bpsi μ β` enters closure exactly one
  stage later.
* `psiν-least-gap {ν μ β m} : Cν ν m (bpsi μ β) → Σ k, suc k ≤ m × Cν ν k β`
  — least-gap decomposition. Delegates to the existing
  `cν-psi-decompose` but under the least-gap name matching the
  roadmap plan.

Paired, these pin the minimal entry stage of `bpsi μ β` at exactly
one above the minimal entry stage of its argument.

Pinned in both `Ordinal.Buchholz.Smoke` and the top-level `Smoke`.
Roadmap E5 flipped PARTIAL → DONE.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

proofs/agda/Ordinal/Buchholz/Psi.agda

@@ -2,19 +2,20 @@
 
 -- 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.
+-- Least-gap shape for the Buchholz ψ_ν constructor, mirroring the
+-- pedagogical `psi-notin-C` / `psi-at-1` / `psi-least` triple in
+-- `Ordinal.PsiSimple` but parameterised by the Ω-index ν.
 
 module Ordinal.Buchholz.Psi where
 
-open import Data.Nat.Base using (_≤_; z≤n; s≤s)
-open import Data.Nat.Properties using (≤-trans)
+open import Data.Nat.Base using (ℕ; suc; _≤_; _<_; z≤n; s≤s)
+open import Data.Nat.Properties using (≤-refl; ≤-trans)
+open import Data.Product.Base using (Σ; _,_; _×_)
 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; cν-psi-index)
+open import Ordinal.Buchholz.Closure using (Cν; cν-psi; cν-psi-index; cν-psi-decompose)
 
 psiν-notin-Cν : ∀ {ν μ β} → ¬ Cν ν 0 (bpsi μ β)
 psiν-notin-Cν (cν-psi _ () _)
@@ -26,3 +27,19 @@ 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
+
+-- Constructive entry (analogue of `psi-at-1`): once `β` is generable
+-- at stage `k` and the Ω-index side-condition `μ ≤Ω ν` holds,
+-- `bpsi μ β` enters the closure one stage later.
+
+psiν-at-succ : ∀ {ν μ β k} → μ ≤Ω ν → Cν ν k β → Cν ν (suc k) (bpsi μ β)
+psiν-at-succ μ≤ν ck = cν-psi μ≤ν ≤-refl ck
+
+-- Least-gap shape (analogue of `psi-least`): any stage `m` that
+-- derives `bpsi μ β` decomposes into a strictly earlier stage `k`
+-- (i.e. `suc k ≤ m`) at which `β` was already derivable. Paired with
+-- `psiν-at-succ` this pins the minimal entry stage of `bpsi μ β` at
+-- exactly one above the minimal entry stage of its argument.
+
+psiν-least-gap : ∀ {ν μ β m} → Cν ν m (bpsi μ β) → Σ ℕ (λ k → (suc k ≤ m) × Cν ν k β)
+psiν-least-gap = cν-psi-decompose

proofs/agda/Ordinal/Buchholz/Smoke.agda

@@ -78,6 +78,8 @@ open import Ordinal.Buchholz.Psi using
   ( psiν-notin-Cν
   ; psiν-stage-lb
   ; psiν-index-bound
+  ; psiν-at-succ
+  ; psiν-least-gap
   )
 
 open import Ordinal.Buchholz.Examples using

proofs/agda/Smoke.agda

@@ -213,6 +213,8 @@ open import Ordinal.Buchholz.Psi using
   ( psiν-notin-Cν
   ; psiν-stage-lb
   ; psiν-index-bound
+  ; psiν-at-succ
+  ; psiν-least-gap
   )
 
 open import Ordinal.Buchholz.Examples using

roadmap.adoc

@@ -393,18 +393,14 @@ E5. Buchholz fragment (ν ≤ ω):
 * add `proofs/agda/Ordinal/Buchholz/{Syntax,Closure,Psi}.agda`
 * prove `Cν-monotone`, `psiν-notin-Cν`, `psiν-least-gap`
 
-Status: PARTIAL (2026-04-24)
+Status: DONE (2026-04-24)
 
-Delivered:
+Delivered in `proofs/agda/Ordinal/Buchholz/{Closure, Psi}.agda`:
 
-* `Ordinal/Buchholz/Syntax.agda`, `Closure.agda`, `Psi.agda` all compile
 * `Cν-monotone`, `Cν-index-monotone`, `Cν-monotone-both`
 * `psiν-notin-Cν`, `psiν-stage-lb`, `psiν-index-bound`
-
-Still open:
-
-* `psiν-least-gap` — the stronger least-gap theorem (stage-lb gives `1 ≤ m`;
-  least-gap gives the sharper minimal-stage side).
+* `psiν-at-succ` — constructive entry at stage `suc k` from `Cν ν k β`
+* `psiν-least-gap` — least-gap decomposition `(k, suc k ≤ m, Cν ν k β)`
 
 E6. Target expressibility: