refactor(proofs/coq): consolidate trusted-base dups (Follow-ups 1+2+3)

.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/

.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")

docs/proof-debt-triage.md

@@ -161,17 +161,33 @@ These are concrete sub-projects that fall out of the table. Each is
 its own PR-sized piece of work — none of them is in scope for this
 triage PR.
 
-1. **De-duplicate physics constants.** `kB_positive` and
-   `temperature_positive` are axiomatised three times (QuantumCNO,
-   StatMech, LandauerDerivation). Move to a shared `Physics.Constants`
-   module and import.
-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.
+1. **De-duplicate physics constants.** ✅ DONE 2026-05-27.
+   `kB_positive` and `temperature_positive` previously axiomatised
+   three times (QuantumCNO, StatMech, LandauerDerivation); now
+   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.** ✅ 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

proofs/coq/_CoqProject

@@ -1,5 +1,7 @@
 -R common CNO
 -R malbolge Malbolge
 
+common/PhysicsConstants.v
 common/CNO.v
+common/StatMechBasis.v
 malbolge/MalbolgeCore.v

proofs/coq/common/PhysicsConstants.v

@@ -0,0 +1,39 @@
+(** * Physical Constants — Shared Across CNO Theory
+
+    Single source of truth for the [kB] (Boltzmann constant) and
+    [temperature] parameters that show up in the quantum and statistical
+    mechanics modules. Consolidates triplicated declarations from
+    [QuantumCNO.v], [StatMech.v], and [LandauerDerivation.v] (Follow-up 1
+    of [docs/proof-debt-triage.md]).
+
+    Author: Jonathan D. A. Jewell
+    Project: Absolute Zero
+    License: MPL-2.0
+*)
+
+Require Import Coq.Reals.Reals.
+
+Open Scope R_scope.
+
+(** ** Boltzmann constant *)
+
+(** Boltzmann constant [k_B] (J/K). In SI units:
+    [kB ≈ 1.380649 × 10^{-23} J/K]. *)
+Parameter kB : R.
+
+(* AXIOM: kB_positive; Boltzmann constant — physical constant.
+   Consolidated from QuantumCNO.v:31, StatMech.v:25,
+   LandauerDerivation.v:28 (Follow-up 1 of docs/proof-debt-triage.md).
+   §(c) per docs/proof-debt.md. *)
+Axiom kB_positive : kB > 0.
+
+(** ** Temperature *)
+
+(** Temperature in Kelvin (must be positive). Room temperature ≈ 300 K. *)
+Parameter temperature : R.
+
+(* AXIOM: temperature_positive; Temperature scalar — physical precondition.
+   Consolidated from QuantumCNO.v:35, StatMech.v:30,
+   LandauerDerivation.v:32 (Follow-up 1 of docs/proof-debt-triage.md).
+   §(c) per docs/proof-debt.md. *)
+Axiom temperature_positive : temperature > 0.

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.

proofs/coq/physics/LandauerDerivation.v

@@ -16,79 +16,36 @@ Require Import Coq.micromega.Psatz.
 Require Import Coq.Lists.List.
 Require Import Lia.
 Require Import CNO.CNO.
+(* Shared physics constants — kB, temperature, kB_positive,
+   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.
 
-(** ** Physical Constants (Measured Values, Not Derived) *)
+(** ** Physical Constants (Measured Values, Not Derived)
 
-(** Boltzmann constant: k_B = 1.380649 × 10^-23 J/K *)
-(** This is a measured physical constant, grounded in experiment *)
-Parameter kB : R.
-(* AXIOM: kB_positive; Boltzmann constant — physical constant. Duplicate of
-   StatMech.v:25 + QuantumCNO.v:31 (see follow-up 1 in docs/proof-debt-triage.md).
-   §(c) per docs/proof-debt.md (Phase 2e triage). *)
-Axiom kB_positive : kB > 0.
-
-(** Temperature in Kelvin (must be positive) *)
-Parameter temperature : R.
-(* AXIOM: temperature_positive; Temperature scalar — physical precondition.
-   Duplicate of StatMech.v:30 + QuantumCNO.v:35 (see follow-up 1).
-   §(c) per docs/proof-debt.md (Phase 2e triage). *)
-Axiom temperature_positive : temperature > 0.
-
-(** ** Foundation: Probability Theory *)
+    Boltzmann constant [k_B = 1.380649 × 10^{-23} J/K] and [temperature]
+    in Kelvin (must be positive) are imported from [CNO.PhysicsConstants]
+    (consolidated by Follow-up 1). These are measured physical constants,
+    grounded in experiment. *)
 
-(** 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.
+(** ** Foundation: Probability + Shannon Entropy Basis
 
-(* 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). *)

proofs/coq/physics/StatMech.v

@@ -14,86 +14,31 @@ Require Import Coq.Logic.FunctionalExtensionality.
 Require Import Coq.Lists.List.
 Require Import Coq.micromega.Psatz.
 Require Import CNO.CNO.
+(* Shared physics constants — kB, temperature, kB_positive,
+   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.
 
-(** ** Physical Constants *)
+(** ** Physical Constants
 
-(** Boltzmann constant (J/K) *)
-Parameter kB : R.
-(* AXIOM: kB_positive; Boltzmann constant — physical constant. Duplicate of
-   LandauerDerivation.v:28 + QuantumCNO.v:31 (see follow-up 1).
-   §(c) per docs/proof-debt.md (Phase 2e triage). *)
-Axiom kB_positive : kB > 0.
-(** In SI units: kB ≈ 1.380649×10⁻²³ J/K *)
-
-(** Temperature (Kelvin) *)
-Parameter temperature : R.
-(* AXIOM: temperature_positive; Temperature scalar — physical precondition.
-   Duplicate of LandauerDerivation.v:32 + QuantumCNO.v:35 (see follow-up 1).
-   §(c) per docs/proof-debt.md (Phase 2e triage). *)
-Axiom temperature_positive : temperature > 0.
-(** Room temperature ≈ 300 K *)
-
-(** ** Probability Distributions *)
-
-(** 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}.
+    [kB], [temperature], [kB_positive], and [temperature_positive] are
+    imported from [CNO.PhysicsConstants] (consolidated by Follow-up 1).
+    In SI units: [kB ≈ 1.380649×10⁻²³ J/K]; room temperature ≈ 300 K. *)
 
-(** Point distribution (all probability on one state) *)
-Definition point_dist (s0 : ProgramState) : StateDistribution :=
-  fun s => if state_dec s s0 then 1 else 0.
+(** ** Probability Distributions, Entropy
 
-(** ** 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).