feat(coq): prove the reversibility↔CNO bridge MAA cites (A2, zero axioms)

PROOF-STATUS.adoc

@@ -86,6 +86,37 @@ assumed. `Print Assumptions` on every headline theorem shows only Coq stdlib axi
 (`ClassicalDedekindReals.*`, `functional_extensionality*`) plus, where relevant, the
 explicitly-tagged postulate above — never a hidden project axiom.
 
+=== Reversibility <-> CNO bridge (2026-07-16, the theorem MAA cites)
+
+`proofs/coq/common/CNO.v` now carries the bridge between `reversible` and the
+"composes to a no-op" characterisation the MAA framework (aletheia) cites. All five
+new results are **`Closed under the global context` (zero axioms)**:
+
+* `reversible_iff_exists_reverses` — the repo's `reversible` is exactly "exists a
+  one-sided left inverse" (`exists p_inv, reverses p p_inv`).
+* `reverses_seq_computes_identity` — the core lemma: a left inverse sequenced after
+  `p` computes the state-identity on every composite transition (via `eval_app` +
+  `eval_deterministic`).
+* `cno_equiv_seq_empty_of_reverses` — repackaged as `cno_equiv (p ;; p_inv) []`
+  (CNO-equivalence to the canonical no-op).
+* `reversible_bridge_forward` — the faithful *forward* direction of the aletheia
+  contract: a **two-sided** inverse makes *both* composites CNO-equivalent to the
+  no-op.
+* `reversible_bridge_backward_upto` — the *backward* direction, **necessarily up to
+  `=st=`**, with an explicit `p_inv`-termination hypothesis.
+
+*Honesty note.* The literal biconditional
+`reversible p <-> exists p_inv, is_CNO (p;;p_inv) /\ is_CNO (p_inv;;p)` is **not**
+provable under these definitions, and is deliberately *not* asserted: (1) `is_CNO`
+also demands purity and totality, which a `reversible` program need not have — so
+"=== CNO" is rendered by `cno_equiv _ []` (the identity-on-state component); (2)
+`state_eq` excludes the program counter while `eval` propagates it (the
+`eval_respects_state_eq_*` axioms were removed as unsound on 2026-05-20), forcing the
+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.*
+
 == OND — VERIFIED (this environment), the disclosure pillar
 
 `proofs/coq/ond/OND.v` discharges roadmap obligations *OND-1..OND-5* with **zero

ROADMAP.adoc

@@ -131,12 +131,19 @@ No fixed dates — a solo project proceeds as time allows. Ordered by value.
 
 Absolute Zero is the CNO foundation that `hyperpolymath/maa-framework`
 coordinates as a pinned submodule. The theorem MAA actually cites is the
-*general reversibility biconditional*, which does not yet exist at the general
-level (only a filesystem-specific, axiom-backed instance).
-
-* [ ] Prove `reversible p ↔ ∃ p_inv, is_CNO (p ;; p_inv) ∧ is_CNO (p_inv ;; p)`
-  in `proofs/coq/common/CNO.v` (linking `reversible` to `cno_composition`),
-  with a Lean mirror.
+*general reversibility biconditional*.
+
+* [x] *Reversibility <-> CNO bridge — landed in Coq (2026-07-16, zero axioms).*
+  `proofs/coq/common/CNO.v` proves the forward direction of the aletheia contract
+  (`reversible_bridge_forward`: a two-sided inverse makes both composites
+  `cno_equiv _ []`) and the backward direction up to `=st=`
+  (`reversible_bridge_backward_upto`), via the core lemma
+  `reverses_seq_computes_identity`. All `Closed under the global context`.
+  *Finding:* the literal `reversible p ↔ ∃ p_inv, is_CNO (p;;p_inv) ∧ is_CNO (p_inv;;p)`
+  is **not** provable here — `is_CNO` over-demands purity/totality, `state_eq`
+  excludes the PC (forcing up-to-`=st=`), and `reversible` is one-sided; so the
+  contract should be stated two-sided and `=st=`-relative (see `PROOF-STATUS.adoc`).
+  *Remaining:* Lean mirror.
 * [ ] Discharge the filesystem existence axioms in `FilesystemCNO.v` so
   `valence_reversible_pair_is_cno` becomes axiom-free.
 * [ ] Discharge the "provable debt" axioms triaged in `proof-debt-triage.md`

proofs/coq/common/CNO.v

@@ -675,3 +675,126 @@ Proof.
     exists s1; exact Heval1.
 Qed.
 
+(** ** The Reversibility <-> CNO Bridge (task A2)
+
+    This section connects the repo's [reversible] predicate to the
+    "composes to a no-op" characterisation the MAA framework (aletheia)
+    cites:
+
+        IsReversible(op) <-> exists op_inv, (op ;; op_inv) === CNO
+                                          /\ (op_inv ;; op) === CNO
+
+    Three honest modelling facts shape what is actually provable (the
+    naive biconditional against the repo's [reversible]/[is_CNO] is NOT
+    true here, and we do not assert it):
+
+    1. [is_CNO] is strictly stronger than "computes the identity": it also
+       demands purity and termination from *every* state. A [reversible]
+       program need be neither (it may perform undone I/O, and may diverge
+       on states outside p's range). So "=== CNO" is rendered faithfully by
+       [cno_equiv _ []] — CNO-equivalence to the canonical no-op (the empty
+       program), i.e. the identity-on-state component — not full [is_CNO].
+
+    2. [state_eq] (=st=) deliberately EXCLUDES the program counter, while
+       [eval] propagates the PC deterministically. The axioms that would
+       let one replace a state by an =st=-equal one under [eval] were
+       removed as UNSOUND on 2026-05-20 (see the note above
+       [cno_eval_on_equal_states]). Hence the *backward* direction is only
+       recoverable up to =st= ([reversible_bridge_backward_upto]), never
+       syntactically.
+
+    3. The repo's [reversible] is a *one-sided* left inverse
+       ([reversible_iff_exists_reverses]); the aletheia contract is
+       *two-sided*. The forward bridge is therefore stated for the honest
+       two-sided notion [reverses p p_inv /\ reverses p_inv p].
+
+    Everything below is axiom-free (Print Assumptions: "Closed under the
+    global context"), resting only on [eval_deterministic] and [eval_app]. *)
+
+(** [reverses p p_inv]: p_inv undoes p on every reachable transition. *)
+Definition reverses (p p_inv : Program) : Prop :=
+  forall s s', eval p s s' -> eval p_inv s' s.
+
+(** The repo's one-sided [reversible] is exactly "there exists a left
+    inverse" — making explicit that the two-sided bridge below needs a
+    strictly stronger hypothesis. *)
+Lemma reversible_iff_exists_reverses :
+  forall p, reversible p <-> exists p_inv, reverses p p_inv.
+Proof.
+  intros p. split; intros [p_inv H]; exists p_inv; exact H.
+Qed.
+
+(** Core lemma: a left inverse sequenced after p computes the
+    state-identity on every transition of the composite. Uses only
+    [eval_app] and [eval_deterministic]. *)
+Lemma reverses_seq_computes_identity :
+  forall p p_inv,
+    reverses p p_inv ->
+    forall s s', eval (seq_comp p p_inv) s s' -> s =st= s'.
+Proof.
+  intros p p_inv Hrev s s' Heval.
+  unfold seq_comp in Heval.
+  apply eval_app in Heval.
+  destruct Heval as [sm [Ep Epinv]].
+  (* p_inv from sm reaches both s' (given) and s (by reversibility);
+     determinism forces s' =st= s. *)
+  pose proof (Hrev s sm Ep) as Hback.
+  pose proof (eval_deterministic _ _ _ _ Epinv Hback) as Heq.
+  apply state_eq_sym; exact Heq.
+Qed.
+
+(** Evaluating the empty program is the identity on states (syntactic). *)
+Lemma eval_nil_eq : forall s s', eval [] s s' -> s' = s.
+Proof.
+  intros s s' H. inversion H. reflexivity.
+Qed.
+
+(** Repackaged as CNO-equivalence to the empty program: p ;; p_inv is a
+    no-op (in the identity-on-state sense) whenever p_inv reverses p. *)
+Lemma cno_equiv_seq_empty_of_reverses :
+  forall p p_inv,
+    reverses p p_inv ->
+    cno_equiv (seq_comp p p_inv) [].
+Proof.
+  intros p p_inv Hrev s s1 s2 H1 H2.
+  (* eval [] s s2 forces s2 = s (without a fragile subst on s). *)
+  pose proof (eval_nil_eq _ _ H2) as Hs2.
+  rewrite Hs2.
+  apply state_eq_sym.
+  apply (reverses_seq_computes_identity p p_inv Hrev s s1 H1).
+Qed.
+
+(** Forward bridge (the faithful direction of the aletheia contract):
+    a two-sided inverse makes BOTH composites CNO-equivalent to the
+    no-op. Axiom-free. *)
+Theorem reversible_bridge_forward :
+  forall p,
+    (exists p_inv, reverses p p_inv /\ reverses p_inv p) ->
+    exists p_inv,
+      cno_equiv (seq_comp p p_inv) [] /\ cno_equiv (seq_comp p_inv p) [].
+Proof.
+  intros p [p_inv [Hpp Hpi]].
+  exists p_inv. split.
+  - apply cno_equiv_seq_empty_of_reverses; exact Hpp.
+  - apply cno_equiv_seq_empty_of_reverses; exact Hpi.
+Qed.
+
+(** Backward bridge, up to =st= (necessarily — see fact 2 above): if
+    p ;; p_inv is a no-op and p_inv terminates on p's output, then p_inv
+    recovers the input up to state-equivalence. A syntactic converse is
+    unavailable because =st= excludes the PC. *)
+Theorem reversible_bridge_backward_upto :
+  forall p p_inv,
+    cno_equiv (seq_comp p p_inv) [] ->
+    forall s s',
+      eval p s s' ->
+      (exists u, eval p_inv s' u) ->
+      exists u, eval p_inv s' u /\ u =st= s.
+Proof.
+  intros p p_inv Hce s s' Ep [u Epinv].
+  exists u. split; [ exact Epinv | ].
+  assert (Ecomp : eval (seq_comp p p_inv) s u).
+  { unfold seq_comp. apply eval_app. exists s'. split; assumption. }
+  apply (Hce s u s Ecomp). apply eval_empty.
+Qed.
+