docs+annotate: Physics cluster — 38 inline AXIOM: + 4 §(d) DEBT entries (Phase 2e)

Annotates the Physics cluster per standards#203 trusted-base policy:

- 11 inline `(* AXIOM: ... *)` in `proofs/coq/physics/LandauerDerivation.v`
  (Boltzmann constant, temperature, Kolmogorov + Shannon axioms, second
  law, entropy_change_erasure, isothermal_work_bound, state_eq_dec — all
  §(c); duplicates flagged for follow-up 1+3).
- 9 inline `(* AXIOM: ... *)` in `proofs/coq/physics/StatMech.v` (same
  pattern; cross-references to LandauerDerivation duplicates).
- 14 inline `-- AXIOM:` in `proofs/lean4/StatMech.lean` (mirrors Coq
  §(c) classifications).
- New "Phase 2e triage — Lean StatMech cluster" section in docs/proof-debt.md
  classifying all 14 Lean axioms (all §(c); Coq counterpart for
  reversible_zero_dissipation is DISCHARGE but Lean stays §(c) until
  a derivation chain lands).
- 4 new §(d) DEBT entries in docs/proof-debt.md (Coq DISCHARGE-class):
  - StatMech.v:229 reversible_zero_dissipation
  - LandauerDerivation.v:81 shannon_entropy_additive
  - LandauerDerivation.v:277 cno_preserves_shannon_entropy
  - LandauerDerivation.v:326 cno_zero_energy_dissipation_derived
- Lean pending-triage count: 14 → 0 (Lean side fully classified).

`check-trusted-base.sh`: 42/129 → 4/129 undocumented (38-drop matching
11 + 9 + 14 + 4 = 38 newly documented markers). Physics cluster is
0 errors. Remaining 4 = Idris2 `src/abi/Proofs/DivMod.idr` (out of
Phase 2 scope; BoJ vendored proofs).

Refs: docs/proof-debt-triage.md (Phase 1 #58); Phase 2a (#60),
Phase 2b (#61), Phase 2c (#62), Phase 2d (#63).

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

docs/proof-debt.md

@@ -136,6 +136,42 @@ once a concrete basis-state model lands.
 All 11 §(c) entries above are annotated inline with `-- AXIOM:`
 leading comments.
 
+## Phase 2e triage — Lean StatMech cluster (2026-05-27)
+
+Fourth Lean cluster: `proofs/lean4/StatMech.lean` (14 axioms).
+
+### Physical constants (§(c) AXIOM — duplicate of Coq, 4)
+
+| Line | Identifier | Disposition |
+|-----:|------------|-------------|
+|  23  | `kB`                    | §(c) AXIOM (opaque, mirrors Coq StatMech.v:25) |
+|  24  | `kB_positive`           | §(c) AXIOM (mirrors Coq StatMech.v:25) |
+|  27  | `temperature`           | §(c) AXIOM (opaque, mirrors Coq StatMech.v:30) |
+|  28  | `temperature_positive`  | §(c) AXIOM (mirrors Coq StatMech.v:30) |
+
+### Probability + Shannon entropy (§(c) AXIOM — mirror Coq, 5)
+
+| Line | Identifier | Disposition |
+|-----:|------------|-------------|
+|  36  | `prob_nonneg`               | §(c) AXIOM (mirrors Coq StatMech.v:39) |
+|  40  | `prob_normalized`           | §(c) AXIOM (mirrors Coq StatMech.v:45) |
+|  51  | `shannonEntropy`            | §(c) AXIOM (opaque entropy functional) |
+|  54  | `shannon_entropy_nonneg`    | §(c) AXIOM (mirrors Coq StatMech.v:67) |
+|  58  | `shannon_entropy_point_zero`| §(c) AXIOM (mirrors Coq StatMech.v:72) |
+
+### Landauer + execution model (§(c) AXIOM, 5)
+
+| Line | Identifier | Disposition |
+|-----:|------------|-------------|
+|  91  | `energyDissipatedPhys`     | §(c) AXIOM (opaque physical energy primitive) |
+|  95  | `landauer_principle`       | §(c) AXIOM (mirrors Coq StatMech.v:132) |
+| 107  | `postExecutionDist`        | §(c) AXIOM (opaque execution-distribution primitive) |
+| 116  | `postExecutionDist_id_of_state_preserving` | §(c) AXIOM (bridge to per-state semantics; required because `postExecutionDist` is opaque) |
+| 142  | `reversible_zero_dissipation` | §(c) AXIOM (Coq counterpart is DISCHARGE; Lean keeps as §(c) until derivation chain lands) |
+
+All 14 §(c) entries above are annotated inline with `-- AXIOM:`
+leading comments.
+
 ## (a) DISCHARGE backlog (Coq, 17)
 
 Provable propositions currently stated as `Axiom`. Enumerated in
@@ -250,6 +286,34 @@ no longer in §(d).
     Triaged DISCHARGE in #58 (Phase 2d).
   - **Deadline**: INDEFINITE.
 
+- `proofs/coq/physics/StatMech.v:229` — `reversible_zero_dissipation`
+  - **Owner**: @hyperpolymath
+  - **Plan**: derivable from `landauer_principle` + reversibility
+    hypothesis. Triaged DISCHARGE in #58 (Phase 2e).
+  - **Deadline**: INDEFINITE.
+
+- `proofs/coq/physics/LandauerDerivation.v:81` — `shannon_entropy_additive`
+  - **Owner**: @hyperpolymath
+  - **Plan**: chain rule of entropy; provable from the definition of
+    `H(X,Y)` given an independence hypothesis. Triaged DISCHARGE in #58
+    (Phase 2e).
+  - **Deadline**: INDEFINITE (blocked on `product_dist` semantics).
+
+- `proofs/coq/physics/LandauerDerivation.v:277` — `cno_preserves_shannon_entropy`
+  - **Owner**: @hyperpolymath
+  - **Plan**: should follow from the CNO definition (state in = state
+    out) + functional Shannon entropy. Triaged DISCHARGE in #58 (Phase 2e).
+  - **Deadline**: INDEFINITE (blocked on bijection-preserves-entropy
+    machinery).
+
+- `proofs/coq/physics/LandauerDerivation.v:326` — `cno_zero_energy_dissipation_derived`
+  - **Owner**: @hyperpolymath
+  - **Plan**: name literally says `_derived`; the file admits this
+    rather than discharging it. Should follow from
+    `cno_preserves_shannon_entropy` + Landauer. Triaged DISCHARGE in #58
+    (Phase 2e).
+  - **Deadline**: INDEFINITE.
+
 ### Lean — provable, awaiting proof
 
 - `proofs/lean4/LambdaCNO.lean:183` — `subst_closed_term`
@@ -299,10 +363,9 @@ no longer in §(d).
 
 ### Lean — pending triage
 
-14 Lean axioms remain to be triaged (StatMech only; Lambda, Filesystem,
-and QuantumCNO clusters done in Phase 2a/2c/2d). Triage planned in
-cluster-sized PRs through 2026-06 — see this file's status block at
-the bottom.
+0 Lean axioms remain to be triaged — Lambda (Phase 2a), Filesystem
+(Phase 2c), QuantumCNO (Phase 2d), and StatMech (Phase 2e) clusters
+all done. Lean side fully classified per standards#203 as of 2026-05-27.
 
 ### Idris2 — pending triage
 

proofs/coq/physics/LandauerDerivation.v

@@ -25,10 +25,16 @@ Open Scope R_scope.
 (** 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 *)
@@ -37,14 +43,24 @@ Axiom temperature_positive : temperature > 0.
 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) *)
@@ -60,14 +76,22 @@ Parameter shannon_entropy : StateDistribution -> R.
 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). *)
 Axiom shannon_entropy_uniform_max :
   forall (P : StateDistribution) (n : nat) (states : list ProgramState),
     length states = n ->
@@ -78,6 +102,9 @@ Axiom shannon_entropy_uniform_max :
 Parameter product_dist : StateDistribution -> StateDistribution -> StateDistribution.
 
 (** Entropy is additive for independent distributions *)
+(* Triaged DISCHARGE in docs/proof-debt-triage.md; enumerated as §(d) DEBT
+   in docs/proof-debt.md (Phase 2e) — chain rule of entropy, provable from
+   the definition of `H(X,Y)` given independence hypothesis. *)
 Axiom shannon_entropy_additive :
   forall P Q : StateDistribution,
     (* For independent P and Q *)
@@ -123,6 +150,8 @@ Qed.
     ΔS ≥ 0 for irreversible processes
     ΔS = 0 for reversible processes *)
 
+(* AXIOM: second_law; Physical postulate (second law of thermodynamics).
+   §(c) per docs/proof-debt.md (Phase 2e triage). *)
 Axiom second_law :
   forall (P_initial P_final : StateDistribution),
     (* For any physical process *)
@@ -178,6 +207,8 @@ Definition erasure_final (s_final : ProgramState) : StateDistribution :=
 
     This is a fundamental result from information theory.
 *)
+(* AXIOM: entropy_change_erasure; Landauer–Bennett result.
+   §(c) per docs/proof-debt.md (Phase 2e triage). *)
 Axiom entropy_change_erasure :
   forall (n : nat) (s_final : ProgramState),
     (n > 0)%nat ->
@@ -194,6 +225,8 @@ Axiom entropy_change_erasure :
     This is the minimum work that must be dissipated as heat.
 *)
 
+(* AXIOM: isothermal_work_bound; Thermodynamic bound (Helmholtz free energy).
+   §(c) per docs/proof-debt.md (Phase 2e triage). *)
 Axiom isothermal_work_bound :
   forall (P_initial P_final : StateDistribution),
     work_dissipated P_initial P_final >=
@@ -274,6 +307,9 @@ Definition post_execution_dist (p : Program) (P : StateDistribution) : StateDist
     and μ is a probability measure, then H(μ) = H(T_*μ) where T_*μ is the
     pushforward measure. For the identity map, T_*μ = μ.
 *)
+(* Triaged DISCHARGE in docs/proof-debt-triage.md; enumerated as §(d) DEBT
+   in docs/proof-debt.md (Phase 2e) — should follow from the CNO definition
+   (state in = state out) + functional Shannon entropy. *)
 Axiom cno_preserves_shannon_entropy :
   forall (p : Program) (P : StateDistribution),
     is_CNO p ->
@@ -323,6 +359,9 @@ Qed.
     and is safely axiomatized given the complexity of the thermodynamic machinery
     required for a complete proof.
 *)
+(* Triaged DISCHARGE in docs/proof-debt-triage.md; enumerated as §(d) DEBT
+   in docs/proof-debt.md (Phase 2e) — name literally says `_derived`; this
+   file appears to admit the result rather than discharge it. *)
 Axiom cno_zero_energy_dissipation_derived :
   forall (p : Program) (P : StateDistribution),
     is_CNO p ->

proofs/coq/physics/StatMech.v

@@ -22,11 +22,17 @@ Open Scope R_scope.
 
 (** 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 *)
 
@@ -36,18 +42,28 @@ Axiom temperature_positive : temperature > 0.
 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}.
 
@@ -64,16 +80,24 @@ Definition point_dist (s0 : ProgramState) : StateDistribution :=
 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.
 
 (** Axiom: Entropy is maximized for uniform distribution *)
+(* AXIOM: shannon_entropy_maximum; H ≤ log n (Gibbs inequality).
+   §(c) per docs/proof-debt.md (Phase 2e triage). *)
 Axiom shannon_entropy_maximum :
   forall (P : StateDistribution) (states : list ProgramState),
     (forall s1 s2, In s1 states -> In s2 states -> P s1 = P s2) ->
@@ -129,6 +153,8 @@ Qed.
 (** Energy dissipated by a computational process (Joules) *)
 Parameter energy_dissipated_phys : StateDistribution -> StateDistribution -> R.
 
+(* AXIOM: landauer_principle; Physical postulate (Landauer's principle).
+   §(c) per docs/proof-debt.md (Phase 2e triage). *)
 Axiom landauer_principle :
   forall (P_initial P_final : StateDistribution),
     let ΔS := shannon_entropy P_final - shannon_entropy P_initial in
@@ -226,6 +252,9 @@ Qed.
 
 (** Physical axiom: Reversible processes (ΔS = 0) dissipate no energy *)
 (** This is a consequence of Landauer's Principle and thermodynamic reversibility *)
+(* Triaged DISCHARGE in docs/proof-debt-triage.md; enumerated as §(d) DEBT
+   in docs/proof-debt.md (Phase 2e) — derivable from `landauer_principle`
+   + reversibility hypothesis. *)
 Axiom reversible_zero_dissipation :
   forall P_initial P_final : StateDistribution,
     shannon_entropy P_initial = shannon_entropy P_final ->