[Integration] Ground L3 (reversibility + equivalence + loss) theorems in echo-types LAYER3 module

[hyperpolymath]

Background

Audit 2026-06-01 (companion to deep audit #41-#46) found that valence-shell's three core L3 theorems are formalised independently across 6 proof systems, yet are exact L3 (echo-layer) shapes as defined in hyperpolymath/echo-types.

Current state

Aspect	Finding
Active imports of echo-types	0 (zero Coq Require Import EchoTypes.*, zero Lean import EchoTypes, zero Agda open import EchoTypes)
Referenced-only mentions	1 (in proofs/agda/README.adoc — notes shared --safe --without-K discipline)
Cargo.toml / flake.nix echo-types entries	none

L3-shape theorems already in valence-shell

#	Theorem	File	Echo-types cousin
1	fsEquiv + fsEquivIsEquivalence	FilesystemEquivalence.lean / filesystem_equivalence.v	EchoObservationalEquivalence._≡m_ + ≡m-refl/sym/trans
2	reversibleCreatesEquiv	FilesystemEquivalence.lean	EchoObservationalEquivalence.mode-equality-strictly-finer-at-linear
3	obliterate_not_injective	RMOOperations.lean	EchoLossTaxonomy.const-fibre-↔-domain (CONST case)
4	operationSequenceReversible + isCNOSequence	FilesystemComposition.lean	EchoNoSectionGeneric.no-section-of-collapsing-map + EchoOFSUnivF5
5	copyFile_reversible	CopyMoveOperations.lean	EchoTotalCompletion / EchoNoSectionGeneric.no-section-when-non-injective-at-y

Per estate-memory directive [Proofs MUST check + cross-doc echo-types] (owner 2026-06-01), every proof in any repo with an echo-types link must first audit hyperpolymath/echo-types, reuse if applicable, extend upstream WITH proofs if not, then cross-document.

Why this matters

1. Proof-debt reduction. The remaining obliterate_overwrites_all_blocks hole (per docs/PROOF_HOLES_AUDIT.md) drops out as a downstream consequence of EchoLossTaxonomy.const-fibre-↔-domain rather than needing a standalone axiom.
2. Cross-language validation. echo-types' F5 (orthogonal factorisation) proofs would ground FilesystemComposition.cnO in EchoOFSUnivF5.echo-factorisation-strict — upgrading composition theory from "compositional-by-definition" to "compositionally-universal".
3. L3 obligations are load-bearing per estate policy. The MAA framework IS L3: reversible operations + observational equivalence + loss taxonomy = the three-pillar L3 structure. Integrating echo-types makes this explicit and audit-trail-ready.

Smallest first step

Import EchoObservationalEquivalence in proofs/agda/FilesystemEquivalence.agda and re-state fsEquiv + fsEquivIsEquivalence as instances of _≡m_ at mode linear:

open import EchoObservationalEquivalence using (_≡m_; ≡m-refl; ≡m-sym; ≡m-trans)

fsEquiv : (fs1 fs2 : Filesystem) → Prop
fsEquiv fs1 fs2 = fs1 ≡m fs2   -- at mode linear

fsEquivTrans : ∀ fs1 fs2 fs3 → fs1 ≈ fs2 → fs2 ≈ fs3 → fs1 ≈ fs3
fsEquivTrans = ≡m-trans

Once Agda validates, extract bindings via the project's existing proofs/agda → proofs/lean4 → proofs/coq pipeline. The Rust CLI layer is unaffected.

Layer scope

• L3 (echo): IN SCOPE — observational equivalence + reversibility + loss
• L1 (regions/linear): not applicable to filesystem reversibility
• L2 (modality): possibly relevant for read/write permissions but a stretch (out of scope for this issue)
• L4 (dyadic): possibly relevant for transaction grouping (begin/commit/rollback) but out of scope

Refs

• Audit conducted 2026-06-01 by echo-types integration audit subagent
• Companion: Seam walk: 3 prod panics + 10 unreachables + 28 TODOs + 6 proof holes (audit 2026-06-01) #41 (seam walk), Proof inventory — 478 candidate theorems + 8-theorem foundation pack #42 (proof inventory), PR docs(proof): proof narrative + open frontier + reconciled PROOF-NEEDS #47 (proof narrative)
• Cross-repo: hyperpolymath/echo-types — slices F1-F5, Route A 6-PR arc closed 2026-05-30
• Estate-memory: [Proofs MUST check + cross-doc echo-types], [Echo-types Slice 3+4 — Route A 6-PR arc CLOSED 2026-05-30]

🤖 Filed by echo-types integration audit 2026-06-01