feat(lean): mirror the A2 reversibility<->CNO bridge (UNVERIFIED — env-blocked)

Add proofs/lean4/CNOBridge.lean, a Lean 4 mirror of the five Coq bridge
results (reverses, reverses_seq_computes_identity,
cnoEquiv_seq_empty_of_reverses, reversible_bridge_forward,
reversible_bridge_backward + a functional-model biconditional corollary).

HONESTY: this file could NOT be machine-checked in the authoring environment
— the Lean toolchain and Mathlib cache download from GitHub release assets,
which the egress policy blocked (HTTP 403; confirmed on both the elan release
and the lean4 v4.16.0 toolchain). It is therefore:
  - registered in lakefile.lean as a NON-@[default_target] lean_lib, so the
    standard `lake build` (the repo's green proof suite) is unaffected;
  - loudly labelled UNVERIFIED in its header, with the exact verify command
    (`lake build CNOBridge` + `#print axioms`);
  - disclosed as such in PROOF-STATUS.adoc.

Modelling note: Lean's `eval` is a total function and `ProgramState.eq`
includes the PC, so the mirror states the bridge with syntactic state
equality — a stronger, cleaner form than Coq's `=st=`-relative statement
(no determinism lemma or up-to-=st= slack needed). A disclosed cross-model
difference, consistent with "each prover checks its own formalisation".

No Coq files touched; the merged A2 development is unchanged.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_015qwVESTcbfanY2iJPQNoSz

Author: claude

PROOF-STATUS.adoc

@@ -115,7 +115,19 @@ also demands purity and totality, which a `reversible` program need not have —
 backward direction to be up-to-`=st=`; (3) the repo's `reversible` is one-sided
 whereas the contract is two-sided. The in-file section header documents all three.
 This is a genuine statement-shape finding: it tells the aletheia contract to be
-stated two-sided and `=st=`-relative, not a proof dodged. *Lean mirror deferred.*
+stated two-sided and `=st=`-relative, not a proof dodged.
+
+*Lean mirror — `proofs/lean4/CNOBridge.lean` (UNVERIFIED in this environment).*
+A functional-model mirror of the five bridge results was written for Lean 4, but
+it could **not** be machine-checked here: the Lean toolchain and Mathlib cache
+download from GitHub release assets, which the egress policy blocked (HTTP 403).
+It is registered in `lakefile.lean` as a **non-`@[default_target]`** `lean_lib`,
+so it does not gate the standard `lake build`; verify with
+`lake build CNOBridge` (+ `#print axioms`) where the toolchain is available. Note
+the mirror states the bridge with *syntactic* state equality (Lean's `eval` is a
+total function and `ProgramState.eq` includes the PC), a stronger/cleaner form
+than the Coq `=st=`-relative statement — a disclosed cross-model difference, not
+a claim of literal equivalence.
 
 == OND — VERIFIED (this environment), the disclosure pillar
 

proofs/lean4/CNOBridge.lean

@@ -0,0 +1,97 @@
+/- Reversibility ↔ CNO Bridge — Lean 4 mirror of the Coq A2 development
+
+   Mirrors the theorems added to proofs/coq/common/CNO.v (the "reversibility
+   ↔ CNO bridge" the MAA framework / aletheia cites). See PROOF-STATUS.adoc.
+
+   ┌─ VERIFICATION STATUS ──────────────────────────────────────────────────┐
+   │ NOT machine-checked in the environment where this file was written:     │
+   │ the Lean toolchain and Mathlib cache download from GitHub release        │
+   │ assets, which the egress policy blocked (HTTP 403). This file is a       │
+   │ best-effort transcription against the CNO.lean API and is registered in  │
+   │ lakefile.lean as a NON-default `lean_lib`, so the standard `lake build`  │
+   │ is unaffected by it. To verify:                                          │
+   │     cd proofs/lean4 && lake exe cache get && lake build CNOBridge        │
+   │ and `#print axioms` on each theorem. Treat as unverified until then.     │
+   └─────────────────────────────────────────────────────────────────────────┘
+
+   Modelling note (honest cross-prover difference): Lean's `eval` is a TOTAL
+   FUNCTION and `ProgramState.eq` INCLUDES the program counter, whereas Coq's
+   `eval` is a relation and `=st=` EXCLUDES the PC. So this Lean mirror states
+   the bridge with SYNTACTIC equality of evaluated states — a stronger, cleaner
+   form that needs no determinism lemma (free for a function) and no
+   "up-to-=st=" slack on the backward direction. It is therefore not a literal
+   transcription of the Coq statement but its functional-model analogue,
+   consistent with the repo's "each prover checks its own formalisation" stance.
+
+   Author: Jonathan D. A. Jewell
+   Project: Absolute Zero
+   License: MPL-2.0
+-/
+
+import CNO
+
+namespace CNOBridge
+
+open CNO
+
+/-- `reverses p p_inv`: `p_inv` undoes `p` on every state. In Lean's functional
+    model this is `∀ s, eval p_inv (eval p s) = s` — the body of `CNO.reversible`. -/
+def reverses (p p_inv : Program) : Prop :=
+  ∀ s, eval p_inv (eval p s) = s
+
+/-- The repo's `reversible` is exactly "there exists a (one-sided) left inverse". -/
+theorem reversible_iff_exists_reverses (p : Program) :
+    reversible p ↔ ∃ p_inv, reverses p p_inv := Iff.rfl
+
+/-- CNO-equivalence to the no-op, functional form: the two programs evaluate to
+    the same state from every start state. -/
+def cnoEquiv (p1 p2 : Program) : Prop :=
+  ∀ s, eval p1 s = eval p2 s
+
+/-- Core lemma: a left inverse sequenced after `p` computes the identity on
+    every state. Uses only `eval_seqComp` (Coq needed `eval_app` +
+    `eval_deterministic`; determinism is free here because `eval` is a function). -/
+theorem reverses_seq_computes_identity {p p_inv : Program}
+    (h : reverses p p_inv) : ∀ s, eval (seqComp p p_inv) s = s := by
+  intro s
+  rw [eval_seqComp]
+  exact h s
+
+/-- Repackaged as CNO-equivalence to the empty program (the canonical no-op). -/
+theorem cnoEquiv_seq_empty_of_reverses {p p_inv : Program}
+    (h : reverses p p_inv) : cnoEquiv (seqComp p p_inv) [] := by
+  intro s
+  show eval (seqComp p p_inv) s = eval [] s
+  have hnil : eval [] s = s := rfl
+  rw [hnil]
+  exact reverses_seq_computes_identity h s
+
+/-- Forward bridge (the faithful direction of the aletheia contract): a
+    two-sided inverse makes BOTH composites CNO-equivalent to the no-op. -/
+theorem reversible_bridge_forward {p : Program}
+    (h : ∃ p_inv, reverses p p_inv ∧ reverses p_inv p) :
+    ∃ p_inv, cnoEquiv (seqComp p p_inv) [] ∧ cnoEquiv (seqComp p_inv p) [] := by
+  obtain ⟨p_inv, hpp, hpi⟩ := h
+  exact ⟨p_inv, cnoEquiv_seq_empty_of_reverses hpp,
+               cnoEquiv_seq_empty_of_reverses hpi⟩
+
+/-- Backward bridge: from "the composite is a no-op" recover the inverse. In
+    Lean's functional/PC-inclusive model this is exact (SYNTACTIC), with no
+    up-to-`=st=` slack and no termination hypothesis — the two facts Coq needed
+    (its `reversible_bridge_backward_upto`) because its `eval` is relational and
+    `=st=` drops the PC. -/
+theorem reversible_bridge_backward {p p_inv : Program}
+    (h : cnoEquiv (seqComp p p_inv) []) : reverses p p_inv := by
+  intro s
+  have hs := h s
+  rw [eval_seqComp] at hs
+  -- hs : eval p_inv (eval p s) = eval [] s, and eval [] s = s definitionally
+  exact hs
+
+/-- Corollary: in the functional model the forward and backward directions
+    combine into a genuine biconditional for a single inverse `p_inv`. -/
+theorem reverses_iff_cnoEquiv_seq_empty (p p_inv : Program) :
+    reverses p p_inv ↔ cnoEquiv (seqComp p p_inv) [] :=
+  ⟨cnoEquiv_seq_empty_of_reverses, reversible_bridge_backward⟩
+
+end CNOBridge

proofs/lean4/lakefile.lean

@@ -31,3 +31,10 @@ lean_lib StatMech
 
 @[default_target]
 lean_lib OND
+
+-- Reversibility ↔ CNO bridge (mirror of the Coq A2 development). Deliberately
+-- NOT a @[default_target]: it was authored where the Lean toolchain could not be
+-- fetched (egress policy blocked the GitHub release, HTTP 403), so it is
+-- unverified in that environment and must not gate the standard `lake build`.
+-- Build/verify explicitly with `lake build CNOBridge`.
+lean_lib CNOBridge