Add echos exploration: fibre accounting draft (unverified), design no…

docs/echos/BOT-PROMPT.adoc

@@ -0,0 +1,80 @@
+// SPDX-License-Identifier: MPL-2.0
+= Investigation brief: echo-based fidelity for autoformalisation
+
+Paste the section below into a bot tied to the `echo-types` repository on
+branch `arena/93ae4ce1-echo-types`. Work only on that branch.
+
+== Prompt
+
+____
+You are investigating whether echo types (fibres with witnesses) can help
+assure fidelity of autoformalisation: the step where an informal or source
+statement is translated into a formal statement that a proof checker accepts.
+
+Context you must read first:
+
+* `docs/echos/README.adoc` (scope, status, ground truth)
+* `docs/echos/FIDELITY-FIBRE-DESIGN.adoc` (design and what is not claimed)
+* `proofs/agda/EchoFidelity.agda` (draft model, NOT yet type-checked)
+* `proofs/agda/EchoEpistemic.agda` (existing knowledge/observation model)
+* `docs/CLAIMS_AUDIT.adoc` (how this repo audits its own claims)
+
+Core question: if the fibre of each target atom is traceable to its source
+atoms, does that help assure that the translation preserved what matters?
+
+Tasks, in order:
+
+1. *Type-check the draft.* Attempt to type-check `EchoFidelity.agda` with the
+   same Agda version and standard library the repo uses (see
+   `echo-types.agda-lib` and the version noted in `EXPLAINME.adoc`). Fix only
+   errors that are syntactic or type-level. Do not change claims. Report the
+   exact errors and fixes. If Agda is unavailable, say so and stop this task.
+
+2. *Test the claims in the design note.* For each claim in
+   `FIDELITY-FIBRE-DESIGN.adoc` section "What the types buy", state whether
+   it is (a) enforced by the type, (b) a definitional consequence, or
+   (c) only a convention. Give evidence for each.
+
+3. *Check the direction example.* Confirm that `cmp 4 5 ≡ weaker` reflects the
+   stated convention (smaller parameter = stronger claim). Then construct one
+   more example of your own from a different domain (for example, a hypothesis
+   that is added, or a bound that is tightened) and encode it. Say whether the
+   convention generalises or needs more structure.
+
+4. *Stress-test the checker/auditor split.* Write down a concrete pair of
+   translations with identical target atoms and different fibres. Show that a
+   checker's observation is identical, and that the auditor can tell them
+   apart. Then describe one case where the auditor's view is still not enough.
+
+5. *Survey the surrounding tools (read-only).* In the sibling repositories
+   `echidna`, `echidnabot`, and `proof-burrower`, identify any place where a
+   source-to-target mapping could be recorded. Use the existing content-ID
+   scheme (`echidna/src/rust/ids.rs`) as a candidate. Do not modify those
+   repositories. Report file paths and line references.
+
+6. *Propose, do not implement, a persistence format.* Sketch the minimal record
+   needed to store a fibre alongside a proof receipt. Keep it to fields and
+   invariants. Put it in `docs/echos/FIBRE-RECORD-PROPOSAL.adoc`.
+
+Rules:
+
+* Label every statement as VERIFIED (you ran it), READ (you read the code), or
+  INFERRED (reasoning only). Do not present inferred results as verified.
+* Do not claim fidelity is established. The output is about structure and
+  assurance layers, not about whether any particular theorem is correct.
+* Do not wire `EchoFidelity.agda` into `All.agda` or `Smoke.agda` unless every
+  check passes and the user asks for it.
+* Keep changes to `docs/echos/` and `proofs/agda/EchoFidelity.agda` unless a
+  task requires otherwise. Explain any other file you touch.
+* Commit to `arena/93ae4ce1-echo-types` only.
+
+Deliverable: a short report at `docs/echos/INVESTIGATION-REPORT.adoc` with one
+section per task, the labels above, and a list of open questions.
+____
+
+== Notes for the person running the bot
+
+* The bot's output is a structured exploration, not a verdict on any
+  autoformalisation result.
+* If the bot reports that Agda cannot be run, treat task 1 as open, and do not
+  let later tasks rely on the draft compiling.

docs/echos/FIDELITY-FIBRE-DESIGN.adoc

@@ -0,0 +1,79 @@
+// SPDX-License-Identifier: MPL-2.0
+= Fibre accounting for autoformalisation: design note
+:toc: preamble
+
+== The object
+
+For one translation step, let `SA` be the source atoms (hypotheses, constants,
+bounds, quantifier structure, conclusion) and `TA` the target atoms of the
+formal statement. A translation is a total map
+
+[source]
+----
+account : SA -> Verdict TA
+Verdict TA = mapped t | dropped reason
+----
+
+The fibre of a target atom `t` is the set of source atoms whose verdict is
+`mapped t`. This is the echo-type reading: `Fibre t = Σ s. account s ≡ mapped t`.
+
+== What the types buy
+
+* *No silent loss.* `account` is total, so every source atom has a verdict.
+  An atom that vanishes from the translation is a type error, not an
+  oversight.
+* *Fabrication is a fibre question.* A target atom with an empty fibre has no
+  source in this step. It may be a helpful lemma or an invented one. The
+  record makes that visible; it does not decide which.
+* *Checker blindness is explicit.* Two translations with the same target atoms
+  look identical to a checker, whatever their fibres say. The auditor needs the
+  fibre to tell them apart.
+
+== Direction, not just equality
+
+Equality of atoms is too coarse. The video's case is a numeric parameter: the
+paper needs four, the formal version needs five. Both are "a bound", but the
+formal one is a weaker claim. `EchoFidelity.agda` encodes this as a direction
+check: `cmp 4 5 ≡ weaker`.
+
+The same idea extends to hypotheses (a target with an extra hypothesis is
+weaker) and to conclusions (a target with a stronger conclusion is stronger
+and needs proof, not just a check).
+
+== What is not claimed
+
+* The fibre does not show that matched atoms have the same meaning. A `Nat`
+  standing in for `ℝ` maps cleanly and is still wrong.
+* The fibre cannot see what the source left implicit. Unstated assumptions
+  need a reader.
+* A trace produced by the translating process can be wrong in the same way as
+  the translation. Its independence is what gives it value.
+* Round-trip back-translation is a useful heuristic, not a proof of equivalence.
+
+== Layers of assurance
+
+[cols="1,2,2"]
+|===
+|Layer |What it checks |Decidable?
+
+|1. Accounting |Every source atom has a verdict; drops carry reasons |Yes
+|2. Structural diff |Hypothesis set, quantifier order, numeric parameters,
+ direction of each change |Yes, for the syntactic fragment
+|3. Back-translation |Target re-read as informal text, compared with source |No;
+ needs review
+|4. Axiom audit |No postulates or assumptions added on the target side |Yes
+|5. Human reading |Implicit assumptions and meaning |No
+|===
+
+Layers 1, 2, and 4 are cheap and should run on every step. Layers 3 and 5 are
+where judgement is needed. The design aim is that judgement is spent on the
+few atoms the structural layers flag, not on the whole statement.
+
+== Open questions
+
+* Which fragment of statements admits a complete structural diff? Derivative
+  counts and bounds are plausible; full first-order equivalence is not.
+* How should a fibre be persisted alongside a proof receipt so the link from
+  source to check is durable? Candidate: content IDs from `echidna/src/rust/ids.rs`.
+* Who writes the trace? Options: the translator (cheap, weak), a separate
+  model (medium), code that diffs both sides (strong for structure only).

docs/echos/README.adoc

@@ -0,0 +1,65 @@
+// SPDX-License-Identifier: MPL-2.0
+= Echos: fidelity exploration for autoformalisation
+:toc: preamble
+
+== Scope
+
+This directory is the exploration space for using echo types (fibres with
+witnesses) to reason about fidelity of translation steps, in particular
+autoformalisation: informal or source statement → formal statement → checked
+proof.
+
+It is exploratory. Nothing here is a claimed result. The question is:
+
+____
+If the fibre of each target atom is traceable back to its source atoms, does
+that help assure that the translation preserved what matters?
+____
+
+== Status
+
+[cols="2,1,3"]
+|===
+|Item |Status |Where
+
+|Fibre accounting model (Agda) |DRAFT, unverified |`proofs/agda/EchoFidelity.agda`
+|Design note (what fibres do and do not give) |Draft |`FIDELITY-FIBRE-DESIGN.adoc`
+|Investigation brief for a repo-tied bot |Ready to use |`BOT-PROMPT.adoc`
+|Wired into `All.agda` / `Smoke.agda` |No |Deliberately not wired until checked
+|===
+
+== Ground truth from the surrounding tools
+
+Checked on 2026-10-11 against the sibling repositories (read-only):
+
+* `echidna`: proof identity and goal identity hash the submitted goal text
+  (`src/rust/proof_encoding.rs`). Nothing in the trust path records a
+  source-to-target mapping. Axiom detection is pattern-based
+  (`src/rust/corpus/agda.rs`).
+* `echidna`: `src/rust/ids.rs` provides a stable content-ID scheme (UUIDv8 over
+  canonical JSON) that could hold atom identifiers.
+* `proof-burrower`: goal matching is Jaccard over signature tokens, described
+  in the code as crude (`crates/burrower-core/src/ranking.rs`).
+
+So the fibre trace described here does not exist in those tools yet.
+
+== Principles
+
+1. *Accounting is decidable; fidelity is not.* Every source atom must end up
+   mapped or explicitly dropped with a reason. That is a structural check. It
+   is not evidence that the meanings agree.
+2. *The checker sees only the target.* A proof checker cannot observe
+   fidelity. Fidelity needs an observer that sees both sides.
+3. *Traces need an independent author.* A trace written by the same process
+   that translated can share its errors. Prefer a structural diff run by code.
+4. *Record, don't assume.* A dropped or strengthened atom is information, not
+   an error to hide.
+
+== Files
+
+* `proofs/agda/EchoFidelity.agda`: fibre accounting, checker vs auditor
+  observation, and a direction check for a numeric parameter (the 4-vs-5 case).
+* `FIDELITY-FIBRE-DESIGN.adoc`: the design note, with what is and is not
+  claimed.
+* `BOT-PROMPT.adoc`: a prompt for a bot tied to this repository to carry out
+  the investigation.

proofs/agda/EchoFidelity.agda

@@ -0,0 +1,106 @@
+{-# OPTIONS --safe --without-K #-}
+-- SPDX-License-Identifier: MPL-2.0
+--
+-- STATUS: DRAFT, NOT YET TYPE-CHECKED. Agda was not available in the
+-- authoring environment. Before relying on this module, run
+--   agda proofs/agda/EchoFidelity.agda
+-- and fix any errors. It is deliberately NOT imported from All.agda or
+-- Smoke.agda until it has been checked.
+--
+-- Purpose: a small model of an autoformalisation step as a fibre record.
+-- Every source atom (hypothesis, constant, bound, conclusion) receives a
+-- verdict: mapped to a target atom, or dropped with a recorded reason.
+-- The types enforce that nothing is silently lost. They do NOT establish
+-- semantic fidelity; see docs/echos/FIDELITY-FIBRE-DESIGN.adoc.
+
+module EchoFidelity where
+
+open import Agda.Builtin.String using (String)
+open import Data.Empty using (⊥)
+open import Data.List.Base using (List)
+open import Data.Nat.Base using (ℕ; zero; suc)
+open import Data.Product.Base using (Σ; _,_)
+open import Relation.Binary.PropositionalEquality using (_≡_; refl)
+
+------------------------------------------------------------------------
+-- Verdicts for a single source atom.
+------------------------------------------------------------------------
+
+data Verdict (TA : Set) : Set where
+  mapped  : TA → Verdict TA
+  dropped : String → Verdict TA      -- reason must be recorded
+
+------------------------------------------------------------------------
+-- A translation step: a total accounting of source atoms.
+------------------------------------------------------------------------
+
+record Translation (SA TA : Set) : Set where
+  field
+    source-atoms : List SA
+    target-atoms : List TA
+    -- Totality: every source atom gets a verdict. This is the
+    -- "nothing silently lost" constraint, enforced by the type.
+    account      : SA → Verdict TA
+
+open Translation public
+
+------------------------------------------------------------------------
+-- Fibres: the source atoms that a given target atom traces back to.
+-- A fibre is a Σ-type of source atoms together with a proof that the
+-- source atom is mapped to that target atom.
+------------------------------------------------------------------------
+
+Fibre : {SA TA : Set} → Translation SA TA → TA → Set
+Fibre T t = Σ _ (λ s → account T s ≡ mapped t)
+
+-- A target atom with an empty fibre has no source: it is fabricated
+-- relative to this step. Stated here as the definition of "fabricated";
+-- deciding it for an arbitrary translation needs decidable equality.
+Fabricated : {SA TA : Set} → Translation SA TA → TA → Set
+Fabricated T t = Fibre T t → ⊥
+
+------------------------------------------------------------------------
+-- Checker observation vs auditor observation.
+-- The proof checker (Lean, Agda, Coq) sees only the target side. The
+-- auditor sees the whole translation, including the fibre.
+------------------------------------------------------------------------
+
+checker-obs : {SA TA : Set} → Translation SA TA → List TA
+checker-obs T = target-atoms T
+
+-- Two translations that agree on the target side are indistinguishable
+-- to the checker, whatever their fibres say.
+same-target-same-checker-obs :
+  {SA TA : Set} (T T' : Translation SA TA) →
+  target-atoms T ≡ target-atoms T' →
+  checker-obs T ≡ checker-obs T'
+same-target-same-checker-obs T T' eq = eq
+
+------------------------------------------------------------------------
+-- Direction check for a numeric parameter, using the 4-vs-5 example.
+-- Convention: the parameter k means "to control the output, you need
+-- k more derivatives on the input". A smaller k is a stronger claim.
+------------------------------------------------------------------------
+
+data Direction : Set where
+  same stronger weaker : Direction
+
+-- cmp paper target: `stronger` means the target claims more than the
+-- paper, `weaker` means it claims less.
+cmp : ℕ → ℕ → Direction
+cmp zero    zero    = same
+cmp zero    (suc _) = weaker
+cmp (suc _) zero    = stronger
+cmp (suc m) (suc n) = cmp m n
+
+-- The video's case: paper says 4, Lean needs 5. The Lean statement is
+-- weaker, so the composed result is not the paper's result.
+lemma-8-6-check : cmp 4 5 ≡ weaker
+lemma-8-6-check = refl
+
+-- Sanity cases.
+cmp-same : cmp 4 4 ≡ same
+cmp-same = refl
+
+cmp-stronger : cmp 5 4 ≡ stronger
+cmp-stronger = refl