agda: make CNO echo bridge relation-first

Author: hyperpolymath

absolute-zero/README.adoc

@@ -211,7 +211,7 @@ Agda bridge note:
 
 * `proofs/agda/EchoBridgeScaffold.agda` is now present as a compile-safe adapter layer to connect CNO identity witnesses to the echo/fiber shape used in `echo-types`.
 * `proofs/agda/EchoBridgeCNO.agda` now provides a concrete `Program`/`eval` model instantiation into that scaffold.
-* This concrete bridge currently uses a function-extensionality parameter to convert `state-eq` into propositional equality for `Echo`.
+* The concrete bridge now exposes relation-based echoes over `state-eq` directly; function extensionality is only used for optional propositional `Echo` corollaries.
 
 **Coq Proof Status** (2026-02-05): 81 Qed / 19 Admitted / 6 Defined / 63 Axioms across 10 files. 4 files fully complete (CNO.v, CNOCategory.v, StatMech.v, StatMech_helpers.v).
 

absolute-zero/proofs/agda/EchoBridgeCNO.agda

@@ -1,7 +1,7 @@
 -- Concrete Echo/CNO instantiation against CNO.Program and CNO.eval.
 --
--- Note: CNO identity is phrased as state-eq, so we parameterize by
--- function extensionality to recover propositional equality of states.
+-- Primary bridge: use CNO.state-eq directly as the relation in EchoRel.
+-- Secondary bridge: recover propositional equality with extensionality.
 
 module EchoBridgeCNO where
 
@@ -11,7 +11,28 @@ open import Relation.Binary.PropositionalEquality using (_≡_; refl)
 open import Axiom.Extensionality.Propositional using (Extensionality)
 
 import CNO
-open import EchoBridgeScaffold using (CNOModel; Echo; echo-from-cno)
+open import EchoBridgeScaffold using
+  ( CNOModel
+  ; Echo
+  ; EchoRel
+  ; echo-from-cno
+  ; echo-from-rel
+  )
+
+echo-from-cno-program-rel :
+  (p : CNO.Program) →
+  CNO.IsCNO p →
+  (s : CNO.ProgramState) →
+  EchoRel (CNO.eval p) CNO.state-eq s
+echo-from-cno-program-rel p cno s =
+  echo-from-rel (CNO.eval p) CNO.state-eq s s
+    (CNO.IsCNO.cno-identity cno s)
+
+absolute-zero-echo-rel :
+  (s : CNO.ProgramState) →
+  EchoRel (CNO.eval CNO.absolute-zero) CNO.state-eq s
+absolute-zero-echo-rel s =
+  echo-from-cno-program-rel CNO.absolute-zero CNO.absolute-zero-is-cno s
 
 state-eq→≡ :
   Extensionality zero zero →
@@ -30,18 +51,18 @@ program-state-model ext = record
       state-eq→≡ ext (CNO.IsCNO.cno-identity cno s)
   }
 
-echo-from-cno-program :
+echo-from-cno-program-≡ :
   (ext : Extensionality zero zero) →
   (p : CNO.Program) →
   CNO.IsCNO p →
   (s : CNO.ProgramState) →
   Echo (CNO.eval p) s
-echo-from-cno-program ext p cno s =
+echo-from-cno-program-≡ ext p cno s =
   echo-from-cno (program-state-model ext) p cno s
 
-absolute-zero-echo :
+absolute-zero-echo-≡ :
   (ext : Extensionality zero zero) →
   (s : CNO.ProgramState) →
   Echo (CNO.eval CNO.absolute-zero) s
-absolute-zero-echo ext s =
-  echo-from-cno-program ext CNO.absolute-zero CNO.absolute-zero-is-cno s
+absolute-zero-echo-≡ ext s =
+  echo-from-cno-program-≡ ext CNO.absolute-zero CNO.absolute-zero-is-cno s

absolute-zero/proofs/agda/EchoBridgeScaffold.agda

@@ -16,6 +16,21 @@ open import Agda.Builtin.Unit using (⊤; tt)
 Echo : ∀ {a b} {A : Set a} {B : Set b} → (A → B) → B → Set (a ⊔ b)
 Echo {A = A} f y = Σ A (λ x → f x ≡ y)
 
+-- Relation-indexed fiber shape, useful when identity is stated up to
+-- a semantic relation instead of propositional equality.
+EchoRel :
+  ∀ {a b r} {A : Set a} {B : Set b} →
+  (A → B) → (B → B → Set r) → B → Set (a ⊔ r)
+EchoRel {A = A} f _≈_ y = Σ A (λ x → _≈_ (f x) y)
+
+echo-from-rel :
+  ∀ {a b r} {A : Set a} {B : Set b}
+  (f : A → B) (_≈_ : B → B → Set r)
+  (x : A) (y : B) →
+  _≈_ (f x) y →
+  EchoRel f _≈_ y
+echo-from-rel _ _ x _ rel = x , rel
+
 -- Minimal interface needed to connect a CNO model to echoes.
 record CNOModel {ℓs ℓo : Level} (State : Set ℓs) : Set (lsuc (ℓs ⊔ ℓo)) where
   field

absolute-zero/proofs/agda/README.adoc

@@ -26,8 +26,10 @@ This module imports `CNO.agda` and instantiates `CNOModel` concretely with:
 * `IsCNO = IsCNO`
 
 Because `CNO.cno-identity` is phrased as `state-eq` (with function-valued memory),
-the bridge takes a function-extensionality parameter to derive propositional
-state equality for `Echo`.
+the bridge provides two layers:
+
+* primary: relation-based echoes via `EchoRel ... CNO.state-eq` (no extensionality needed);
+* secondary: propositional `Echo` corollaries via a function-extensionality parameter.
 
 == Integration plan