refactor(proofs/coq): Follow-ups 2 + 3 — consolidate quantum-law dups + statmech basis

hyperpolymath · claude · hyperpolymath · commit ce1f3191153c · 2026-05-27T12:30:21.000+01:00
Builds on Follow-up 1 (PhysicsConstants.v) with the remaining two mechanical dedupes from docs/proof-debt-triage.md. Follow-up 2 — dead duplicate axioms removed from QuantumMechanicsExact.v: - `unitary_preserves_entropy` (line 323) — was dead code; canonical lives in QuantumCNO.v (which uses an unindexed `QuantumGate`, the only form with downstream callers). - `no_cloning` (line 404) — was dead code AND its statement `forall ψ, False` was trivially `True`-equivalent. Canonical in QuantumCNO.v. Follow-up 3 — statmech basis consolidated: - New file `proofs/coq/common/StatMechBasis.v` declares once: `StateDistribution`, `prob_nonneg`, `prob_normalized`, `state_dec`, `point_dist`, `shannon_entropy` (parameter), `shannon_entropy_nonneg`, `shannon_entropy_point_zero`. - `StatMech.v` and `LandauerDerivation.v` import via `Require Import CNO.StatMechBasis` and drop their local copies. - `state_eq_dec` aliased into canonical `state_dec` (LandauerDerivation only used the local name internally; no external callers). Cleanup + machine-readable: - `.gitignore`: adds Coq build artefact patterns (*.vo, *.vok, *.vos, *.glob, .*.aux, .lia.cache, .nia.cache) so future builds don't pollute status output. - `_CoqProject`: adds `common/StatMechBasis.v` to the build manifest (alongside PhysicsConstants.v from Follow-up 1). - `.machine_readable/META.scm`: ADR-011 (Phase 2a–2e Lean triage) and ADR-012 (Follow-ups 1–3 consolidation) recorded. - `docs/proof-debt-triage.md`: Follow-ups 2 + 3 marked DONE. Verification: - `coqc -R common CNO common/{PhysicsConstants,Complex,CNO,StatMechBasis}.v` — OK - `coqc -R common CNO physics/{StatMech,LandauerDerivation}.v` — OK - `coqc -R common CNO quantum/{QuantumCNO,QuantumMechanicsExact}.v` — OK - `check-trusted-base.sh` — 4/118 undocumented (remaining 4 are Idris2 `src/abi/Proofs/DivMod.idr`; out of Phase 2 scope). Net change since Phase 2e closeout (#66): 129 → 118 markers, −11. Refs: docs/proof-debt-triage.md (Phase 1 #58); Phase 2a (#60), Phase 2b (#61), Phase 2c (#62), Phase 2d (#63), Phase 2e (#66). 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
diff --git a/.gitignore b/.gitignore
@@ -82,5 +82,14 @@ htmlcov/
 ai-cli-crash-capture/
 proofs/lean4/.lake/
 
+# Coq build outputs
+*.vo
+*.vok
+*.vos
+*.glob
+.*.aux
+.lia.cache
+.nia.cache
+
 # Rust build outputs in subdirectories (e.g. fuzz/target/)
 **/target/
diff --git a/.machine_readable/META.scm b/.machine_readable/META.scm
@@ -13,7 +13,9 @@
      ("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)")
      ("ADR-009" "accepted" "Delete unsound alignmentMatchesPlatformWord Idris2 postulate (HasAlignment carries no evidence; would derive So (1 mod 8 == 0) from CNOResultLayout.alignment); replace single consumer with per-Platform decidable proof. Consolidate remaining alignedSizeCorrect postulate into shared AbsoluteZero.ABI.Proofs.DivMod module as the estate-wide div/mod lemma surface (absolute-zero#27, civic-connect alignUpDivides/mkFieldsAligned/offsetInBoundsPrf migrate here)")
-     ("ADR-010" "accepted" "Phase 1 per-axiom triage of 72 Coq Axioms per standards#203 trusted-base policy (2026-05-27, PR #58): 52 §c TRUSTED-BASE + 17 §a DISCHARGE backlog + 3 §b PROPERTY-TEST; canonical disposition in docs/proof-debt-triage.md")))
+     ("ADR-010" "accepted" "Phase 1 per-axiom triage of 72 Coq Axioms per standards#203 trusted-base policy (2026-05-27, PR #58): 52 §c TRUSTED-BASE + 17 §a DISCHARGE backlog + 3 §b PROPERTY-TEST; canonical disposition in docs/proof-debt-triage.md")
+     ("ADR-011" "accepted" "Phase 2a–2e Lean triage + inline annotations across Lambda, CNOCategory, Filesystem, Quantum, StatMech clusters (2026-05-27, PRs #60/#61/#62/#63/#66): 52 Lean axioms classified (49 §c + 3 §d); 4 §d Coq DISCHARGE entries surfaced for Physics cluster")
+     ("ADR-012" "accepted" "Follow-ups 1–3 consolidation: physics constants → common/PhysicsConstants.v, statmech basis (prob_*/state_dec/shannon_entropy*) → common/StatMechBasis.v, dead QuantumMechanicsExact.v duplicates of unitary_preserves_entropy + no_cloning removed (2026-05-27, PR #67); net 129 → 118 trusted-base markers (−11)")))
 
   (development-practices
     (code-style "Coq proof engineering")
diff --git a/docs/proof-debt-triage.md b/docs/proof-debt-triage.md
@@ -167,13 +167,27 @@ triage PR.
    consolidated in `proofs/coq/common/PhysicsConstants.v` and imported
    via `Require Import CNO.PhysicsConstants`. Net: 129 → 125 markers
    (−4: removed 6 sites, added 2 canonical sites).
-2. **De-duplicate quantum laws.** `unitary_preserves_entropy` and
-   `no_cloning` appear in both `QuantumMechanicsExact.v` and
-   `QuantumCNO.v` with the same name. Pick one as canonical.
+2. **De-duplicate quantum laws.** ✅ DONE 2026-05-27.
+   `unitary_preserves_entropy` and `no_cloning` previously appeared in
+   both `QuantumMechanicsExact.v` and `QuantumCNO.v` with the same
+   name. The `QuantumMechanicsExact.v` copies were dead code (no
+   in-file usage; `no_cloning`'s statement was trivially `True`-equivalent)
+   so they were removed. `QuantumCNO.v` is the canonical declaration
+   for both. Net: −2 markers in `QuantumMechanicsExact.v`. The
+   `X_gate_unitary` name-shadow noted in the per-axiom table refers to
+   axiomatisations of two distinct gate definitions (indexed vs
+   unindexed `QuantumGate`); not consolidated here.
 3. **De-duplicate decidability + probability + Shannon axioms.**
-   `prob_nonneg`, `prob_normalized`, `state_eq_dec`/`state_dec`,
-   `shannon_entropy_nonneg`, `shannon_entropy_point_zero` are
-   duplicated between `StatMech.v` and `LandauerDerivation.v`.
+   ✅ DONE 2026-05-27. `prob_nonneg`, `prob_normalized`, `state_dec`
+   (canonical name; subsumes `state_eq_dec`), `shannon_entropy`
+   (parameter), `shannon_entropy_nonneg`, `shannon_entropy_point_zero`,
+   and the `point_dist` definition are now in
+   `proofs/coq/common/StatMechBasis.v` and imported by both
+   `StatMech.v` and `LandauerDerivation.v` via
+   `Require Import CNO.StatMechBasis`. Net: 125 → 118 markers (−7:
+   removed 12 sites incl. the `shannon_entropy` parameter duplicate,
+   added 5 canonical axiom sites; `state_eq_dec` aliased to canonical
+   `state_dec`).
 4. **Constructively define `Cexp` in `Complex.v`.** `Complex.v` has
    zero axioms today; if it defines `Cexp` from a power series (or
    imports from a Coq reals/complex stdlib), the four `Cexp_*` axioms
diff --git a/proofs/coq/_CoqProject b/proofs/coq/_CoqProject
@@ -3,4 +3,5 @@
 
 common/PhysicsConstants.v
 common/CNO.v
+common/StatMechBasis.v
 malbolge/MalbolgeCore.v
diff --git a/proofs/coq/common/StatMechBasis.v b/proofs/coq/common/StatMechBasis.v
@@ -0,0 +1,75 @@
+(** * Statistical Mechanics Basis — Shared Probability + Entropy Axioms
+
+    Single source of truth for the Kolmogorov-style probability axioms,
+    state-equality decision procedure, point distribution, Shannon
+    entropy parameter, and the two core Shannon-entropy inequalities
+    used by both [StatMech.v] and [LandauerDerivation.v].
+    Consolidates duplicated declarations (Follow-up 3 of
+    [docs/proof-debt-triage.md]).
+
+    Author: Jonathan D. A. Jewell
+    Project: Absolute Zero
+    License: MPL-2.0
+*)
+
+Require Import Coq.Reals.Reals.
+Require Import Coq.Lists.List.
+Require Import CNO.CNO.
+Import ListNotations.
+
+Open Scope R_scope.
+
+(** ** Probability distributions over [ProgramState] *)
+
+Definition StateDistribution : Type := ProgramState -> R.
+
+(* AXIOM: prob_nonneg; Kolmogorov probability axiom (non-negativity).
+   Consolidated from StatMech.v:39 and LandauerDerivation.v:40
+   (Follow-up 3 of docs/proof-debt-triage.md).
+   §(c) per docs/proof-debt.md. *)
+Axiom prob_nonneg :
+  forall (P : StateDistribution) (s : ProgramState),
+    P s >= 0.
+
+(* Consolidated from StatMech.v:45 and LandauerDerivation.v:43
+   (Follow-up 3). Picked the `map P` form from StatMech.v; the
+   LandauerDerivation form (fold_right with explicit lambda) is
+   equivalent. AXIOM: prob_normalized; Kolmogorov axiom (Σp = 1).
+   §(c) per docs/proof-debt.md. *)
+Axiom prob_normalized :
+  forall (P : StateDistribution),
+    exists (states : list ProgramState),
+      fold_right Rplus 0 (map P states) = 1.
+
+(** ** Decidable equality on [ProgramState] *)
+
+(* Consolidated from StatMech.v:51 (`state_dec`) and
+   LandauerDerivation.v:48 (`state_eq_dec`); canonical name picked:
+   `state_dec` (Follow-up 3). AXIOM: state_dec; decidable equality
+   over opaque `ProgramState`; PROPERTY-TEST (§(b)) — treated as §(c)
+   until a property-test budget is attached. *)
+Axiom state_dec :
+  forall s1 s2 : ProgramState, {s1 = s2} + {s1 <> s2}.
+
+(** Point distribution (Dirac delta) over [ProgramState]. *)
+Definition point_dist (s0 : ProgramState) : StateDistribution :=
+  fun s => if state_dec s s0 then 1 else 0.
+
+(** ** Shannon entropy *)
+
+(** Shannon entropy: [H(P) = -Σ p(s) log₂ p(s)], measured in bits. *)
+Parameter shannon_entropy : StateDistribution -> R.
+
+(* AXIOM: shannon_entropy_nonneg; Shannon entropy core inequality.
+   Consolidated from StatMech.v:67 and LandauerDerivation.v:63
+   (Follow-up 3 of docs/proof-debt-triage.md).
+   §(c) per docs/proof-debt.md. *)
+Axiom shannon_entropy_nonneg :
+  forall P : StateDistribution, shannon_entropy P >= 0.
+
+(* AXIOM: shannon_entropy_point_zero; H(δ_x) = 0. Consolidated from
+   StatMech.v:72 and LandauerDerivation.v:67 (Follow-up 3 of
+   docs/proof-debt-triage.md).
+   §(c) per docs/proof-debt.md. *)
+Axiom shannon_entropy_point_zero :
+  forall s : ProgramState, shannon_entropy (point_dist s) = 0.
diff --git a/proofs/coq/physics/LandauerDerivation.v b/proofs/coq/physics/LandauerDerivation.v
@@ -20,6 +20,11 @@ Require Import CNO.CNO.
    temperature_positive. See proofs/coq/common/PhysicsConstants.v
    (consolidated by Follow-up 1 of docs/proof-debt-triage.md). *)
 Require Import CNO.PhysicsConstants.
+(* Shared statmech basis — StateDistribution, prob_nonneg, prob_normalized,
+   state_dec, point_dist, shannon_entropy, shannon_entropy_nonneg,
+   shannon_entropy_point_zero. See proofs/coq/common/StatMechBasis.v
+   (consolidated by Follow-up 3 of docs/proof-debt-triage.md). *)
+Require Import CNO.StatMechBasis.
 Import ListNotations.
 
 Open Scope R_scope.
@@ -31,58 +36,16 @@ Open Scope R_scope.
     (consolidated by Follow-up 1). These are measured physical constants,
     grounded in experiment. *)
 
-(** ** Foundation: Probability Theory *)
+(** ** Foundation: Probability + Shannon Entropy Basis
 
-(** A probability distribution over program states *)
-Definition StateDistribution : Type := ProgramState -> R.
-
-(** Probability axioms (Kolmogorov) *)
-(* AXIOM: prob_nonneg; Kolmogorov probability axiom (non-negativity).
-   Duplicate of StatMech.v:39 (see follow-up 3 in docs/proof-debt-triage.md).
-   §(c) per docs/proof-debt.md (Phase 2e triage). *)
-Axiom prob_nonneg :
-  forall (P : StateDistribution) (s : ProgramState), P s >= 0.
-
-(* AXIOM: prob_normalized; Kolmogorov probability axiom (Σp = 1).
-   Duplicate of StatMech.v:45 (see follow-up 3).
-   §(c) per docs/proof-debt.md (Phase 2e triage). *)
-Axiom prob_normalized :
-  forall (P : StateDistribution),
-    exists (states : list ProgramState),
-      fold_right (fun s acc => acc + P s) 0 states = 1.
-
-(* AXIOM: state_eq_dec; Decidable equality over opaque `ProgramState`;
-   needs oracle or §(b) refutation budget. Duplicate of StatMech.v:51
-   `state_dec` (see follow-up 3). PROPERTY-TEST (§(b)) — treated as §(c)
-   until a property-test budget is attached. *)
-Axiom state_eq_dec : forall s1 s2 : ProgramState, {s1 = s2} + {s1 <> s2}.
-
-(** Point distribution (Dirac delta) *)
-Definition point_dist (s0 : ProgramState) : StateDistribution :=
-  fun s => if state_eq_dec s s0 then 1 else 0.
-
-(** ** Shannon Entropy: Information-Theoretic Foundation *)
-
-(** Shannon entropy: H(P) = -Σ p_i log_2(p_i)
-    Measured in bits *)
-Parameter shannon_entropy : StateDistribution -> R.
+    [StateDistribution], [prob_nonneg], [prob_normalized], [state_dec],
+    [point_dist], [shannon_entropy], [shannon_entropy_nonneg], and
+    [shannon_entropy_point_zero] are imported from [CNO.StatMechBasis]
+    (consolidated by Follow-up 3 of [docs/proof-debt-triage.md]). This
+    file adds [log2] and the uniform-max / additive axioms below. *)
 
 Definition log2 (x : R) : R := ln x / ln 2.
 
-(** Shannon entropy axioms (from information theory) *)
-(* AXIOM: shannon_entropy_nonneg; Shannon entropy core inequality.
-   Duplicate of StatMech.v:67 (see follow-up 3).
-   §(c) per docs/proof-debt.md (Phase 2e triage). *)
-Axiom shannon_entropy_nonneg :
-  forall P : StateDistribution, shannon_entropy P >= 0.
-
-(** Point distributions have zero entropy (no uncertainty) *)
-(* AXIOM: shannon_entropy_point_zero; H(δ_x) = 0. Duplicate of
-   StatMech.v:72 (see follow-up 3).
-   §(c) per docs/proof-debt.md (Phase 2e triage). *)
-Axiom shannon_entropy_point_zero :
-  forall s : ProgramState, shannon_entropy (point_dist s) = 0.
-
 (** Entropy is maximized for uniform distribution *)
 (* AXIOM: shannon_entropy_uniform_max; Variant of Gibbs inequality for
    uniform distributions. §(c) per docs/proof-debt.md (Phase 2e triage). *)
diff --git a/proofs/coq/physics/StatMech.v b/proofs/coq/physics/StatMech.v
@@ -18,6 +18,11 @@ Require Import CNO.CNO.
    temperature_positive. See proofs/coq/common/PhysicsConstants.v
    (consolidated by Follow-up 1 of docs/proof-debt-triage.md). *)
 Require Import CNO.PhysicsConstants.
+(* Shared statmech basis — StateDistribution, prob_nonneg, prob_normalized,
+   state_dec, point_dist, shannon_entropy, shannon_entropy_nonneg,
+   shannon_entropy_point_zero. See proofs/coq/common/StatMechBasis.v
+   (consolidated by Follow-up 3 of docs/proof-debt-triage.md). *)
+Require Import CNO.StatMechBasis.
 Import ListNotations.
 
 Open Scope R_scope.
@@ -28,64 +33,12 @@ Open Scope R_scope.
     imported from [CNO.PhysicsConstants] (consolidated by Follow-up 1).
     In SI units: [kB ≈ 1.380649×10⁻²³ J/K]; room temperature ≈ 300 K. *)
 
-(** ** Probability Distributions *)
+(** ** Probability Distributions, Entropy
 
-(** A probability distribution over program states *)
-Definition StateDistribution : Type := ProgramState -> R.
-
-(** Axiom: Probabilities are non-negative *)
-(* AXIOM: prob_nonneg; Kolmogorov probability axiom (non-negativity).
-   Duplicate of LandauerDerivation.v:40 (see follow-up 3).
-   §(c) per docs/proof-debt.md (Phase 2e triage). *)
-Axiom prob_nonneg :
-  forall (P : StateDistribution) (s : ProgramState),
-    P s >= 0.
-
-(** Axiom: Probabilities sum to 1 (normalization) *)
-(** Note: Proper formalization requires measure theory *)
-(* AXIOM: prob_normalized; Kolmogorov probability axiom (Σp = 1).
-   Duplicate of LandauerDerivation.v:43 (see follow-up 3).
-   §(c) per docs/proof-debt.md (Phase 2e triage). *)
-Axiom prob_normalized :
-  forall (P : StateDistribution),
-    exists (states : list ProgramState),
-      fold_right Rplus 0 (map P states) = 1.
-
-(** State decidability *)
-(* AXIOM: state_dec; Decidable equality over opaque `ProgramState`; needs
-   oracle or §(b) refutation budget. Duplicate of LandauerDerivation.v:48
-   `state_eq_dec` (see follow-up 3). PROPERTY-TEST (§(b)) — treated as
-   §(c) until a property-test budget is attached. *)
-Axiom state_dec :
-  forall s1 s2 : ProgramState, {s1 = s2} + {s1 <> s2}.
-
-(** Point distribution (all probability on one state) *)
-Definition point_dist (s0 : ProgramState) : StateDistribution :=
-  fun s => if state_dec s s0 then 1 else 0.
-
-(** ** Information-Theoretic Entropy *)
-
-(** Shannon entropy: H(P) = -Σ p(s) log₂ p(s)
-
-    Measured in bits (using log base 2)
-*)
-Parameter shannon_entropy : StateDistribution -> R.
-
-(** Axiom: Shannon entropy is non-negative *)
-(* AXIOM: shannon_entropy_nonneg; Shannon entropy core inequality. Duplicate
-   of LandauerDerivation.v:63 (see follow-up 3).
-   §(c) per docs/proof-debt.md (Phase 2e triage). *)
-Axiom shannon_entropy_nonneg :
-  forall P : StateDistribution,
-    shannon_entropy P >= 0.
-
-(** Axiom: Point distributions have zero entropy *)
-(* AXIOM: shannon_entropy_point_zero; H(δ_x) = 0. Duplicate of
-   LandauerDerivation.v:67 (see follow-up 3).
-   §(c) per docs/proof-debt.md (Phase 2e triage). *)
-Axiom shannon_entropy_point_zero :
-  forall s : ProgramState,
-    shannon_entropy (point_dist s) = 0.
+    [StateDistribution], [prob_nonneg], [prob_normalized], [state_dec],
+    [point_dist], [shannon_entropy], [shannon_entropy_nonneg], and
+    [shannon_entropy_point_zero] are imported from [CNO.StatMechBasis]
+    (consolidated by Follow-up 3 of [docs/proof-debt-triage.md]). *)
 
 (** Axiom: Entropy is maximized for uniform distribution *)
 (* AXIOM: shannon_entropy_maximum; H ≤ log n (Gibbs inequality).
diff --git a/proofs/coq/quantum/QuantumMechanicsExact.v b/proofs/coq/quantum/QuantumMechanicsExact.v
@@ -315,16 +315,13 @@ Qed.
 
     The result is deeply connected to the fact that quantum mechanics is
     deterministic at the level of pure state evolution (Schrödinger equation).
-*)
-(* AXIOM: unitary_preserves_entropy; Quantum statmech postulate (von Neumann
-   entropy invariant under unitary). Duplicate of QuantumCNO:372 (see
-   follow-up 2 in docs/proof-debt-triage.md).
-   §(c) per docs/proof-debt.md (Phase 2d triage). *)
-Axiom unitary_preserves_entropy :
-  forall (n : nat) (U : QuantumGate n) (ψ : QuantumState n),
-    is_unitary U ->
-    is_normalized ψ ->
-    von_neumann_entropy (U ψ) = von_neumann_entropy ψ.
+
+    Canonical declaration: see `unitary_preserves_entropy` in
+    `proofs/coq/quantum/QuantumCNO.v` (Follow-up 2 of
+    `docs/proof-debt-triage.md`). The QuantumMechanicsExact.v duplicate
+    was dead code (no in-file usage) and has been removed to reduce
+    the trust base; downstream callers in this file's namespace use the
+    QuantumCNO version (with the unindexed `QuantumGate` type). *)
 
 (** ** Quantum CNO Definition (Exact) *)
 
@@ -396,16 +393,13 @@ Qed.
 
     The no-cloning theorem is a direct consequence of the linearity of quantum
     mechanics and is empirically confirmed through countless quantum experiments.
-*)
-(* AXIOM: no_cloning; Fundamental quantum theorem; standardly taken as
-   physical postulate in this style of axiomatisation. Duplicate of
-   QuantumCNO:391 (see follow-up 2 in docs/proof-debt-triage.md).
-   §(c) per docs/proof-debt.md (Phase 2d triage). *)
-Axiom no_cloning :
-  ~ exists (U : QuantumGate 2),
-      forall (ψ : QuantumState 1),
-        (* Cannot clone arbitrary quantum states *)
-        False.  (* Simplified statement *)
+
+    Canonical declaration: see `no_cloning` in
+    `proofs/coq/quantum/QuantumCNO.v` (Follow-up 2 of
+    `docs/proof-debt-triage.md`). The QuantumMechanicsExact.v duplicate
+    was dead code (no in-file usage, and the previous statement
+    [`forall ψ, False`] was trivially equivalent to [True]) and has
+    been removed to reduce the trust base. *)
 
 (** ** Summary: What is Exact vs. Axiomatized *)
 
