feat(proofs/agda): upstream Echo/CNO bridge files from maa-framework vendored copy

docs/proof-debt.md

@@ -334,6 +334,21 @@ the bottom.
 4. The `check-trusted-base` CI job (standards#211) ensures markers
    are never un-annotated AND un-enumerated simultaneously.
 
+## False positives (no markers; script over-matches)
+
+### `proofs/agda/EchoBridgeCNO.agda` — `Axiom.Extensionality` import
+
+`check-trusted-base.sh`'s grep matches the line
+`open import Axiom.Extensionality.Propositional using (Extensionality)`
+at L11 as if it were an axiom declaration. It is not — it imports the
+`Extensionality` type, which is then accepted as an *explicit module
+parameter* by every downstream function that needs it
+(`program-state-model`, `program-rel-bridge`, etc.). The file
+introduces zero postulates and zero axioms; extensionality is
+propagated from the caller as a hypothesis.
+
+Listed here to satisfy the script's path-enumeration clause.
+
 ## Companion documents
 
 - [standards#195](https://github.com/hyperpolymath/standards/pull/195) — estate proof-debt audit.

proofs/agda/EchoBridgeCNO.agda

@@ -0,0 +1,68 @@
+-- Concrete Echo/CNO instantiation against CNO.Program and CNO.eval.
+--
+-- Primary bridge: use CNO.state-eq directly as the relation in EchoRel.
+-- Secondary bridge: recover propositional equality with extensionality.
+
+module EchoBridgeCNO where
+
+open import Level using (zero)
+open import Data.Product using (_,_)
+open import Relation.Binary.PropositionalEquality using (_≡_; refl)
+open import Axiom.Extensionality.Propositional using (Extensionality)
+
+import 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 →
+  ∀ {s₁ s₂ : CNO.ProgramState} →
+  CNO.state-eq s₁ s₂ → s₁ ≡ s₂
+state-eq→≡ ext {CNO.mk-state m₁ r₁ i₁ pc₁} {CNO.mk-state m₂ r₂ i₂ pc₂}
+             (m-eq , r-eq , io-eq , pc-eq)
+  rewrite ext m-eq | r-eq | io-eq | pc-eq = refl
+
+program-state-model : Extensionality zero zero → CNOModel CNO.ProgramState
+program-state-model ext = record
+  { Op = CNO.Program
+  ; run = CNO.eval
+  ; IsCNO = CNO.IsCNO
+  ; cno-identity = λ cno s →
+      state-eq→≡ ext (CNO.IsCNO.cno-identity cno s)
+  }
+
+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-state-model ext) p cno s
+
+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

proofs/agda/EchoBridgeScaffold.agda

@@ -0,0 +1,62 @@
+{-# OPTIONS --safe --without-K #-}
+
+-- Echo/CNO Agda bridge scaffold.
+--
+-- This module is intentionally independent from `CNO.agda` so it can
+-- stay typecheckable while that file is still being completed.
+
+module EchoBridgeScaffold where
+
+open import Agda.Primitive using (Level; lsuc; _⊔_)
+open import Agda.Builtin.Equality using (_≡_; refl)
+open import Agda.Builtin.Sigma using (Σ; _,_)
+open import Agda.Builtin.Unit using (⊤; tt)
+
+-- Canonical echo/fiber shape used by echo-types.
+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
+    Op           : Set ℓo
+    run          : Op → State → State
+    IsCNO        : Op → Set (ℓs ⊔ ℓo)
+    cno-identity : ∀ {op} → IsCNO op → (s : State) → run op s ≡ s
+
+open CNOModel public
+
+-- Any CNO witness yields an echo at any visible state.
+echo-from-cno :
+  ∀ {ℓs ℓo} {State : Set ℓs}
+  (M : CNOModel {ℓs} {ℓo} State)
+  (op : Op M) → IsCNO M op →
+  (s : State) → Echo (run M op) s
+echo-from-cno M op cno s = s , cno-identity M cno s
+
+-- A tiny closed model kept here as a local smoke witness.
+TrivialModel : CNOModel ⊤
+TrivialModel = record
+  { Op = ⊤
+  ; run = λ _ s → s
+  ; IsCNO = λ _ → ⊤
+  ; cno-identity = λ _ _ → refl
+  }
+
+trivial-echo : Echo (run TrivialModel tt) tt
+trivial-echo = echo-from-cno TrivialModel tt tt tt

proofs/agda/README.adoc

@@ -0,0 +1,38 @@
+= Agda Proofs (absolute-zero)
+
+This directory currently contains:
+
+* `CNO.agda` — main Agda CNO development (compiles locally).
+* `EchoBridgeScaffold.agda` — compile-safe interface layer for bridging CNO identity witnesses to the echo/fiber shape used in `echo-types`.
+* `EchoBridgeCNO.agda` — concrete model instantiation from `CNO.Program` / `eval` into the scaffold interface.
+
+== Purpose of `EchoBridgeScaffold.agda`
+
+The scaffold avoids importing `CNO.agda` directly so this bridge path can
+remain typecheckable while `CNO.agda` is still being completed.
+
+It provides:
+
+* `Echo` as `Σ x , f x ≡ y`.
+* `CNOModel` interface with `run`, `IsCNO`, and `cno-identity`.
+* `echo-from-cno` conversion from a CNO witness to an echo witness.
+
+== Purpose of `EchoBridgeCNO.agda`
+
+This module imports `CNO.agda` and instantiates `CNOModel` concretely with:
+
+* `Op = Program`
+* `run = eval`
+* `IsCNO = IsCNO`
+
+Because `CNO.cno-identity` is phrased as `state-eq` (with function-valued memory),
+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
+
+1. Add reciprocal consistency checks against:
+* `echo-types` (`proofs/agda/EchoCNOBridge.agda`)
+* this repository's Coq/Lean CNO statements.