Skip to content

Commit 0b9b215

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
authored
refactor(proofs/coq): consolidate trusted-base dups (Follow-ups 1+2+3) (#67)
## Summary Mechanical follow-ups 1, 2, 3 from the Phase 1 proof-debt triage (#58). Consolidates triplicated / duplicated trusted-base axioms into shared modules and removes dead duplicate copies, reducing the estate trust base by **11 markers** (129 → 118) without changing semantics. ### Follow-up 1 — physics constants (`PhysicsConstants.v`) - **New**: `proofs/coq/common/PhysicsConstants.v` — single declaration of `kB`, `kB_positive`, `temperature`, `temperature_positive`. - **Updated**: `QuantumCNO.v`, `StatMech.v`, `LandauerDerivation.v` — drop local declarations, `Require Import CNO.PhysicsConstants`. ### Follow-up 2 — quantum laws (dead-code removal in `QuantumMechanicsExact.v`) - **Removed**: `Axiom unitary_preserves_entropy` (line 323) and `Axiom no_cloning` (line 404) from `QuantumMechanicsExact.v`. Both were dead code (no in-file callers). The `no_cloning` body `forall ψ, False` was trivially `True`-equivalent, so removal also strengthens the trust base. - **Canonical**: `QuantumCNO.v` declarations remain (used by `quantum_cno_preserves_information` and friends). ### Follow-up 3 — statmech basis (`StatMechBasis.v`) - **New**: `proofs/coq/common/StatMechBasis.v` — single declaration of `StateDistribution`, `prob_nonneg`, `prob_normalized`, `state_dec` (canonical name; subsumes `state_eq_dec`), `point_dist`, `shannon_entropy`, `shannon_entropy_nonneg`, `shannon_entropy_point_zero`. - **Updated**: `StatMech.v` and `LandauerDerivation.v` — drop local declarations, `Require Import CNO.StatMechBasis`. ### 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. - **`_CoqProject`**: registers `common/PhysicsConstants.v` and `common/StatMechBasis.v` in the build manifest. - **`.machine_readable/META.scm`**: ADR-011 (Phase 2a–2e Lean triage campaign) and ADR-012 (Follow-ups 1–3 consolidation) added to the architecture-decisions ledger. - **`docs/proof-debt-triage.md`**: Follow-ups 1, 2, 3 marked `✅ DONE 2026-05-27` with the consolidation summaries. ## Verification ``` coqc -R common CNO common/PhysicsConstants.v → OK coqc -R common CNO common/Complex.v → OK coqc -R common CNO common/CNO.v → OK coqc -R common CNO common/StatMechBasis.v → OK coqc -R common CNO physics/StatMech.v → OK coqc -R common CNO physics/LandauerDerivation.v → OK coqc -R common CNO quantum/QuantumCNO.v → OK coqc -R common CNO quantum/QuantumMechanicsExact.v → OK ``` `bash ~/developer/repos/standards/scripts/check-trusted-base.sh .`: | | Total markers | Undocumented | |---|---:|---:| | Before this PR (after Phase 2e #66) | 129 | 4 (Idris2 BoJ) | | After this PR | **118** | 4 (Idris2 BoJ, unchanged) | | Delta | **−11** | 0 | The 4 remaining undocumented markers are in `src/abi/Proofs/DivMod.idr` (BoJ vendored proofs) — explicitly out of Phase 2 scope and tracked at #27. ## Why this is low-risk The consolidated axioms are opaque `Parameter`s and `Axiom`s (no executable definitions). Consolidating means all callers now reference the **same** symbol instead of nominally-distinct copies — strictly an improvement for soundness. The dead-code removal in Follow-up 2 is verified by `coqc` building all downstream files unchanged. ## Refs - Phase 1 triage: #58 - Phase 2a (Lambda): #60 - Phase 2b (CNOCategory): #61 - Phase 2c (Filesystem): #62 - Phase 2d (Quantum): #63 - Phase 2e (Physics): #66 - Follow-ups source: `docs/proof-debt-triage.md` §"Follow-ups surfaced by triage" (1, 2, 3 of 5; 4 + 5 require real proof work, deferred) - Policy: [standards#203](hyperpolymath/standards#203) - CI enforcement: [standards#211](hyperpolymath/standards#211) ## Test plan - [x] All eight touched/new Coq files compile under `coqc -R common CNO ...` (verified locally) - [x] `check-trusted-base.sh` — 129 → 118 markers, undocumented count unchanged at 4 - [x] No code semantics changed; refactor only - [x] `.gitignore` covers Coq build artefacts - [x] Machine-readable ADR ledger updated (ADR-011, ADR-012) - [ ] CI green on this branch 🤖 Generated with [Claude Code](https://claude.com/claude-code) --------- Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 parent 5650dd0 commit 0b9b215

10 files changed

Lines changed: 213 additions & 179 deletions

File tree

‎.gitignore‎

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -82,5 +82,14 @@ htmlcov/
8282
ai-cli-crash-capture/
8383
proofs/lean4/.lake/
8484

85+
# Coq build outputs
86+
*.vo
87+
*.vok
88+
*.vos
89+
*.glob
90+
.*.aux
91+
.lia.cache
92+
.nia.cache
93+
8594
# Rust build outputs in subdirectories (e.g. fuzz/target/)
8695
**/target/

‎.machine_readable/META.scm‎

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,9 @@
1313
("ADR-007" "accepted" "Discharge eval_deterministic Axiom → Theorem via step_deterministic_strong helper (2026-05-20, PR #24); first post-T0 axiom audit win")
1414
("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)")
1515
("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)")
16-
("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")))
16+
("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")
17+
("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")
18+
("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)")))
1719

1820
(development-practices
1921
(code-style "Coq proof engineering")

‎docs/proof-debt-triage.md‎

Lines changed: 26 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -161,17 +161,33 @@ These are concrete sub-projects that fall out of the table. Each is
161161
its own PR-sized piece of work — none of them is in scope for this
162162
triage PR.
163163

164-
1. **De-duplicate physics constants.** `kB_positive` and
165-
`temperature_positive` are axiomatised three times (QuantumCNO,
166-
StatMech, LandauerDerivation). Move to a shared `Physics.Constants`
167-
module and import.
168-
2. **De-duplicate quantum laws.** `unitary_preserves_entropy` and
169-
`no_cloning` appear in both `QuantumMechanicsExact.v` and
170-
`QuantumCNO.v` with the same name. Pick one as canonical.
164+
1. **De-duplicate physics constants.** ✅ DONE 2026-05-27.
165+
`kB_positive` and `temperature_positive` previously axiomatised
166+
three times (QuantumCNO, StatMech, LandauerDerivation); now
167+
consolidated in `proofs/coq/common/PhysicsConstants.v` and imported
168+
via `Require Import CNO.PhysicsConstants`. Net: 129 → 125 markers
169+
(−4: removed 6 sites, added 2 canonical sites).
170+
2. **De-duplicate quantum laws.** ✅ DONE 2026-05-27.
171+
`unitary_preserves_entropy` and `no_cloning` previously appeared in
172+
both `QuantumMechanicsExact.v` and `QuantumCNO.v` with the same
173+
name. The `QuantumMechanicsExact.v` copies were dead code (no
174+
in-file usage; `no_cloning`'s statement was trivially `True`-equivalent)
175+
so they were removed. `QuantumCNO.v` is the canonical declaration
176+
for both. Net: −2 markers in `QuantumMechanicsExact.v`. The
177+
`X_gate_unitary` name-shadow noted in the per-axiom table refers to
178+
axiomatisations of two distinct gate definitions (indexed vs
179+
unindexed `QuantumGate`); not consolidated here.
171180
3. **De-duplicate decidability + probability + Shannon axioms.**
172-
`prob_nonneg`, `prob_normalized`, `state_eq_dec`/`state_dec`,
173-
`shannon_entropy_nonneg`, `shannon_entropy_point_zero` are
174-
duplicated between `StatMech.v` and `LandauerDerivation.v`.
181+
✅ DONE 2026-05-27. `prob_nonneg`, `prob_normalized`, `state_dec`
182+
(canonical name; subsumes `state_eq_dec`), `shannon_entropy`
183+
(parameter), `shannon_entropy_nonneg`, `shannon_entropy_point_zero`,
184+
and the `point_dist` definition are now in
185+
`proofs/coq/common/StatMechBasis.v` and imported by both
186+
`StatMech.v` and `LandauerDerivation.v` via
187+
`Require Import CNO.StatMechBasis`. Net: 125 → 118 markers (−7:
188+
removed 12 sites incl. the `shannon_entropy` parameter duplicate,
189+
added 5 canonical axiom sites; `state_eq_dec` aliased to canonical
190+
`state_dec`).
175191
4. **Constructively define `Cexp` in `Complex.v`.** `Complex.v` has
176192
zero axioms today; if it defines `Cexp` from a power series (or
177193
imports from a Coq reals/complex stdlib), the four `Cexp_*` axioms

‎proofs/coq/_CoqProject‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,7 @@
11
-R common CNO
22
-R malbolge Malbolge
33

4+
common/PhysicsConstants.v
45
common/CNO.v
6+
common/StatMechBasis.v
57
malbolge/MalbolgeCore.v

‎proofs/coq/common/PhysicsConstants.v‎

Lines changed: 39 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,39 @@
1+
(** * Physical Constants — Shared Across CNO Theory
2+
3+
Single source of truth for the [kB] (Boltzmann constant) and
4+
[temperature] parameters that show up in the quantum and statistical
5+
mechanics modules. Consolidates triplicated declarations from
6+
[QuantumCNO.v], [StatMech.v], and [LandauerDerivation.v] (Follow-up 1
7+
of [docs/proof-debt-triage.md]).
8+
9+
Author: Jonathan D. A. Jewell
10+
Project: Absolute Zero
11+
License: MPL-2.0
12+
*)
13+
14+
Require Import Coq.Reals.Reals.
15+
16+
Open Scope R_scope.
17+
18+
(** ** Boltzmann constant *)
19+
20+
(** Boltzmann constant [k_B] (J/K). In SI units:
21+
[kB ≈ 1.380649 × 10^{-23} J/K]. *)
22+
Parameter kB : R.
23+
24+
(* AXIOM: kB_positive; Boltzmann constant — physical constant.
25+
Consolidated from QuantumCNO.v:31, StatMech.v:25,
26+
LandauerDerivation.v:28 (Follow-up 1 of docs/proof-debt-triage.md).
27+
§(c) per docs/proof-debt.md. *)
28+
Axiom kB_positive : kB > 0.
29+
30+
(** ** Temperature *)
31+
32+
(** Temperature in Kelvin (must be positive). Room temperature ≈ 300 K. *)
33+
Parameter temperature : R.
34+
35+
(* AXIOM: temperature_positive; Temperature scalar — physical precondition.
36+
Consolidated from QuantumCNO.v:35, StatMech.v:30,
37+
LandauerDerivation.v:32 (Follow-up 1 of docs/proof-debt-triage.md).
38+
§(c) per docs/proof-debt.md. *)
39+
Axiom temperature_positive : temperature > 0.

‎proofs/coq/common/StatMechBasis.v‎

Lines changed: 75 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,75 @@
1+
(** * Statistical Mechanics Basis — Shared Probability + Entropy Axioms
2+
3+
Single source of truth for the Kolmogorov-style probability axioms,
4+
state-equality decision procedure, point distribution, Shannon
5+
entropy parameter, and the two core Shannon-entropy inequalities
6+
used by both [StatMech.v] and [LandauerDerivation.v].
7+
Consolidates duplicated declarations (Follow-up 3 of
8+
[docs/proof-debt-triage.md]).
9+
10+
Author: Jonathan D. A. Jewell
11+
Project: Absolute Zero
12+
License: MPL-2.0
13+
*)
14+
15+
Require Import Coq.Reals.Reals.
16+
Require Import Coq.Lists.List.
17+
Require Import CNO.CNO.
18+
Import ListNotations.
19+
20+
Open Scope R_scope.
21+
22+
(** ** Probability distributions over [ProgramState] *)
23+
24+
Definition StateDistribution : Type := ProgramState -> R.
25+
26+
(* AXIOM: prob_nonneg; Kolmogorov probability axiom (non-negativity).
27+
Consolidated from StatMech.v:39 and LandauerDerivation.v:40
28+
(Follow-up 3 of docs/proof-debt-triage.md).
29+
§(c) per docs/proof-debt.md. *)
30+
Axiom prob_nonneg :
31+
forall (P : StateDistribution) (s : ProgramState),
32+
P s >= 0.
33+
34+
(* Consolidated from StatMech.v:45 and LandauerDerivation.v:43
35+
(Follow-up 3). Picked the `map P` form from StatMech.v; the
36+
LandauerDerivation form (fold_right with explicit lambda) is
37+
equivalent. AXIOM: prob_normalized; Kolmogorov axiom (Σp = 1).
38+
§(c) per docs/proof-debt.md. *)
39+
Axiom prob_normalized :
40+
forall (P : StateDistribution),
41+
exists (states : list ProgramState),
42+
fold_right Rplus 0 (map P states) = 1.
43+
44+
(** ** Decidable equality on [ProgramState] *)
45+
46+
(* Consolidated from StatMech.v:51 (`state_dec`) and
47+
LandauerDerivation.v:48 (`state_eq_dec`); canonical name picked:
48+
`state_dec` (Follow-up 3). AXIOM: state_dec; decidable equality
49+
over opaque `ProgramState`; PROPERTY-TEST (§(b)) — treated as §(c)
50+
until a property-test budget is attached. *)
51+
Axiom state_dec :
52+
forall s1 s2 : ProgramState, {s1 = s2} + {s1 <> s2}.
53+
54+
(** Point distribution (Dirac delta) over [ProgramState]. *)
55+
Definition point_dist (s0 : ProgramState) : StateDistribution :=
56+
fun s => if state_dec s s0 then 1 else 0.
57+
58+
(** ** Shannon entropy *)
59+
60+
(** Shannon entropy: [H(P) = -Σ p(s) log₂ p(s)], measured in bits. *)
61+
Parameter shannon_entropy : StateDistribution -> R.
62+
63+
(* AXIOM: shannon_entropy_nonneg; Shannon entropy core inequality.
64+
Consolidated from StatMech.v:67 and LandauerDerivation.v:63
65+
(Follow-up 3 of docs/proof-debt-triage.md).
66+
§(c) per docs/proof-debt.md. *)
67+
Axiom shannon_entropy_nonneg :
68+
forall P : StateDistribution, shannon_entropy P >= 0.
69+
70+
(* AXIOM: shannon_entropy_point_zero; H(δ_x) = 0. Consolidated from
71+
StatMech.v:72 and LandauerDerivation.v:67 (Follow-up 3 of
72+
docs/proof-debt-triage.md).
73+
§(c) per docs/proof-debt.md. *)
74+
Axiom shannon_entropy_point_zero :
75+
forall s : ProgramState, shannon_entropy (point_dist s) = 0.

‎proofs/coq/physics/LandauerDerivation.v‎

Lines changed: 20 additions & 63 deletions
Original file line numberDiff line numberDiff line change
@@ -16,79 +16,36 @@ Require Import Coq.micromega.Psatz.
1616
Require Import Coq.Lists.List.
1717
Require Import Lia.
1818
Require Import CNO.CNO.
19+
(* Shared physics constants — kB, temperature, kB_positive,
20+
temperature_positive. See proofs/coq/common/PhysicsConstants.v
21+
(consolidated by Follow-up 1 of docs/proof-debt-triage.md). *)
22+
Require Import CNO.PhysicsConstants.
23+
(* Shared statmech basis — StateDistribution, prob_nonneg, prob_normalized,
24+
state_dec, point_dist, shannon_entropy, shannon_entropy_nonneg,
25+
shannon_entropy_point_zero. See proofs/coq/common/StatMechBasis.v
26+
(consolidated by Follow-up 3 of docs/proof-debt-triage.md). *)
27+
Require Import CNO.StatMechBasis.
1928
Import ListNotations.
2029

2130
Open Scope R_scope.
2231

23-
(** ** Physical Constants (Measured Values, Not Derived) *)
32+
(** ** Physical Constants (Measured Values, Not Derived)
2433
25-
(** Boltzmann constant: k_B = 1.380649 × 10^-23 J/K *)
26-
(** This is a measured physical constant, grounded in experiment *)
27-
Parameter kB : R.
28-
(* AXIOM: kB_positive; Boltzmann constant — physical constant. Duplicate of
29-
StatMech.v:25 + QuantumCNO.v:31 (see follow-up 1 in docs/proof-debt-triage.md).
30-
§(c) per docs/proof-debt.md (Phase 2e triage). *)
31-
Axiom kB_positive : kB > 0.
32-
33-
(** Temperature in Kelvin (must be positive) *)
34-
Parameter temperature : R.
35-
(* AXIOM: temperature_positive; Temperature scalar — physical precondition.
36-
Duplicate of StatMech.v:30 + QuantumCNO.v:35 (see follow-up 1).
37-
§(c) per docs/proof-debt.md (Phase 2e triage). *)
38-
Axiom temperature_positive : temperature > 0.
39-
40-
(** ** Foundation: Probability Theory *)
34+
Boltzmann constant [k_B = 1.380649 × 10^{-23} J/K] and [temperature]
35+
in Kelvin (must be positive) are imported from [CNO.PhysicsConstants]
36+
(consolidated by Follow-up 1). These are measured physical constants,
37+
grounded in experiment. *)
4138

42-
(** A probability distribution over program states *)
43-
Definition StateDistribution : Type := ProgramState -> R.
44-
45-
(** Probability axioms (Kolmogorov) *)
46-
(* AXIOM: prob_nonneg; Kolmogorov probability axiom (non-negativity).
47-
Duplicate of StatMech.v:39 (see follow-up 3 in docs/proof-debt-triage.md).
48-
§(c) per docs/proof-debt.md (Phase 2e triage). *)
49-
Axiom prob_nonneg :
50-
forall (P : StateDistribution) (s : ProgramState), P s >= 0.
51-
52-
(* AXIOM: prob_normalized; Kolmogorov probability axiom (Σp = 1).
53-
Duplicate of StatMech.v:45 (see follow-up 3).
54-
§(c) per docs/proof-debt.md (Phase 2e triage). *)
55-
Axiom prob_normalized :
56-
forall (P : StateDistribution),
57-
exists (states : list ProgramState),
58-
fold_right (fun s acc => acc + P s) 0 states = 1.
39+
(** ** Foundation: Probability + Shannon Entropy Basis
5940
60-
(* AXIOM: state_eq_dec; Decidable equality over opaque `ProgramState`;
61-
needs oracle or §(b) refutation budget. Duplicate of StatMech.v:51
62-
`state_dec` (see follow-up 3). PROPERTY-TEST (§(b)) — treated as §(c)
63-
until a property-test budget is attached. *)
64-
Axiom state_eq_dec : forall s1 s2 : ProgramState, {s1 = s2} + {s1 <> s2}.
65-
66-
(** Point distribution (Dirac delta) *)
67-
Definition point_dist (s0 : ProgramState) : StateDistribution :=
68-
fun s => if state_eq_dec s s0 then 1 else 0.
69-
70-
(** ** Shannon Entropy: Information-Theoretic Foundation *)
71-
72-
(** Shannon entropy: H(P) = -Σ p_i log_2(p_i)
73-
Measured in bits *)
74-
Parameter shannon_entropy : StateDistribution -> R.
41+
[StateDistribution], [prob_nonneg], [prob_normalized], [state_dec],
42+
[point_dist], [shannon_entropy], [shannon_entropy_nonneg], and
43+
[shannon_entropy_point_zero] are imported from [CNO.StatMechBasis]
44+
(consolidated by Follow-up 3 of [docs/proof-debt-triage.md]). This
45+
file adds [log2] and the uniform-max / additive axioms below. *)
7546

7647
Definition log2 (x : R) : R := ln x / ln 2.
7748

78-
(** Shannon entropy axioms (from information theory) *)
79-
(* AXIOM: shannon_entropy_nonneg; Shannon entropy core inequality.
80-
Duplicate of StatMech.v:67 (see follow-up 3).
81-
§(c) per docs/proof-debt.md (Phase 2e triage). *)
82-
Axiom shannon_entropy_nonneg :
83-
forall P : StateDistribution, shannon_entropy P >= 0.
84-
85-
(** Point distributions have zero entropy (no uncertainty) *)
86-
(* AXIOM: shannon_entropy_point_zero; H(δ_x) = 0. Duplicate of
87-
StatMech.v:72 (see follow-up 3).
88-
§(c) per docs/proof-debt.md (Phase 2e triage). *)
89-
Axiom shannon_entropy_point_zero :
90-
forall s : ProgramState, shannon_entropy (point_dist s) = 0.
91-
9249
(** Entropy is maximized for uniform distribution *)
9350
(* AXIOM: shannon_entropy_uniform_max; Variant of Gibbs inequality for
9451
uniform distributions. §(c) per docs/proof-debt.md (Phase 2e triage). *)

‎proofs/coq/physics/StatMech.v‎

Lines changed: 18 additions & 73 deletions
Original file line numberDiff line numberDiff line change
@@ -14,86 +14,31 @@ Require Import Coq.Logic.FunctionalExtensionality.
1414
Require Import Coq.Lists.List.
1515
Require Import Coq.micromega.Psatz.
1616
Require Import CNO.CNO.
17+
(* Shared physics constants — kB, temperature, kB_positive,
18+
temperature_positive. See proofs/coq/common/PhysicsConstants.v
19+
(consolidated by Follow-up 1 of docs/proof-debt-triage.md). *)
20+
Require Import CNO.PhysicsConstants.
21+
(* Shared statmech basis — StateDistribution, prob_nonneg, prob_normalized,
22+
state_dec, point_dist, shannon_entropy, shannon_entropy_nonneg,
23+
shannon_entropy_point_zero. See proofs/coq/common/StatMechBasis.v
24+
(consolidated by Follow-up 3 of docs/proof-debt-triage.md). *)
25+
Require Import CNO.StatMechBasis.
1726
Import ListNotations.
1827

1928
Open Scope R_scope.
2029

21-
(** ** Physical Constants *)
30+
(** ** Physical Constants
2231
23-
(** Boltzmann constant (J/K) *)
24-
Parameter kB : R.
25-
(* AXIOM: kB_positive; Boltzmann constant — physical constant. Duplicate of
26-
LandauerDerivation.v:28 + QuantumCNO.v:31 (see follow-up 1).
27-
§(c) per docs/proof-debt.md (Phase 2e triage). *)
28-
Axiom kB_positive : kB > 0.
29-
(** In SI units: kB ≈ 1.380649×10⁻²³ J/K *)
30-
31-
(** Temperature (Kelvin) *)
32-
Parameter temperature : R.
33-
(* AXIOM: temperature_positive; Temperature scalar — physical precondition.
34-
Duplicate of LandauerDerivation.v:32 + QuantumCNO.v:35 (see follow-up 1).
35-
§(c) per docs/proof-debt.md (Phase 2e triage). *)
36-
Axiom temperature_positive : temperature > 0.
37-
(** Room temperature ≈ 300 K *)
38-
39-
(** ** Probability Distributions *)
40-
41-
(** A probability distribution over program states *)
42-
Definition StateDistribution : Type := ProgramState -> R.
43-
44-
(** Axiom: Probabilities are non-negative *)
45-
(* AXIOM: prob_nonneg; Kolmogorov probability axiom (non-negativity).
46-
Duplicate of LandauerDerivation.v:40 (see follow-up 3).
47-
§(c) per docs/proof-debt.md (Phase 2e triage). *)
48-
Axiom prob_nonneg :
49-
forall (P : StateDistribution) (s : ProgramState),
50-
P s >= 0.
51-
52-
(** Axiom: Probabilities sum to 1 (normalization) *)
53-
(** Note: Proper formalization requires measure theory *)
54-
(* AXIOM: prob_normalized; Kolmogorov probability axiom (Σp = 1).
55-
Duplicate of LandauerDerivation.v:43 (see follow-up 3).
56-
§(c) per docs/proof-debt.md (Phase 2e triage). *)
57-
Axiom prob_normalized :
58-
forall (P : StateDistribution),
59-
exists (states : list ProgramState),
60-
fold_right Rplus 0 (map P states) = 1.
61-
62-
(** State decidability *)
63-
(* AXIOM: state_dec; Decidable equality over opaque `ProgramState`; needs
64-
oracle or §(b) refutation budget. Duplicate of LandauerDerivation.v:48
65-
`state_eq_dec` (see follow-up 3). PROPERTY-TEST (§(b)) — treated as
66-
§(c) until a property-test budget is attached. *)
67-
Axiom state_dec :
68-
forall s1 s2 : ProgramState, {s1 = s2} + {s1 <> s2}.
32+
[kB], [temperature], [kB_positive], and [temperature_positive] are
33+
imported from [CNO.PhysicsConstants] (consolidated by Follow-up 1).
34+
In SI units: [kB ≈ 1.380649×10⁻²³ J/K]; room temperature ≈ 300 K. *)
6935

70-
(** Point distribution (all probability on one state) *)
71-
Definition point_dist (s0 : ProgramState) : StateDistribution :=
72-
fun s => if state_dec s s0 then 1 else 0.
36+
(** ** Probability Distributions, Entropy
7337
74-
(** ** Information-Theoretic Entropy *)
75-
76-
(** Shannon entropy: H(P) = -Σ p(s) log₂ p(s)
77-
78-
Measured in bits (using log base 2)
79-
*)
80-
Parameter shannon_entropy : StateDistribution -> R.
81-
82-
(** Axiom: Shannon entropy is non-negative *)
83-
(* AXIOM: shannon_entropy_nonneg; Shannon entropy core inequality. Duplicate
84-
of LandauerDerivation.v:63 (see follow-up 3).
85-
§(c) per docs/proof-debt.md (Phase 2e triage). *)
86-
Axiom shannon_entropy_nonneg :
87-
forall P : StateDistribution,
88-
shannon_entropy P >= 0.
89-
90-
(** Axiom: Point distributions have zero entropy *)
91-
(* AXIOM: shannon_entropy_point_zero; H(δ_x) = 0. Duplicate of
92-
LandauerDerivation.v:67 (see follow-up 3).
93-
§(c) per docs/proof-debt.md (Phase 2e triage). *)
94-
Axiom shannon_entropy_point_zero :
95-
forall s : ProgramState,
96-
shannon_entropy (point_dist s) = 0.
38+
[StateDistribution], [prob_nonneg], [prob_normalized], [state_dec],
39+
[point_dist], [shannon_entropy], [shannon_entropy_nonneg], and
40+
[shannon_entropy_point_zero] are imported from [CNO.StatMechBasis]
41+
(consolidated by Follow-up 3 of [docs/proof-debt-triage.md]). *)
9742

9843
(** Axiom: Entropy is maximized for uniform distribution *)
9944
(* AXIOM: shannon_entropy_maximum; H ≤ log n (Gibbs inequality).

0 commit comments

Comments
 (0)