proof(coq): discharge eval_respects_state_eq_{left,right} via deletio…

.machine_readable/6a2/META.a2ml

@@ -21,6 +21,7 @@ decisions = [
   { id = "ADR-005", status = "proposed", title = "Fix QuantumCNO.v Cexp: real exp -> complex phase factor" },
   { id = "ADR-006", status = "accepted", title = "state_eq excludes state_pc — PC is control-flow bookkeeping, not observable side effect (2026-05-18 rescue)" },
   { id = "ADR-007", status = "accepted", title = "Discharge eval_deterministic Axiom → Theorem via step_deterministic_strong helper (2026-05-20, PR #24); first post-T0 axiom audit win" },
+  { id = "ADR-008", status = "accepted", title = "Delete unsound eval_respects_state_eq_{left,right} axioms; weaken logically_reversible definition to use =st= (observational reversibility); re-prove cno_eval_on_equal_states + cno_logically_reversible via cno_terminates + cno_preserves_state (2026-05-20); rationale: under PC-excluding state_eq the strong axioms force a syntactically-identical eval result, which is unsound because eval propagates PC deterministically while =st= ignores it" },
 ]
 
 [development-practices]

.machine_readable/6a2/STATE.a2ml

@@ -26,7 +26,7 @@ maturity = "experimental"
 
 [components]
 # Format: name = [percentage, "notes"]
-coq-proofs = [88, "11/11 files compile (Coq 8.18.0+8.20.1); 0 Admitted (rescue 2026-05-18); ~120 Axiom/Parameter as post-T0 audit, 1 discharged (eval_deterministic, PR #24, 2026-05-20)"]
+coq-proofs = [90, "11/11 files compile (Coq 8.18.0+8.20.1); 0 Admitted (rescue 2026-05-18); 75→73 Axioms + 42 Parameters; 3 discharges 2026-05-20 — eval_deterministic (PR #24) + eval_respects_state_eq_{left,right} (deleted as unsound, downstream refactored to use cno_terminates + weakened logically_reversible); remainder are legitimate model-layer assumptions about abstract Parameters"]
 lean4-proofs = [95, "lake build 1631/1632 green (mathlib + 6 lean_lib targets); verified 2026-05-20"]
 z3-proofs = [90, "10 theorems encoded, needs z3 runtime"]
 agda-proofs = [60, "CNO.agda type-checks clean — 0 postulates/holes/unsolved metas (verified 2026-05-18)"]
@@ -78,7 +78,8 @@ this-month = [
 
 [session-history]
 sessions = [
-  { date = "2026-05-20", agent = "opus", summary = "Rescue branch rebased onto current main (clean); eval_deterministic Axiom discharged → Theorem (via step_deterministic_strong helper); Print Assumptions Closed under global context; 11/11 Coq + 1631/1632 Lean targets green; PR #24 filed (draft, Refs standards#124+#133)" },
+  { date = "2026-05-20", agent = "opus", summary = "Post-T0 axiom audit: 117 declarations triaged into Tier A/B/C; 2 unsound axioms (eval_respects_state_eq_left/right) deleted with downstream refactor; logically_reversible weakened to =st=; cno_eval_on_equal_states + cno_logically_reversible re-proved without axioms; 75→73 Axioms total" },
+  { date = "2026-05-20", agent = "opus", summary = "Rescue branch rebased onto current main (clean); eval_deterministic Axiom discharged → Theorem (via step_deterministic_strong helper); Print Assumptions Closed under global context; 11/11 Coq + 1631/1632 Lean targets green; PR #24 MERGED (admin-squash 69e7a22)" },
   { date = "2026-05-18", agent = "opus", summary = "Tier-0 rescue: CNO.v keystone re-proved (state_eq PC-exclusion fix, 9 named repairs); Complex.v self-contained complex numbers added; 11 Coq files compile under Coq 8.20.1; full Lean lake build succeeds; PROOF-STATUS-2026-05-18.md ledger added" },
   { date = "2026-02-05", agent = "opus", summary = "Completed 8 proofs, created PROOF-INSIGHTS.md" },
   { date = "2026-02-04", agent = "opus", summary = "Completed cno_logically_reversible, added axioms" },

.machine_readable/META.scm

@@ -10,7 +10,8 @@
      ("ADR-004" "accepted" "post_execution_dist specialized for CNOs (identity on distributions)")
      ("ADR-005" "proposed" "Fix QuantumCNO.v Cexp: real exp -> complex phase factor")
      ("ADR-006" "accepted" "state_eq excludes state_pc — PC is control-flow bookkeeping, not observable side effect (2026-05-18 rescue)")
-     ("ADR-007" "accepted" "Discharge eval_deterministic Axiom → Theorem via step_deterministic_strong helper (2026-05-20, PR #24); first post-T0 axiom audit win")))
+     ("ADR-007" "accepted" "Discharge eval_deterministic Axiom → Theorem via step_deterministic_strong helper (2026-05-20, PR #24); first post-T0 axiom audit win")
+     ("ADR-008" "accepted" "Delete unsound eval_respects_state_eq_{left,right} axioms; weaken logically_reversible to =st= (observational reversibility); re-prove cno_eval_on_equal_states + cno_logically_reversible via cno_terminates + cno_preserves_state (2026-05-20)")))
 
   (development-practices
     (code-style "Coq proof engineering")

PROOF-STATUS-2026-05-18.md

@@ -78,14 +78,15 @@ quantum) `Require Import CNO.Complex.` — fixes the inconsistent
 | `proofs/coq/filesystem/FilesystemCNO.v` | ✅ compiles | fixed `CNO.CNO` import and `fold_left` argument order. |
 | `proofs/lean4/CNO.lean` | ✅ builds | completed `loadStore_preserves_memory` cons case with rewrite helper lemmas; no proof holes. |
 | `proofs/lean4/{FilesystemCNO,LambdaCNO,QuantumCNO,StatMech,CNOCategory}.lean` | ✅ build | full `lake build` succeeds. |
-| ~120 Coq `Axiom`/`Parameter` | ⚠️ assumptions | **NOT holes.** Separate post-T0 audit (e.g. `cno_decidable`, `eval_respects_state_eq_left/right`). `eval_deterministic` was on this list — **discharged 2026-05-20** (PR `#24`, `Print Assumptions` "Closed under the global context"). |
+| 73 Coq `Axiom` + 42 `Parameter` | ⚠️ model-layer assumptions | **NOT holes.** Triage 2026-05-20: ~73 Axioms are properties of abstract `Parameter`s (physics constants/laws, quantum gate unitarity, Cexp properties, POSIX semantics, Y-combinator non-termination, intentionally-typed `hom_functor` per inline comment) — **legitimate model layer; do not discharge without first defining the underlying Parameter**. **3 discharges shipped: `eval_deterministic` (PR #24, 2026-05-20), `eval_respects_state_eq_left` + `_right` (this PR, 2026-05-20)** — the last two were unsound under the rescue branch's PC-excluding `state_eq` and have been **deleted outright**; their downstream consumers (`cno_eval_on_equal_states`, `cno_logically_reversible`) re-proved via `cno_terminates` + `cno_preserves_state` with a correspondingly-weakened `logically_reversible` definition. `cno_decidable` (depends on undecidable Memory function equality) deferred. |
 
 ## Tier-0 status
 
 - **Keystone complete:** `CNO.v` (Coq) + `CNO.agda` (Agda) verified.
 - **T0 complete:** dependent Coq files, `StatMech_helpers.v`, and full Lean package build.
-- **Post-T0 (in progress):** the ~120-axiom audit (classify *legitimate model assumption*
-  vs *hard proof papered over*). 1 axiom discharged so far (`eval_deterministic`).
+- **Post-T0 (in progress):** 75 → 73 Axioms; the remainder are model-layer assumptions
+  (legitimate model assumptions about abstract Parameters or external physical laws).
+  See ADR-008 (`logically_reversible` weakening / removal of unsound state_eq axioms).
 
 ## Position vs. before the review
 
@@ -107,7 +108,24 @@ by `Theorem eval_deterministic` proved from a new helper `Lemma
 step_deterministic_strong`. `Print Assumptions` on both reports "Closed
 under the global context". Re-verified on Coq 8.18.0 + 8.20.1 (proof is
 portable). Full `lake build` 1631/1632 green; all 11 Coq files
-recompile clean. ~120 other `Axiom`/`Parameter` declarations remain.
+recompile clean.
+
+**Status update 2026-05-20 (later).** Full triage of the remaining axioms:
+75 Axioms total; ~73 are legitimate model-layer assumptions (properties
+of abstract `Parameter`s — physics constants/laws, quantum gate unitarity,
+Cexp properties, POSIX semantics, Y combinator non-termination,
+intentionally-typed `hom_functor`); 2 (`eval_respects_state_eq_left/right`)
+were **unsound** under the rescue branch's PC-excluding [state_eq]
+(s and s'' can be `=st=` with different PC, while eval deterministically
+propagates PC). Discharged 2026-05-20 by **deletion + downstream
+refactor**: `logically_reversible` definition weakened to use `=st=`
+(observational reversibility — the strict form was unproveable, and
+`bennett_logical_implies_thermodynamic`'s body never used the hypothesis,
+so no theory is lost); `cno_eval_on_equal_states` re-proved via
+`cno_terminates` (different witnesses, sound); `cno_logically_reversible`
+re-proved via `cno_terminates` + `cno_preserves_state`. `Print Assumptions`
+on both lemmas: "Closed under the global context". 75 → 73 axioms.
+See ADR-008.
 
 **Branch:** `repair/proofs-tier0-2026-05-18` (not pushed). Repo:
 `~/dev/repos/absolute-zero`.

proofs/coq/common/CNO.v

@@ -631,51 +631,35 @@ Conjecture cno_verification_overhead :
 
 (** ** State Equality and Evaluation *)
 
-(** CRITICAL LEMMA: Evaluation respects state equality on the right
-
-    This lemma 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''.
-
-    This is needed because the eval relation is defined inductively
-    on specific states, but CNO theory works with state equality (=st=).
-*)
-Axiom eval_respects_state_eq_right :
-  forall p s s' s'',
-    eval p s s' ->
-    s' =st= s'' ->
-    eval p s s''.
-
-(** TODO: Prove this axiom by induction on eval structure.
-    This requires showing that each step constructor respects state equality.
-    For now, we axiomatize it to unblock cno_logically_reversible proof.
-*)
-
-(** Similarly for the left side *)
-Axiom eval_respects_state_eq_left :
-  forall p s s' s'',
-    eval p s s'' ->
-    s =st= s' ->
-    eval p s' s''.
-
-(** For CNOs specifically, if s =st= s', then eval p s s evaluates the same as eval p s' s' *)
+(** UNSOUND-AS-STATED axioms previously declared here
+    (`eval_respects_state_eq_right` and `_left`) have been REMOVED
+    (2026-05-20). The rescue branch's PC-excluding [state_eq] (memory +
+    registers + I/O, not [state_pc]) means two `=st=` states can carry
+    different PCs, while the eval relation deterministically propagates
+    PC through every step constructor. So [eval p s s'] forces a unique
+    [s'] (cf. [eval_deterministic]) — replacing [s'] by an [=st=]-equal
+    [s''] is generally unsound (different PC).
+
+    The only consumer that needed the strong form ([cno_logically_reversible]
+    in StatMech.v) has been refactored to use [cno_terminates] +
+    [cno_preserves_state] directly, with a correspondingly-weakened
+    [logically_reversible] definition. See ADR-008. *)
+
+(** For CNOs specifically, termination from one state is equivalent to
+    termination from any state-equal state — both can be witnessed by
+    [cno_terminates] (the witnesses need not coincide). *)
 Lemma cno_eval_on_equal_states :
   forall p s s',
     is_CNO p ->
     s =st= s' ->
     (exists s1, eval p s s1) <-> (exists s2, eval p s' s2).
 Proof.
-  intros p s s' H_cno H_eq.
-  split; intros [sx H_eval].
-  - (* Forward: eval p s sx  and  s =st= s'  ==>  eval p s' sx *)
-    exists sx.
-    eapply eval_respects_state_eq_left.
-    + eassumption.
-    + assumption.
-  - (* Backward: eval p s' sx  and  s =st= s'  ==>  eval p s sx *)
-    exists sx.
-    eapply eval_respects_state_eq_left.
-    + eassumption.
-    + apply state_eq_sym. assumption.
+  intros p s s' H_cno _.
+  split; intros _.
+  - (* termination from s' is direct from is_CNO p *)
+    destruct (cno_terminates p H_cno s') as [s2 Heval2].
+    exists s2; exact Heval2.
+  - destruct (cno_terminates p H_cno s) as [s1 Heval1].
+    exists s1; exact Heval1.
 Qed.
 

proofs/coq/physics/StatMech.v

@@ -251,12 +251,23 @@ 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 up to observational equivalence:
+    there exists an inverse program that, run on the post-execution state,
+    recovers a state observationally equal ([=st=]) to the input.
+
+    Stating reversibility up to [=st=] (rather than strict [=]) is forced
+    by the rescue branch's PC-excluding [state_eq]: [eval p s s'] uniquely
+    determines [s'] (cf. [eval_deterministic_strong]) including its PC,
+    so re-running [p] on a different start state cannot in general produce
+    a PC-identical result. Observational reversibility is what the
+    thermodynamic argument actually needs (memory + registers + I/O are
+    the bits of physical record; the PC is bookkeeping). See ADR-008
+    (2026-05-20). *)
 Definition logically_reversible (p : Program) : Prop :=
   exists p_inv : Program,
     forall s s',
       eval p s s' ->
-      eval p_inv s' s.
+      exists s'', eval p_inv s' s'' /\ s'' =st= s.
 
 (** Logical reversibility implies thermodynamic reversibility *)
 
@@ -328,11 +339,13 @@ Proof.
     - apply state_eq_sym. exact H_s'_eq_s''.
     - apply state_eq_sym. exact H_state_eq. }
 
-  (* 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'').
-  - exact H_eval'.
-  - exact H_s''_eq_s.
+  (* Step 5: We have eval p s' s'' and s'' =st= s.
+     The (now weakened) definition of [logically_reversible] only requires
+     a witness end-state observationally equal to s — H_eval' + H_s''_eq_s
+     supply it directly. The previous proof used the unsound
+     [eval_respects_state_eq_right] axiom; that axiom has been removed
+     (see CNO.v / ADR-008). *)
+  exists s''. split; [ exact H_eval' | exact H_s''_eq_s ].
 Qed.
 
 (** ** Physical Implications *)