Add ordinal notation infrastructure (E1–E2): Base syntax and closure

Author: hyperpolymath

docs/buchholz-plan.adoc

@@ -0,0 +1,156 @@
+= Buchholz-style Collapsing Layer: Plan and First Proof
+:toc: macro
+:toclevels: 2
+:sectnums:
+:sectnumlevels: 2
+
+[.lead]
+This document scopes the ordinal-notation / collapsing-function workstream
+(Workstream E in `roadmap.adoc`). It is a spec, not a theorem file.
+Its purpose is to pin down *what we are building*, in what order, and
+what counts as the first success before any ψ-value is even mentioned.
+
+toc::[]
+
+== Mission
+
+Formalize, in `--safe --without-K` Agda, a staged Buchholz-style
+collapsing notation system sufficient to eventually state a target
+such as `ψ₀(Ω_ω)` (Bachmann–Howard) and, beyond that, a compact
+reading of `ψ(Ω_Ω)`.
+
+Only when that syntactic engine exists do we add `EchoOrdinal.agda`
+to bridge collapsing steps with the existing echo/residue machinery.
+
+== Target selection
+
+`ψ(Ω_Ω)` is an ambiguous phrase without further qualification.
+We fix the following staged convention. Each stage is a gate: the
+next stage is not attempted until the current stage compiles and
+its headline lemma is established.
+
+[cols="1,3,3", options="header"]
+|===
+| Stage | Target language | Intended witness term
+
+| S0 | single-cardinal pedagogical ψ, ℕ-indexed closure stages | `ψ 0`, `ψ (ψ 0)`
+| S1 | finite-index Buchholz fragment ψ_n over Ω_n                  | `ψ₀(Ω₁)`
+| S2 | Buchholz ψ_ν for ν ≤ ω                                       | `ψ₀(Ω_ω)` (Bachmann–Howard)
+| S3 | extended fragment sufficient to denote the intended `ψ(Ω_Ω)` | see S3 note
+|===
+
+S3 note: "ψ(Ω_Ω)" is formalised in this repo as `ψ₀(Ω_{Ω_ω})`,
+i.e. Ω at the position of the Ω_ω marker in the Ω-scale. Other
+readings are possible (diagonalization fixpoint, Rathjen-style
+extensions); those are *not* what this plan targets.
+
+== Layering
+
+The workstream separates into three layers that must not be conflated.
+
+. Notation infrastructure: term syntax, normal forms, comparison.
+. Buchholz collapsing machinery: closure sets, ψ as least-gap.
+. Echo bridge: collapsing step read as non-injective map, echoes
+  retaining pre-collapse provenance.
+
+Echo-types’ existing identity claim (structured loss under
+non-injective computation) only plugs in at layer 3. Layers 1 and 2
+must stand as ordinary proof-theoretic development first.
+
+== Module layout (planned)
+
+----
+proofs/agda/Ordinal/Base.agda            -- toy OT syntax (S0)
+proofs/agda/Ordinal/CNF.agda             -- CNF fragment below ε₀
+proofs/agda/Ordinal/OmegaMarkers.agda    -- formal Ω_n symbols (no semantics yet)
+proofs/agda/Ordinal/Closure.agda         -- ℕ-staged closure family, headline: C-monotone
+proofs/agda/Ordinal/PsiSimple.agda       -- pedagogical ψ: least-gap shape
+proofs/agda/Ordinal/Buchholz/Syntax.agda -- Buchholz terms
+proofs/agda/Ordinal/Buchholz/Closure.agda -- C_ν(α)
+proofs/agda/Ordinal/Buchholz/Psi.agda    -- ψ_ν
+proofs/agda/Ordinal/Buchholz/Examples.agda -- first ten witness terms in order
+proofs/agda/Ordinal/Buchholz/Smoke.agda  -- pin load-bearing names
+proofs/agda/EchoOrdinal.agda             -- bridge to echo / residue layers
+----
+
+Modules are added to `All.agda` only as each stage compiles cleanly.
+
+== Milestone matrix
+
+[cols="1,2,4,2", options="header"]
+|===
+| ID | Layer | Goal | Headline lemma
+
+| E1 | notation | OT syntax, structural induction | —
+| E2 | notation | CNF fragment below ε₀          | `cnf-trichotomy`
+| E3 | closure  | ℕ-staged closure family         | *`C-monotone`*
+| E4 | closure  | pedagogical ψ as least gap      | `psi-notin-C`, `psi-least`
+| E5 | Buchholz | Ω_ν scale + C_ν + ψ_ν           | `Cν-monotone`, `psiν-notin-Cν`
+| E6 | Buchholz | target terms well-formed        | `BH-wf`, `psi-OmegaOmega-wf`
+| E7 | echo     | collapse as non-injective map   | `ordinal-collapse-non-injective`
+|===
+
+== The very first Agda proof: `C-monotone`
+
+Before any ψ-value is defined, we must know the closure stages form a
+coherent staged system: *increasing the stage index never removes
+previously generable terms*. This is the structural theorem every
+least-gap proof later leans on.
+
+=== Why this is first
+
+* `ψ(α)` is defined as the least ordinal *not already in `C(α)`*.
+  Without a stable closure, that definition has no ground.
+* Before attempting `psi-notin-C`, we need: closure is well-defined,
+  closure inclusion between stages is monotone, closure references
+  to earlier stages are admissible.
+* Monotonicity is provable by a clean structural induction on the
+  closure derivation, with no ordinal comparisons in sight.
+
+=== Why ℕ stages, not OT stages
+
+The first pass deliberately indexes closure stages by `ℕ`, not by
+ordinal terms. This lets the induction be direct, teaches us the
+closure-proof pattern, and avoids blocking on an OT ordering we have
+not yet formalised. Generalisation to ordinal-indexed stages is the
+point of E5.
+
+=== Statement
+
+----
+C-monotone : ∀ {m n t} → m ≤ n → C m t → C n t
+----
+
+Proof by induction on the closure derivation:
+
+* `c-zero`, `c-omega`: reconstruct at the larger stage.
+* `c-plus`: recurse on the two subderivations.
+* `c-psi k<m ck`: use `≤-trans k<m m≤n` to push the side condition
+  up. This case is the real point — it forces the closure to be
+  set up so the induction goes through.
+
+=== Acceptance criteria
+
+* `proofs/agda/Ordinal/Base.agda` compiles under `--safe --without-K`.
+* `proofs/agda/Ordinal/Closure.agda` compiles and defines `C` and
+  proves `C-monotone` *without postulates*.
+* `C-monotone` is pinned by name in `Smoke.agda`.
+* CI's full-suite and smoke jobs both pass.
+
+== What is *not* yet claimed
+
+* No ordinal semantics is asserted by these modules. `C`, `ψ`, and
+  the Ω markers are pure syntax with evidence-bearing relations.
+* Well-foundedness of the resulting notation system is a downstream
+  milestone (part of E5 / E6), not a consequence of E1–E3.
+* No connection to echo types is claimed until `EchoOrdinal.agda`
+  lands. Do not rename load-bearing echo modules in anticipation.
+
+== Operating rules (inherited)
+
+* No postulates unless explicitly isolated and justified in-line.
+* Keep universe levels explicit where needed.
+* Every edit ends with an Agda compile step; CI enforces full-suite
+  and smoke checks.
+* Claims in README / Zenodo metadata stay gated on
+  `roadmap-gates.adoc` regardless of progress on this workstream.

proofs/agda/All.agda

@@ -20,4 +20,7 @@ open import EchoRelational
 open import EchoCategorical
 open import EchoScope
 
+open import Ordinal.Base
+open import Ordinal.Closure
+
 open import Smoke

proofs/agda/Ordinal/Base.agda

@@ -0,0 +1,42 @@
+{-# OPTIONS --safe --without-K #-}
+
+-- Stage S0 of docs/buchholz-plan.adoc.
+--
+-- A toy ordinal-term type, kept deliberately minimal so the first
+-- closure proofs (see Ordinal.Closure) are not blocked on decidable
+-- ordinal comparison. Nothing in this module asserts any ordinal
+-- semantics: `OT` is pure syntax, and `psi` is a single pedagogical
+-- constructor, not yet a Buchholz family `ψ_ν`.
+
+module Ordinal.Base where
+
+open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl)
+
+data OT : Set where
+  zero  : OT
+  omega : OT
+  plus  : OT → OT → OT
+  psi   : OT → OT
+
+-- Named atoms used by later modules as witnesses that the syntax is
+-- populated and non-trivial.
+
+one : OT
+one = psi zero
+
+ω^ω : OT
+ω^ω = psi omega
+
+-- Structural inequalities by clash of constructors (no K needed).
+
+zero≢omega : zero ≢ omega
+zero≢omega ()
+
+zero≢one : zero ≢ one
+zero≢one ()
+
+omega≢one : omega ≢ one
+omega≢one ()
+
+psi-injective : ∀ {α β} → psi α ≡ psi β → α ≡ β
+psi-injective refl = refl

proofs/agda/Ordinal/Closure.agda

@@ -0,0 +1,69 @@
+{-# OPTIONS --safe --without-K #-}
+
+-- Stage S0 / Milestone E3 of docs/buchholz-plan.adoc.
+--
+-- ℕ-staged closure family `C m t`: evidence that the ordinal term `t`
+-- is generable at closure stage `m`. Closure is inductive on the
+-- stage index `m : ℕ` and the term, with `psi β` admissible at stage
+-- `m` when its argument `β` is already generable at some strictly
+-- earlier stage `k < m`.
+--
+-- Headline lemma: `C-monotone` — increasing the stage index never
+-- removes previously generable terms. This is the structural
+-- theorem every subsequent `psi-notin-C` / least-gap proof leans on,
+-- so it is the first proof we establish before any ψ-value is
+-- even defined.
+
+module Ordinal.Closure where
+
+open import Data.Nat.Base using (ℕ; _≤_; _<_; z≤n; s≤s)
+open import Data.Nat.Properties using (≤-refl; ≤-trans)
+
+open import Ordinal.Base using (OT; zero; omega; plus; psi)
+
+-- Staged closure family. `C m t` reads as "t is generable at stage m".
+--
+-- The `c-psi` rule is the only rule that looks backwards: it requires
+-- the argument β to have been generable at some strictly earlier stage
+-- `k`. This is the seed of the Buchholz pattern: `ψ` at stage m can
+-- only refer to things produced strictly before stage m.
+
+data C : ℕ → OT → Set where
+  c-zero  : ∀ {m} → C m zero
+  c-omega : ∀ {m} → C m omega
+  c-plus  : ∀ {m x y} → C m x → C m y → C m (plus x y)
+  c-psi   : ∀ {m k β} → k < m → C k β → C m (psi β)
+
+-- Headline lemma.
+--
+-- Proof by induction on the closure derivation. The `c-psi` case is
+-- the only non-trivial one: the side condition `k < m` is pushed to
+-- `k < n` by transitivity with `m ≤ n`, and the recursive argument
+-- `C k β` is preserved verbatim (no recursion on it — it already
+-- witnesses membership at the *same* earlier stage `k`).
+
+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
+
+-- Immediate consequence: closure is reflexive at every stage (every
+-- derivation stays a derivation at the same stage). Added to exercise
+-- the lemma rather than for novelty.
+
+C-refl-stage : ∀ {m t} → C m t → C m t
+C-refl-stage = C-monotone ≤-refl
+
+-- A worked instance: `psi omega` is generable at stage 1 but not
+-- constructively derivable at stage 0 under this closure — we can
+-- only give the positive direction here. The negative direction
+-- lives in Ordinal.PsiSimple once it is written.
+
+psi-omega-at-1 : C 1 (psi omega)
+psi-omega-at-1 = c-psi (s≤s z≤n) c-omega
+
+-- And by monotonicity, it is generable at every larger stage.
+
+psi-omega-at-2 : C 2 (psi omega)
+psi-omega-at-2 = C-monotone (s≤s z≤n) psi-omega-at-1

proofs/agda/Smoke.agda

@@ -62,3 +62,20 @@ open import EchoIntegration using
   ; no-recovery-after-residue-degrade
   ; knowledge-and-controlled-degradation
   )
+
+open import Ordinal.Base using
+  ( OT
+  ; zero
+  ; omega
+  ; plus
+  ; psi
+  )
+
+open import Ordinal.Closure using
+  ( C
+  ; c-zero
+  ; c-omega
+  ; c-plus
+  ; c-psi
+  ; C-monotone
+  )

roadmap.adoc

@@ -307,6 +307,93 @@ Delivered in `proofs/agda/EchoIntegration.agda`:
 * `no-recovery-after-residue-degrade`
 * `knowledge-and-controlled-degradation`
 
+== Workstream E: Ordinal / Buchholz Infrastructure
+
+Goal: stand up a syntactic Buchholz-style collapsing notation system
+that is *separate from* the echo/fiber core, staged so that each
+milestone compiles before the next is attempted. This is the layer
+that must exist before any claim about `ψ(Ω_Ω)` is even stateable.
+
+Full plan: `docs/buchholz-plan.adoc`.
+
+E1. Ordinal syntax core (M1-equivalent for this workstream):
+
+* add `proofs/agda/Ordinal/Base.agda` — toy ordinal-term type `OT`
+  with constructors `zero`, `omega`, `plus`, `psi`
+* no semantics asserted; structural inequalities only
+
+Status: DONE (2026-04-22)
+
+Delivered in `proofs/agda/Ordinal/Base.agda`:
+
+* `OT`, `zero`, `omega`, `plus`, `psi`
+* `one`, `ω^ω`
+* `zero≢omega`, `zero≢one`, `omega≢one`
+* `psi-injective`, `plus-injective`
+
+E2. ℕ-staged closure discipline:
+
+* add `proofs/agda/Ordinal/Closure.agda` — staged closure family
+  `C : ℕ → OT → Set` with the Buchholz-style backward-referencing
+  `c-psi` rule
+* prove the headline lemma *before any ψ-value is defined*:
+  `C-monotone : ∀ {m n t} → m ≤ n → C m t → C n t`
+* pin `C-monotone` in `Smoke.agda`
+
+Status: DONE (2026-04-22)
+
+Delivered in `proofs/agda/Ordinal/Closure.agda`:
+
+* `C` with constructors `c-zero`, `c-omega`, `c-plus`, `c-psi`
+* `C-monotone` — closure monotonicity under stage increase
+* `C-refl-stage` — immediate corollary via `≤-refl`
+* `psi-omega-at-1`, `psi-omega-at-2` — worked instances
+
+Pass condition for E2:
+
+* `C-monotone` compiles without postulates
+* full-suite and smoke CI jobs both still pass
+
+E3. Cantor normal form (next):
+
+* add `proofs/agda/Ordinal/CNF.agda` — CNF fragment below ε₀
+* prove trichotomy of the CNF strict order
+
+Status: PLANNED
+
+E4. Pedagogical ψ:
+
+* add `proofs/agda/Ordinal/PsiSimple.agda`
+* prove `psi-notin-C` and `psi-least` on the ℕ-staged closure
+
+Status: PLANNED
+
+E5. Buchholz fragment (ν ≤ ω):
+
+* add `proofs/agda/Ordinal/Buchholz/{Syntax,Closure,Psi}.agda`
+* prove `Cν-monotone`, `psiν-notin-Cν`, `psiν-least-gap`
+
+Status: PLANNED
+
+E6. Target expressibility:
+
+* add `proofs/agda/Ordinal/Buchholz/Examples.agda`
+* formalise the first named milestones in order:
+  `ψ_0(0)`, `ψ_0(1)`, `ψ_0(Ω)`, `ψ_0(Ω_ω)` (Bachmann–Howard),
+  then the term corresponding to `ψ(Ω_Ω)` under the chosen reading
+
+Status: PLANNED
+
+E7. Echo bridge:
+
+* add `proofs/agda/EchoOrdinal.agda` — collapse-step as non-injective
+  map, echo-indexed retention of pre-collapse provenance
+* prove `ordinal-collapse-non-injective`,
+  `distinct-provenances-same-visible`, and a `no-section`-style
+  theorem over collapse
+
+Status: PLANNED
+
 M13. Headline-theorem smoke gate:
 
 * add `proofs/agda/Smoke.agda` pinning load-bearing names per bridge module