From a7de17d3a9f4aaaaa8cc6f7fc4726fb095624d90 Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Wed, 20 May 2026 17:15:14 +0100 Subject: [PATCH] proof(coq): discharge eval_respects_state_eq_{left,right} via deletion + downstream refactor MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Audit of the remaining ~120 Axiom/Parameter declarations after PR #24 identified TWO genuinely unsound axioms (the rest are legitimate model-layer assumptions about abstract Parameters — physics constants, quantum gate primitives, POSIX semantics, Y combinator non-termination, the intentionally-typed hom_functor). The unsound pair: Axiom eval_respects_state_eq_right : forall p s s' s'', eval p s s' -> s' =st= s'' -> eval p s s''. Axiom eval_respects_state_eq_left : forall p s s' s'', eval p s' s'' -> s =st= s' -> eval p s s''. These cannot hold under the rescue branch's PC-excluding [state_eq] (memory + registers + I/O — see ADR-006): two states can be [=st=] yet carry different [state_pc], while [eval] deterministically propagates PC through every step constructor. The axiomatised conclusion would force a syntactically-identical eval result, which is impossible without coincidental PC match. The TODO comment in CNO.v acknowledged "prove this axiom by induction on eval structure" — a proof attempt hits the PC mismatch and fails. This commit *deletes* both axioms outright and refactors the only two consumers: - [cno_eval_on_equal_states] (CNO.v, line ~662) — previously chose the same existential witness for both forward and backward directions, needing [eval_respects_state_eq_left]. The lemma states a termination *iff*; different witnesses suffice. Re-proved using [cno_terminates] alone (witnesses from is_CNO p, no axiom). `Print Assumptions cno_eval_on_equal_states.` → "Closed under the global context". - [cno_logically_reversible] (StatMech.v, line ~296) — previously produced [eval p s' s] from [eval p s' s''] + [s'' =st= s] via [eval_respects_state_eq_right]. Cannot hold; reflects the dual unsoundness. Resolved by weakening the *definition* of [logically_reversible] to observational reversibility: Definition logically_reversible (p : Program) : Prop := exists p_inv, forall s s', eval p s s' -> exists s'', eval p_inv s' s'' /\ s'' =st= s. This is the level at which thermodynamic reversibility actually holds: memory + registers + I/O are the bits of physical record; the PC is bookkeeping. No theory is lost — the only theorem citing the strong [logically_reversible] form is [bennett_logical_implies_thermodynamic], whose proof body never uses its hypothesis (explicit "the logically_reversible hypothesis is not used" comment in the source). `Print Assumptions cno_logically_reversible.` → "Closed under the global context". Verification (build-is-oracle): - `coqc -R common CNO common/CNO.v` exit 0 (Coq 8.18.0). - All 11 Coq files under proofs/coq/{common,quantum,lambda,physics, malbolge,category,filesystem} recompile clean. - `Print Assumptions {cno_eval_on_equal_states, cno_logically_reversible, bennett_logical_implies_thermodynamic}` — first two report "Closed under the global context"; the third reports only the abstract Parameter [shannon_entropy] (legitimate model layer, not a proof escape). Net effect on the axiom ledger: 75 → 73 Axioms (deleted 2, no replacement). 42 Parameters unchanged. Docs reconciled in the same commit: - PROOF-STATUS-2026-05-18.md: post-T0 audit table refreshed; 3 discharges shipped (eval_deterministic + the 2 unsound ones); remainder classified as legitimate model-layer assumptions. - .machine_readable/6a2/STATE.a2ml: components.coq-proofs note rebuilt; session-history prepended. - .machine_readable/6a2/META.a2ml + META.scm: ADR-008 added recording the deletion + refactor + rationale. Refs hyperpolymath/standards#124 Refs hyperpolymath/standards#133 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Opus 4.7 (1M context) --- .machine_readable/6a2/META.a2ml | 1 + .machine_readable/6a2/STATE.a2ml | 5 ++- .machine_readable/META.scm | 3 +- PROOF-STATUS-2026-05-18.md | 26 +++++++++++-- proofs/coq/common/CNO.v | 64 ++++++++++++-------------------- proofs/coq/physics/StatMech.v | 27 ++++++++++---- 6 files changed, 72 insertions(+), 54 deletions(-) diff --git a/.machine_readable/6a2/META.a2ml b/.machine_readable/6a2/META.a2ml index 335aa23..442677b 100644 --- a/.machine_readable/6a2/META.a2ml +++ b/.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] diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index 5699078..a8af850 100644 --- a/.machine_readable/6a2/STATE.a2ml +++ b/.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" }, diff --git a/.machine_readable/META.scm b/.machine_readable/META.scm index 00a2d70..bb017d6 100644 --- a/.machine_readable/META.scm +++ b/.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") diff --git a/PROOF-STATUS-2026-05-18.md b/PROOF-STATUS-2026-05-18.md index 5ca6fd5..9cacf5a 100644 --- a/PROOF-STATUS-2026-05-18.md +++ b/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`. diff --git a/proofs/coq/common/CNO.v b/proofs/coq/common/CNO.v index eb31e5a..193835c 100644 --- a/proofs/coq/common/CNO.v +++ b/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. diff --git a/proofs/coq/physics/StatMech.v b/proofs/coq/physics/StatMech.v index 5fb5ec6..23a7ccb 100644 --- a/proofs/coq/physics/StatMech.v +++ b/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 *)