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

docs/proof-debt-triage.md

@@ -161,10 +161,12 @@ 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.
+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.** `unitary_preserves_entropy` and
    `no_cloning` appear in both `QuantumMechanicsExact.v` and
    `QuantumCNO.v` with the same name. Pick one as canonical.

proofs/coq/_CoqProject

@@ -1,5 +1,6 @@
 -R common CNO
 -R malbolge Malbolge
 
+common/PhysicsConstants.v
 common/CNO.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/physics/LandauerDerivation.v

@@ -16,26 +16,20 @@ 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.
 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.
+    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. *)
 
 (** ** Foundation: Probability Theory *)
 

proofs/coq/physics/StatMech.v

@@ -14,27 +14,19 @@ 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.
 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 *)
+    [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. *)
 
 (** ** Probability Distributions *)
 

proofs/coq/quantum/QuantumCNO.v

@@ -20,23 +20,18 @@ Require Import Coq.Reals.Reals.
 Require Import CNO.Complex.
 Require Import Coq.Logic.FunctionalExtensionality.
 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.
 
 Open Scope R_scope.
 Open Scope C_scope.
 
-(** ** Physical Constants (for Landauer principle) *)
+(** ** Physical Constants (for Landauer principle)
 
-(** Boltzmann constant (J/K) *)
-Parameter kB : R.
-(* AXIOM: kB_positive; Boltzmann constant — physical constant.
-   §(c) per docs/proof-debt.md (Phase 2d triage). *)
-Axiom kB_positive : kB > 0.
-
-(** Temperature (Kelvin) *)
-Parameter temperature : R.
-(* AXIOM: temperature_positive; Temperature scalar — physical precondition.
-   §(c) per docs/proof-debt.md (Phase 2d triage). *)
-Axiom temperature_positive : temperature > 0.
+    [kB], [temperature], [kB_positive], and [temperature_positive] are
+    imported from [CNO.PhysicsConstants] (consolidated by Follow-up 1). *)
 
 (** ** Quantum State Representation *)