agda: complete E7 echo bridge in EchoOrdinal

Extends the existing `ordinal-collapse-non-injective` scaffold with
the rest of the E7 checklist from `roadmap.adoc`:

* sharper same-Ω-index ψ-argument collapse pair
  (`ordinal-psi-arg-bzero` / `ordinal-psi-arg-omega1`) with
  `ordinal-psi-args-distinct`, `ordinal-psi-arg-collapse-agree`,
  `ordinal-echo-psi-distinct` — two distinct ψ-arguments at Ω₀
  share a visible level but stay distinct as echoes.
* `no-section-ordinal-collapse` — any right-inverse
  `g : OmegaIndex → BT` of `ordinal-collapse` collapses the two
  distinct sources sharing `Omega0` into equality, so no section
  exists.
* `IsZeroSource` + `ordinal-collapse-classification` — classifies
  the `Omega0` preimage into the four BT heads (bzero / bplus /
  bOmega Omega0 / bpsi Omega0).
* `distinct-provenances-same-visible` alias for the existing
  `ordinal-echo-left≢ordinal-echo-right`, matching the roadmap's
  naming.

All pinned in the top-level `Smoke.agda`. Roadmap E7 flipped
PLANNED → DONE with a landed-lemma inventory.

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

Author: hyperpolymath

proofs/agda/EchoOrdinal.agda

@@ -1,26 +1,47 @@
 {-# OPTIONS --safe --without-K #-}
 
--- Stage E7 bridge scaffold for docs/buchholz-plan.adoc.
+-- Stage E7 of docs/buchholz-plan.adoc.
 --
--- Collapse a Buchholz term to a visible Ω-index marker and exhibit
--- non-injectivity at the plain-output level.
+-- Echo bridge for the ordinal notation layer. Reads the map that
+-- sends a Buchholz term to its "visible Ω-level" as a non-injective
+-- map, and shows that echoes retain the discarded structure —
+-- specifically the ψ-argument and the structural head.
+--
+-- The map is syntactic, not a semantic denotation of ψ: every
+-- `bpsi ν α` shares the same visible level ν regardless of the
+-- argument α, so distinct ψ-arguments over the same index appear as
+-- distinct echoes over the shared visible output.
 
 module EchoOrdinal where
 
 open import Echo using (Echo; echo-intro)
 
-open import Data.Product.Base using (Σ; _×_; _,_; proj₁)
-open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl; cong)
+open import Data.Product.Base using (Σ; _×_; _,_; proj₁; proj₂)
+open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
+open import Relation.Binary.PropositionalEquality using
+  (_≡_; _≢_; refl; sym; trans; cong)
+open import Relation.Nullary using (¬_)
 
-open import Ordinal.OmegaMarkers using (OmegaIndex; Omega0)
+open import Ordinal.OmegaMarkers using (OmegaIndex; Omega0; Omega1)
 open import Ordinal.Buchholz.Syntax using (BT; bzero; bOmega; bplus; bpsi)
 
+-- The visible Ω-level of a Buchholz term. `bpsi ν _` exposes ν and
+-- discards the argument; `bplus` is read by its left summand; base
+-- cases fall back to `Omega0`.
+
 ordinal-collapse : BT → OmegaIndex
 ordinal-collapse bzero       = Omega0
 ordinal-collapse (bOmega μ)  = μ
 ordinal-collapse (bplus x y) = ordinal-collapse x
 ordinal-collapse (bpsi μ α)  = μ
 
+----------------------------------------------------------------------------
+-- Non-injectivity
+----------------------------------------------------------------------------
+
+-- Two distinct sources sharing the same visible Ω-level Omega0:
+-- one is the bare marker, the other is a ψ-term at index Ω₀.
+
 ordinal-left : BT
 ordinal-left = bOmega Omega0
 
@@ -35,6 +56,10 @@ ordinal-collapse-non-injective :
 ordinal-collapse-non-injective =
   ordinal-left , ordinal-right , ordinal-left≢ordinal-right , refl
 
+----------------------------------------------------------------------------
+-- Echoes retain pre-collapse provenance
+----------------------------------------------------------------------------
+
 ordinal-echo-left : Echo ordinal-collapse Omega0
 ordinal-echo-left = echo-intro ordinal-collapse ordinal-left
 
@@ -43,3 +68,78 @@ ordinal-echo-right = echo-intro ordinal-collapse ordinal-right
 
 ordinal-echo-left≢ordinal-echo-right : ordinal-echo-left ≢ ordinal-echo-right
 ordinal-echo-left≢ordinal-echo-right p = ordinal-left≢ordinal-right (cong proj₁ p)
+
+-- Shared alias matching the roadmap's naming of this theorem.
+
+distinct-provenances-same-visible : ordinal-echo-left ≢ ordinal-echo-right
+distinct-provenances-same-visible = ordinal-echo-left≢ordinal-echo-right
+
+-- Sharper example: two ψ-terms at the SAME Ω-index but with distinct
+-- ψ-arguments both land on the same visible level. This is the
+-- provenance-loss case that motivates the echo framing — the
+-- ψ-argument is exactly the collapsed data.
+
+ordinal-psi-arg-bzero : BT
+ordinal-psi-arg-bzero = bpsi Omega0 bzero
+
+ordinal-psi-arg-omega1 : BT
+ordinal-psi-arg-omega1 = bpsi Omega0 (bOmega Omega1)
+
+ordinal-psi-args-distinct :
+  ordinal-psi-arg-bzero ≢ ordinal-psi-arg-omega1
+ordinal-psi-args-distinct ()
+
+ordinal-psi-arg-collapse-agree :
+  ordinal-collapse ordinal-psi-arg-bzero ≡ ordinal-collapse ordinal-psi-arg-omega1
+ordinal-psi-arg-collapse-agree = refl
+
+ordinal-echo-psi-bzero : Echo ordinal-collapse Omega0
+ordinal-echo-psi-bzero = echo-intro ordinal-collapse ordinal-psi-arg-bzero
+
+ordinal-echo-psi-omega1 : Echo ordinal-collapse Omega0
+ordinal-echo-psi-omega1 = echo-intro ordinal-collapse ordinal-psi-arg-omega1
+
+ordinal-echo-psi-distinct :
+  ordinal-echo-psi-bzero ≢ ordinal-echo-psi-omega1
+ordinal-echo-psi-distinct p =
+  ordinal-psi-args-distinct (cong proj₁ p)
+
+----------------------------------------------------------------------------
+-- No section through the collapse
+----------------------------------------------------------------------------
+
+-- The plain visible level cannot reconstruct the source: any
+-- right-inverse `g : OmegaIndex → BT` of `ordinal-collapse` would
+-- have to send the shared image `Omega0` back to a single source,
+-- but two distinct sources share that image.
+
+no-section-ordinal-collapse :
+  ¬ (Σ (OmegaIndex → BT) (λ g → ∀ t → g (ordinal-collapse t) ≡ t))
+no-section-ordinal-collapse (g , sec) =
+  ordinal-left≢ordinal-right
+    (trans (sym (sec ordinal-left)) (sec ordinal-right))
+
+----------------------------------------------------------------------------
+-- Preimage classification at Omega0
+----------------------------------------------------------------------------
+
+-- Any Buchholz term whose collapse is `Omega0` is structurally one of
+-- four cases, pinning the "visible = Omega0" preimage into a tractable
+-- classification. This is the echo-theoretic counterpart of
+-- `collapse-classification` from `EchoCharacteristic`, applied to the
+-- syntactic ordinal layer.
+
+IsZeroSource : BT → Set
+IsZeroSource t = t ≡ bzero
+              ⊎ (Σ BT (λ x → Σ BT (λ y → t ≡ bplus x y)))
+              ⊎ t ≡ bOmega Omega0
+              ⊎ (Σ BT (λ α → t ≡ bpsi Omega0 α))
+
+ordinal-collapse-classification :
+  ∀ (e : Echo ordinal-collapse Omega0) → IsZeroSource (proj₁ e)
+ordinal-collapse-classification (bzero , _)      = inj₁ refl
+ordinal-collapse-classification (bOmega μ , refl) = inj₂ (inj₂ (inj₁ refl))
+ordinal-collapse-classification (bplus x y , _)  =
+  inj₂ (inj₁ (x , y , refl))
+ordinal-collapse-classification (bpsi μ α , refl) =
+  inj₂ (inj₂ (inj₂ (α , refl)))

proofs/agda/Smoke.agda

@@ -87,6 +87,17 @@ open import EchoOrdinal using
   ; ordinal-echo-left
   ; ordinal-echo-right
   ; ordinal-echo-left≢ordinal-echo-right
+  ; distinct-provenances-same-visible
+  ; ordinal-psi-arg-bzero
+  ; ordinal-psi-arg-omega1
+  ; ordinal-psi-args-distinct
+  ; ordinal-psi-arg-collapse-agree
+  ; ordinal-echo-psi-bzero
+  ; ordinal-echo-psi-omega1
+  ; ordinal-echo-psi-distinct
+  ; no-section-ordinal-collapse
+  ; IsZeroSource
+  ; ordinal-collapse-classification
   )
 
 open import Ordinal.Base using

roadmap.adoc

@@ -426,7 +426,22 @@ E7. Echo bridge:
   `distinct-provenances-same-visible`, and a `no-section`-style
   theorem over collapse
 
-Status: PLANNED
+Status: DONE (2026-04-24)
+
+Delivered in `proofs/agda/EchoOrdinal.agda`:
+
+* `ordinal-collapse : BT → OmegaIndex` — syntactic visible-level map
+* `ordinal-collapse-non-injective`
+* `ordinal-echo-left`, `ordinal-echo-right`,
+  `ordinal-echo-left≢ordinal-echo-right`
+  (aliased as `distinct-provenances-same-visible`)
+* sharper same-Ω-index ψ-argument collapse:
+  `ordinal-psi-arg-bzero`, `ordinal-psi-arg-omega1`,
+  `ordinal-psi-args-distinct`, `ordinal-psi-arg-collapse-agree`,
+  `ordinal-echo-psi-distinct`
+* `no-section-ordinal-collapse` — no right-inverse to collapse
+* `IsZeroSource`, `ordinal-collapse-classification` —
+  Omega0-preimage classification into the four BT heads
 
 M13. Headline-theorem smoke gate: