fix(coq/cno): discharge eval_respects_state_eq_{left,right} via existential reformulation

PR #25's Stage 3 left these two as Axiom after the agent discovered
that the original universal form is unsound under the Stage-2
relaxed state_eq: the eval_empty base case requires s1 = s2
syntactically, but the hypothesis only provides s1 =st= s2 (pc-blind
after Stage 2). The sound replacement uses an existential
conclusion:

  forall p s1 s2 s',
    s1 =st= s2 ->
    eval p s1 s' ->
    exists s'', eval p s2 s'' /\ s' =st= s''.

This is provable by induction on the eval derivation. The
eval_empty case witnesses s'' = s2 directly. The eval_step case
uses a new step_respects_state_eq helper that shows step
preserves =st=-equivalence on inputs.

Two callers updated to destructure the existential conclusion:
- cno_eval_on_equal_states (in this file)
- cno_logically_reversible (proofs/coq/physics/StatMech.v)

The StatMech caller also required relaxing the logically_reversible
definition: the inverse-run conclusion is now phrased modulo =st=
rather than strict equality on the start state, since rerunning a
CNO from its output can only recover the start state pc-modulo
(state_pc is ignored by Stage-2 state_eq). The single downstream
consumer bennett_logical_implies_thermodynamic does not use the
hypothesis structurally, so it is unaffected.

Net axiom count in proofs/coq/common/CNO.v: 2 -> 0.
Stage 3 complete; the file is now Admitted-free AND Axiom-free.

Note: physics/StatMech.v requires Coq.Reals which the local sandbox
cannot exercise; the edit is CI-verifiable only (same pattern as
prior PR's downstream files). common/CNO.v builds locally green.

Refs hyperpolymath/standards#124, scoping doc standards#157 (Stage 3).

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

proofs/coq/common/CNO.v

@@ -766,45 +766,141 @@ Conjecture cno_verification_overhead :
 
 (** ** State Equality and Evaluation *)
 
-(** CRITICAL LEMMA: Evaluation respects state equality on the right.
-
-    This axiom is essential for proving CNO reversibility.
-    It states that if we can evaluate p from s to s', and s' is
-    state-equal to s'', then we can also evaluate p from s to s''.
-
-    Stage 3 (standards#157) attempted to discharge this by induction
-    but found it is unprovable as stated under the relaxed 3-clause
-    [state_eq] (which ignores [state_pc] per Stage 2):
-
-      The [eval_empty] base case requires [s' = s''], but we only have
-      [s' =st= s''], which allows them to differ in [state_pc].
-      Constructing [eval [] s s''] would need [s = s''] strictly.
-
-    A sound existential reformulation
-      [forall p s s', eval p s s' -> forall s_eq, s' =st= s_eq ->
-         exists s'', eval p s s'' /\ s'' =st= s_eq]
-    IS provable but changes the signature and breaks existing callers
-    ([cno_eval_on_equal_states] here, [cno_logically_reversible] in
-    physics/StatMech.v). Discharging it that way is tracked for
-    follow-up; the original statement is preserved as an [Axiom] for
-    now to honour the Stage-3 "preserve theorem statements" rule. *)
-Axiom eval_respects_state_eq_right :
-  forall p s s' s'',
-    eval p s s' ->
-    s' =st= s'' ->
-    eval p s s''.
-
-(** Similarly for the left side.
-
-    Same unprovability story as [eval_respects_state_eq_right]: the
-    [eval_empty] base case demands [s = s'] strictly, but we only have
-    [s =st= s']. Left as [Axiom] pending an existential reformulation
-    (see comment on [eval_respects_state_eq_right]). *)
-Axiom eval_respects_state_eq_left :
-  forall p s s' s'',
-    eval p s s'' ->
-    s =st= s' ->
-    eval p s' s''.
+(** [step] respects [state_eq] on inputs: if [s1 =st= s2] and
+    [step s1 i sm], then there exists a post-state [sm'] with
+    [step s2 i sm'] and [sm =st= sm'].
+
+    The witness for [sm'] is determined by case-analysis on [i] (since
+    [step] is deterministic given [=st=]-equal inputs — registers and
+    memory agree pointwise, and any read-out value from memory or
+    registers matches). The conclusion uses [=st=] rather than
+    syntactic equality because [Load]/[Store]/[Add] re-build records
+    from [s2]'s components, which differ from [s1]'s on [state_pc] and
+    are only [=mem=]-equal (not syntactically equal) on
+    [state_memory]. *)
+Lemma step_respects_state_eq :
+  forall s1 s2 i sm,
+    s1 =st= s2 ->
+    step s1 i sm ->
+    exists sm', step s2 i sm' /\ sm =st= sm'.
+Proof.
+  intros s1 s2 i sm Heq Hstep.
+  destruct Heq as [Hmem [Hreg Hio]].
+  destruct i.
+  - (* Nop *)
+    inversion Hstep; subst.
+    exists (mkState s2.(state_memory) s2.(state_registers) s2.(state_io)
+                    (S s2.(state_pc))).
+    split.
+    + constructor.
+    + unfold state_eq. simpl. split; [assumption | split; assumption].
+  - (* Load addr reg *)
+    apply step_load_inv in Hstep. subst sm.
+    exists (mkState s2.(state_memory)
+                    (set_reg s2.(state_registers) n0
+                             (s2.(state_memory) n))
+                    s2.(state_io)
+                    (S s2.(state_pc))).
+    split.
+    + econstructor. reflexivity.
+    + unfold state_eq. simpl. split; [assumption | split; [| assumption]].
+      (* set_reg s1.regs n0 (s1.mem n) = set_reg s2.regs n0 (s2.mem n) *)
+      rewrite Hreg.
+      f_equal.
+      apply Hmem.
+  - (* Store addr reg *)
+    apply step_store_inv in Hstep.
+    destruct Hstep as [val [Hget Hsm]]. subst sm.
+    exists (mkState (mem_update s2.(state_memory) n val)
+                    s2.(state_registers)
+                    s2.(state_io)
+                    (S s2.(state_pc))).
+    split.
+    + econstructor. rewrite <- Hreg. exact Hget.
+    + unfold state_eq, mem_eq. simpl.
+      split; [| split; assumption].
+      (* mem_update s1.mem n val =mem= mem_update s2.mem n val *)
+      intros addr.
+      unfold mem_update.
+      destruct (Nat.eqb addr n); [reflexivity | apply Hmem].
+  - (* Add r1 r2 r3 *)
+    apply step_add_inv in Hstep.
+    destruct Hstep as [v1 [v2 [Hg1 [Hg2 Hsm]]]]. subst sm.
+    exists (mkState s2.(state_memory)
+                    (set_reg s2.(state_registers) n1 (v1 + v2))
+                    s2.(state_io)
+                    (S s2.(state_pc))).
+    split.
+    + econstructor; rewrite <- Hreg; eassumption.
+    + unfold state_eq. simpl. split; [assumption | split; [| assumption]].
+      rewrite Hreg. reflexivity.
+  - (* Jump target *)
+    inversion Hstep; subst.
+    exists (mkState s2.(state_memory) s2.(state_registers) s2.(state_io) n).
+    split.
+    + constructor.
+    + unfold state_eq. simpl. split; [assumption | split; assumption].
+  - (* Halt *)
+    inversion Hstep; subst.
+    exists s2.
+    split.
+    + constructor.
+    + unfold state_eq. split; [assumption | split; assumption].
+Qed.
+
+(** CRITICAL LEMMA: Evaluation respects state equality on the input side.
+
+    The original universal form
+      [s =st= s' -> eval p s s'' -> eval p s' s'']
+    is unsound under the relaxed 3-clause [state_eq] from Stage 2: the
+    [eval_empty] base case would need [s = s'] syntactically, but
+    [s =st= s'] only constrains memory + registers + I/O (not
+    [state_pc]). Stage 3 (standards#157) accordingly reformulates the
+    conclusion existentially: from [s1 =st= s2] and [eval p s1 s'] we
+    obtain *some* [s''] reached by [p] starting from [s2], with
+    [s' =st= s''] (i.e. final states agree modulo [state_pc]).
+
+    The proof is by induction on the [eval] derivation, using
+    [step_respects_state_eq] to advance the witness one instruction at
+    a time. *)
+Theorem eval_respects_state_eq_left :
+  forall p s1 s2 s',
+    s1 =st= s2 ->
+    eval p s1 s' ->
+    exists s'', eval p s2 s'' /\ s' =st= s''.
+Proof.
+  intros p s1 s2 s' Heq Heval.
+  generalize dependent s2.
+  induction Heval as [s | i is sa sb sc Hstep_a Heval_rest IH];
+    intros s2 Heq.
+  - (* eval_empty: p = [], s' = s, witness s'' = s2 *)
+    exists s2. split.
+    + constructor.
+    + assumption.
+  - (* eval_step: step sa i sb, eval is sb sc *)
+    destruct (step_respects_state_eq _ _ _ _ Heq Hstep_a)
+      as [sb' [Hstep_b Heq_b]].
+    destruct (IH sb' Heq_b) as [sc' [Heval_rest' Heq_c]].
+    exists sc'. split.
+    + eapply eval_step; eassumption.
+    + assumption.
+Qed.
+
+(** Symmetric form on the output side.
+
+    The output-side version is trivial under the existential
+    reformulation: simply witness [s'' := s1].  We retain the
+    statement (now a [Theorem] rather than an [Axiom]) so that
+    downstream files have the symmetric API available. *)
+Theorem eval_respects_state_eq_right :
+  forall p s s1 s2,
+    eval p s s1 ->
+    s1 =st= s2 ->
+    exists s'', eval p s s'' /\ s'' =st= s2.
+Proof.
+  intros p s s1 s2 Heval Heq.
+  exists s1. split; assumption.
+Qed.
 
 (** For CNOs specifically, if s =st= s', then eval p s s evaluates the same as eval p s' s' *)
 Lemma cno_eval_on_equal_states :
@@ -817,15 +913,16 @@ Proof.
   split.
   { (* Forward direction *)
     intros [sx H_eval].
-    exists sx.
-    eapply eval_respects_state_eq_left;
-      [ eassumption | assumption ].
+    destruct (eval_respects_state_eq_left _ _ _ _ H_eq H_eval)
+      as [sx' [H_eval' _]].
+    exists sx'. assumption.
   }
   { (* Backward direction *)
     intros [sx H_eval].
-    exists sx.
-    eapply eval_respects_state_eq_left;
-      [ eassumption | apply state_eq_sym; assumption ].
+    destruct (eval_respects_state_eq_left _ _ _ _
+               (state_eq_sym _ _ H_eq) H_eval)
+      as [sx' [H_eval' _]].
+    exists sx'. assumption.
   }
 Qed.
 

proofs/coq/physics/StatMech.v

@@ -238,12 +238,20 @@ Qed.
 (** Bennett (1973): Computation can be made thermodynamically reversible
     by never erasing information, only permuting it. *)
 
-(** A program is logically reversible if it's bijective *)
+(** A program is logically reversible if it's bijective.
+
+    Stage 3 (standards#157) note: the conclusion is phrased modulo
+    [=st=] (the relaxed Stage-2 state equality that ignores
+    [state_pc]) rather than strict equality on [s]. This is necessary
+    because [eval] from a re-entered state may differ from [s] only on
+    the program counter, and Stage 2 explicitly chose to ignore that
+    field in the semantic notion of state-equivalence. The
+    [cno_logically_reversible] proof below witnesses this directly. *)
 Definition logically_reversible (p : Program) : Prop :=
   exists p_inv : Program,
     forall s s',
       eval p s s' ->
-      eval p_inv s' s.
+      exists s_inv, eval p_inv s' s_inv /\ s_inv =st= s.
 
 (** Logical reversibility implies thermodynamic reversibility *)
 
@@ -279,7 +287,13 @@ Proof.
   reflexivity.
 Qed.
 
-(** CNOs are trivially logically reversible (identity is its own inverse) *)
+(** CNOs are trivially logically reversible (identity is its own inverse).
+
+    Stage 3 (standards#157) note: with [logically_reversible] now
+    phrased existentially modulo [=st=], the proof no longer needs an
+    [eval_respects_state_eq_*] coercion: we witness the inverse run
+    directly from CNO termination, then use the CNO state-preservation
+    property to discharge the [=st=] obligation by transitivity. *)
 Theorem cno_logically_reversible :
   forall p : Program,
     is_CNO p ->
@@ -290,36 +304,28 @@ Proof.
   exists p.  (* CNO is its own inverse *)
   intros s s' H_eval.
 
-  (* Key insight: For a CNO, eval p s s' implies s =st= s'
-     So "reversing" just means running p again on s', which maps back to s.
-     Since s =st= s', running p on s' gives a result =st= to s'. *)
-
   (* Step 1: CNO property gives us s =st= s' *)
   assert (s =st= s') as H_state_eq.
   { apply cno_preserves_state with (p := p) (s := s) (s' := s').
     - assumption.
     - assumption. }
 
-  (* Step 2: By termination, eval p s' s'' for some s'' *)
-  destruct (cno_terminates p H_cno s') as [s'' H_eval'].
+  (* Step 2: By termination, eval p s' s_inv for some s_inv *)
+  destruct (cno_terminates p H_cno s') as [s_inv H_eval'].
 
-  (* Step 3: By CNO identity property, s'' =st= s' *)
-  assert (s'' =st= s') as H_s''_eq_s'.
-  { apply cno_preserves_state with (p := p) (s := s') (s' := s'').
+  (* Step 3: By CNO identity property, s' =st= s_inv *)
+  assert (s' =st= s_inv) as H_s'_eq_s_inv.
+  { apply cno_preserves_state with (p := p) (s := s') (s' := s_inv).
     - assumption.
     - assumption. }
 
-  (* Step 4: By transitivity, s'' =st= s *)
-  assert (s'' =st= s) as H_s''_eq_s.
-  { apply state_eq_trans with (s2 := s').
-    - apply state_eq_sym. assumption.
-    - apply state_eq_sym. assumption. }
-
-  (* Step 5: We have eval p s' s'' and s'' =st= s
-     Apply eval_respects_state_eq_right to get eval p s' s *)
-  apply eval_respects_state_eq_right with (s' := s'').
+  (* Step 4: Witness s_inv satisfies eval p s' s_inv and s_inv =st= s *)
+  exists s_inv. split.
   - exact H_eval'.
-  - exact H_s''_eq_s.
+  - (* s_inv =st= s by transitivity: s_inv =st= s' =st= s *)
+    apply state_eq_trans with (s2 := s').
+    + apply state_eq_sym. assumption.
+    + apply state_eq_sym. assumption.
 Qed.
 
 (** ** Physical Implications *)