fix(coq/cno): Stage 2 - relax state_eq, discharge nop_is_cno Admitted

Per owner ruling on hyperpolymath/standards#157 Stage 2, [state_eq] is
relaxed from four clauses to three:

  state_eq s1 s2 := mem_eq s1.mem s2.mem
                 /\ s1.regs = s2.regs
                 /\ s1.io = s2.io

Dropping the pc-equality clause matches the intuition that "Nop does
nothing": Nop only differs from the input state on the pc field, which
state_eq now ignores. This is the canonical relaxation needed to make
nop_is_cno provable.

Changes to common/CNO.v:

- state_eq definition: dropped 4th conjunct, added comment citing
  standards#157 Stage 2.
- state_eq_refl, state_eq_trans, state_eq_sym: destructure pattern
  reduced from [Hm [Hr [Hi Hp]]] to [Hm [Hr Hi]], proof bodies trimmed
  by one [split] / one bullet each.
- nop_is_cno: proof body replaced. Now uses eval_cons_inv +
  eval_nil_inv (from Stage 1) to invert evaluation, then
  inversion-on-step_nop, then discharges the 3-clause state_eq goal
  by reflexivity on each field.

Downstream files updated to match the new 3-clause shape:

- physics/StatMech_helpers.v: its local state_eq_sym / state_eq_trans
  copy the 4-clause destructure pattern from CNO.v. Updated to drop
  the pc clause + restructure with { } blocks for 8.18 hygiene.
- malbolge/MalbolgeCore.v: malbolge_cno_implies_cno's [repeat split.]
  produced 4 bullets (incl. "PC"). Updated to 3 fields with { } blocks;
  the PC bullet is removed entirely.
- category/CNOCategory.v: one destructure of state_eq's conjuncts
  updated from [H_mem [H_reg [H_io H_pc]]] to [H_mem [H_reg H_io]].

Note: the downstream files (StatMech_helpers, MalbolgeCore,
CNOCategory) could not be verified locally from this worktree due to
sandbox restrictions on the physics/, malbolge/, category/
subdirectories. CI must verify them. The CNO.v changes are verified:
coqc -R common CNO common/CNO.v exits 0, 0 Admitted, 4 Axioms.

Refs hyperpolymath/standards#124
Refs hyperpolymath/standards#157

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

Author: hyperpolymath

proofs/coq/category/CNOCategory.v

@@ -165,7 +165,7 @@ Proof.
     + (* Purity: follows from state equality *)
       intros s s' H_eval.
       assert (H_eq : s =st= s') by (apply H_id; assumption).
-      destruct H_eq as [H_mem [H_reg [H_io H_pc]]].
+      destruct H_eq as [H_mem [H_reg H_io]].
       unfold pure, no_io, no_memory_alloc.
       split; assumption.
     + (* Thermodynamic reversibility: trivially true *)

proofs/coq/common/CNO.v

@@ -59,12 +59,17 @@ Record ProgramState : Type := mkState {
   state_pc : nat  (* Program counter *)
 }.
 
-(** State equality *)
+(** State equality.
+
+    [state_eq] ignores [state_pc] by design - programs are equivalent
+    if they leave memory/registers/IO unchanged, even if they advance
+    the program counter. This matches the intuition that "Nop does
+    nothing" which is otherwise unprovable under strict pc-equality.
+    Owner decision: see hyperpolymath/standards#157 Stage 2. *)
 Definition state_eq (s1 s2 : ProgramState) : Prop :=
   s1.(state_memory) =mem= s2.(state_memory) /\
   s1.(state_registers) = s2.(state_registers) /\
-  s1.(state_io) = s2.(state_io) /\
-  s1.(state_pc) = s2.(state_pc).
+  s1.(state_io) = s2.(state_io).
 
 Notation "s1 '=st=' s2" := (state_eq s1 s2) (at level 70).
 
@@ -327,16 +332,14 @@ Proof.
   { intros addr. reflexivity. }
   split.
   { reflexivity. }
-  split.
-  { reflexivity. }
   reflexivity.
 Qed.
 
 (** State equality is transitive *)
 Lemma state_eq_trans :
   forall s1 s2 s3, s1 =st= s2 -> s2 =st= s3 -> s1 =st= s3.
 Proof.
-  intros s1 s2 s3 [Hm1 [Hr1 [Hi1 Hp1]]] [Hm2 [Hr2 [Hi2 Hp2]]].
+  intros s1 s2 s3 [Hm1 [Hr1 Hi1]] [Hm2 [Hr2 Hi2]].
   unfold state_eq.
   split.
   { (* Memory *)
@@ -348,12 +351,8 @@ Proof.
   { (* Registers *)
     transitivity (s2.(state_registers)); auto.
   }
-  split.
-  { (* I/O *)
-    transitivity (s2.(state_io)); auto.
-  }
-  (* PC *)
-  transitivity (s2.(state_pc)); auto.
+  (* I/O *)
+  transitivity (s2.(state_io)); auto.
 Qed.
 
 (** Purity is transitive *)
@@ -456,14 +455,56 @@ Qed.
 
 (** A single Nop instruction is a CNO.
 
-    Under the strict 4-clause [state_eq] (with pc-equality) this theorem
-    is FALSE: Nop increments the program counter, so the post-state
-    differs from the pre-state on the [state_pc] field. The proof is
-    discharged in Stage 2 once [state_eq] is relaxed to ignore [state_pc].
-    See [hyperpolymath/standards#157] Stage 2. *)
+    Under the strict 4-clause [state_eq] this theorem was FALSE because
+    Nop increments [state_pc]. With the relaxed 3-clause [state_eq]
+    (memory + registers + IO, ignoring [state_pc]) Nop genuinely is a
+    CNO: it only differs from the pre-state on the pc field, which
+    [state_eq] now ignores. See hyperpolymath/standards#157 Stage 2. *)
 Theorem nop_is_cno : is_CNO [Nop].
 Proof.
-Admitted.
+  unfold is_CNO.
+  split.
+  { (* Termination *)
+    intros s.
+    exists (mkState s.(state_memory) s.(state_registers) s.(state_io) (S s.(state_pc))).
+    apply eval_step with
+      (s2 := mkState s.(state_memory) s.(state_registers) s.(state_io) (S s.(state_pc))).
+    { constructor. }
+    constructor.
+  }
+  split.
+  { (* Identity *)
+    intros s s' Heval.
+    apply eval_cons_inv in Heval.
+    destruct Heval as [s2 [Hstep Hrest]].
+    apply eval_nil_inv in Hrest.
+    subst.
+    inversion Hstep; subst.
+    unfold state_eq, mem_eq.
+    split.
+    { intros addr. reflexivity. }
+    split.
+    { reflexivity. }
+    reflexivity.
+  }
+  split.
+  { (* Purity *)
+    intros s s' Heval.
+    apply eval_cons_inv in Heval.
+    destruct Heval as [s2 [Hstep Hrest]].
+    apply eval_nil_inv in Hrest.
+    subst.
+    inversion Hstep; subst.
+    unfold pure, no_io, no_memory_alloc, mem_eq.
+    split.
+    { reflexivity. }
+    intros addr. reflexivity.
+  }
+  (* Thermodynamic reversibility *)
+  unfold thermodynamically_reversible.
+  intros s1 s2 Heval.
+  reflexivity.
+Qed.
 
 (** ** CNO Equivalence *)
 
@@ -494,14 +535,12 @@ Qed.
 (** State equality is symmetric *)
 Lemma state_eq_sym : forall s1 s2, s1 =st= s2 -> s2 =st= s1.
 Proof.
-  intros s1 s2 [Hm [Hr [Hi Hp]]].
+  intros s1 s2 [Hm [Hr Hi]].
   unfold state_eq, mem_eq in *.
   split.
   { intros addr. symmetry. apply Hm. }
   split.
   { symmetry. assumption. }
-  split.
-  { symmetry. assumption. }
   symmetry. assumption.
 Qed.
 

proofs/coq/malbolge/MalbolgeCore.v

@@ -286,23 +286,21 @@ Proof.
   destruct HCNO as [HM [HA [HC [HD HIO]]]].
   unfold malbolge_to_state, state_eq.
   simpl.
-  repeat split.
-  - (* Memory *)
+  split.
+  { (* Memory *)
     unfold mem_eq.
     intros addr.
     rewrite HM.
     reflexivity.
-  - (* Registers *)
+  }
+  split.
+  { (* Registers *)
     simpl.
     rewrite HA, HC, HD.
     reflexivity.
-  - (* I/O *)
-    apply HIO.
-  - (* PC *)
-    simpl.
-    (* C register is PC and is now preserved by strengthened CNO definition *)
-    rewrite HC.
-    reflexivity.
+  }
+  (* I/O - state_eq no longer has a PC clause per standards#157 Stage 2 *)
+  apply HIO.
 Qed.
 
 (** ** The "Absolute Zero" Program *)

proofs/coq/physics/StatMech_helpers.v

@@ -10,33 +10,36 @@
 
 Require Import CNO.
 
-(** State equality is symmetric *)
+(** State equality is symmetric.
+
+    Note: [state_eq] is 3-clause (memory + registers + IO) since
+    standards#157 Stage 2 dropped the pc-equality clause. *)
 Lemma state_eq_sym :
   forall s1 s2 : ProgramState,
     s1 =st= s2 -> s2 =st= s1.
 Proof.
-  intros s1 s2 [H_mem [H_reg [H_io H_pc]]].
+  intros s1 s2 [H_mem [H_reg H_io]].
   unfold state_eq.
-  repeat split.
-  - unfold mem_eq in *. intro addr. symmetry. apply H_mem.
-  - symmetry. assumption.
-  - symmetry. assumption.
-  - symmetry. assumption.
+  split.
+  { unfold mem_eq in *. intro addr. symmetry. apply H_mem. }
+  split.
+  { symmetry. assumption. }
+  symmetry. assumption.
 Qed.
 
 (** State equality is transitive *)
 Lemma state_eq_trans :
   forall s1 s2 s3 : ProgramState,
     s1 =st= s2 -> s2 =st= s3 -> s1 =st= s3.
 Proof.
-  intros s1 s2 s3 [H_mem12 [H_reg12 [H_io12 H_pc12]]] [H_mem23 [H_reg23 [H_io23 H_pc23]]].
+  intros s1 s2 s3 [H_mem12 [H_reg12 H_io12]] [H_mem23 [H_reg23 H_io23]].
   unfold state_eq.
-  repeat split.
-  - unfold mem_eq in *. intro addr.
-    transitivity (state_memory s2 addr); [apply H_mem12 | apply H_mem23].
-  - transitivity (state_registers s2); assumption.
-  - transitivity (state_io s2); assumption.
-  - transitivity (state_pc s2); assumption.
+  split.
+  { unfold mem_eq in *. intro addr.
+    transitivity (state_memory s2 addr); [apply H_mem12 | apply H_mem23]. }
+  split.
+  { transitivity (state_registers s2); assumption. }
+  transitivity (state_io s2); assumption.
 Qed.
 
 (** For CNOs, evaluation from any state leads back to that state *)