Skip to content

Commit e17256b

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
authored
docs: Phase 1 per-axiom triage of 72 Coq Axioms (#58)
## Summary Adds `docs/proof-debt-triage.md` — Phase 1 of the proof-debt triage process described in [the seed `docs/proof-debt.md`](./docs/proof-debt.md) (PR #52). Classifies every Coq `Axiom` in the repo against the [standards#203 trusted-base reduction policy](hyperpolymath/standards#203): - **52 AXIOM** (§c TRUSTED-BASE) — physics constants, quantum gate primitives, POSIX semantics, Kolmogorov + Shannon axioms, complex exponential algebra, fundamental physical laws. - **17 DISCHARGE** (§a) — derivable theorems mistakenly stated as `Axiom`. Lowest-hanging: `cno_zero_energy_dissipation_derived` (name says it), `fidelity_bound`, `unitary_inverse_property`, the two `*_not_identity` existence axioms. - **3 PROPERTY-TEST** (§b) — decidability claims over opaque types (`fs_eq_dec`, `state_dec`, `state_eq_dec`). ## Scope Coq Axioms only (72 of 72 classified). Out of scope but tracked in the doc: - 52 Lean 4 `axiom` declarations in `proofs/lean4/*.lean`. - 7 Idris2 `postulate`s in `src/abi/Layout.idr` (tracked by #27). ## Follow-ups surfaced by triage 1. **De-duplicate physics constants** — `kB_positive` / `temperature_positive` declared 3x across QuantumCNO, StatMech, LandauerDerivation. 2. **De-duplicate quantum laws** — `unitary_preserves_entropy` and `no_cloning` declared twice with the same name. 3. **De-duplicate probability + decidability + Shannon axioms** between `StatMech.v` and `LandauerDerivation.v`. 4. **Define `Cexp` constructively in `Complex.v`** — collapses 4 axioms in QuantumCNO to DISCHARGE. 5. **The 17 DISCHARGE cluster** is the backlog for the next batch of proof PRs. ## Method Inventory generated by `grep -nE '^[[:space:]]*Axiom[[:space:]]' proofs/coq/**/*.v` and each axiom classified by reading its declared type and the nearest doc-comment. Counts triple-checked: `3+29+1+13+10+14+2 = 72`. ## Test plan - [ ] Visual review of `docs/proof-debt-triage.md` table - [ ] `bash /path/to/standards/scripts/check-trusted-base.sh .` still reports the same marker count (the triage doc doesn't change any `Axiom` declarations) 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 parent ab35c07 commit e17256b

1 file changed

Lines changed: 200 additions & 0 deletions

File tree

‎docs/proof-debt-triage.md‎

Lines changed: 200 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,200 @@
1+
<!--
2+
SPDX-License-Identifier: MPL-2.0
3+
SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath)
4+
-->
5+
6+
# Proof Debt — Per-Marker Triage (Coq Axioms)
7+
8+
Companion to [`docs/proof-debt.md`](./proof-debt.md) (the standards#203
9+
seed). This file classifies **every Coq `Axiom` declaration** in this
10+
repo into the three dispositions from the standards#203
11+
trusted-base-reduction policy:
12+
13+
- **AXIOM** — legitimate model-layer assumption (TRUSTED-BASE / §(c)).
14+
The marker encodes a physical postulate, an opaque-primitive
15+
specification, or a metatheoretic assumption that cannot be
16+
discharged within the working logic.
17+
- **DISCHARGE** — a real provable proposition that is currently stated
18+
as `Axiom` for expedience. Targeted for a future proof PR (§(a)).
19+
- **PROPERTY-TEST** — empirical claim better validated by a refutation
20+
budget under §(b); typically decidability over opaque types.
21+
22+
## Scope
23+
24+
This pass triages **only the 72 Coq Axioms**. Out of scope here, but
25+
still markers in `check-trusted-base.sh`:
26+
27+
- 52 Lean 4 `axiom` declarations (FilesystemCNO.lean, LambdaCNO.lean,
28+
QuantumCNO.lean, StatMech.lean).
29+
- 7 Idris2 `postulate`s in `src/abi/Layout.idr` (tracked by [#27]).
30+
- 0 Coq `Admitted.` or `admit.`
31+
- 0 Lean `sorry`, 0 Agda postulates, 0 Rust `unsafePerformIO` /
32+
`unsafeCoerce`.
33+
34+
`docs/proof-debt.md` records **129** total markers (seeded 2026-05-26).
35+
`check-trusted-base.sh` against `origin/main` today reports **124** —
36+
five fewer, reflecting in-flight closures since the seed.
37+
38+
[#27]: https://github.com/hyperpolymath/absolute-zero/issues/27
39+
40+
## Summary
41+
42+
| Disposition | Count | % |
43+
|-------------|------:|-----:|
44+
| AXIOM | 52 | 72% |
45+
| DISCHARGE | 17 | 24% |
46+
| PROPERTY-TEST | 3 | 4% |
47+
| **Total** | **72** | 100% |
48+
49+
## Per-axiom table
50+
51+
### `proofs/coq/quantum/QuantumMechanicsExact.v` (3)
52+
53+
| Line | Identifier | Disposition | Justification |
54+
|-----:|------------|-------------|---------------|
55+
| 249 | `X_gate_unitary` | AXIOM | Pauli-X is a primitive quantum gate; unitarity is its defining property in the model. |
56+
| 316 | `unitary_preserves_entropy` | AXIOM | Quantum statmech postulate (von Neumann entropy invariant under unitary). |
57+
| 393 | `no_cloning` | AXIOM | Fundamental quantum theorem; standardly taken as physical postulate in this style of axiomatisation. |
58+
59+
### `proofs/coq/quantum/QuantumCNO.v` (29)
60+
61+
| Line | Identifier | Disposition | Justification |
62+
|-----:|------------|-------------|---------------|
63+
| 31 | `kB_positive` | AXIOM | Boltzmann constant — physical constant. |
64+
| 35 | `temperature_positive` | AXIOM | Temperature scalar — physical precondition. |
65+
| 45 | `dim_positive` | AXIOM | Hilbert-space dimensionality precondition. |
66+
| 68 | `inner_product_conj_sym` | AXIOM | Inner product space axiom (conjugate symmetry). |
67+
| 73 | `inner_product_linear` | AXIOM | Inner product space axiom (linearity). |
68+
| 80 | `inner_product_pos_def` | AXIOM | Inner product space axiom (positive definiteness). |
69+
| 113 | `X_gate_unitary` | AXIOM | Quantum gate primitive (duplicate of QuantumMechanicsExact:249 — see followup). |
70+
| 117 | `Y_gate_unitary` | AXIOM | Quantum gate primitive. |
71+
| 121 | `Z_gate_unitary` | AXIOM | Quantum gate primitive. |
72+
| 125 | `H_gate_unitary` | AXIOM | Quantum gate primitive. |
73+
| 129 | `CNOT_gate_unitary` | AXIOM | Quantum gate primitive. |
74+
| 150 | `Cexp_zero` | AXIOM | Complex exponential algebra (would move to DISCHARGE if `Complex.v` defines `Cexp` constructively — currently the file has 0 axioms but no `Cexp`). |
75+
| 153 | `Cexp_neg` | AXIOM | Complex exponential algebra (see L150 note). |
76+
| 156 | `Cexp_add` | AXIOM | Complex exponential algebra (see L150 note). |
77+
| 163 | `Cconj_Cexp` | AXIOM | Complex exponential algebra (see L150 note). |
78+
| 258 | `global_phase_unitary` | DISCHARGE | Derivable from gate algebra: `(e^{iθ} U)` is unitary iff `U` is. |
79+
| 283 | `X_gate_not_identity` | DISCHARGE | Existence proof; exhibit `|0⟩` as witness once a concrete basis state is in the model. |
80+
| 296 | `H_gate_not_identity` | DISCHARGE | Existence proof; exhibit `|0⟩` as witness. |
81+
| 361 | `von_neumann_nonneg` | AXIOM | Quantum statmech — von Neumann entropy non-negativity. |
82+
| 366 | `von_neumann_pure_zero` | AXIOM | `S(|ψ⟩⟨ψ|) = 0` for pure states. |
83+
| 372 | `unitary_preserves_entropy` | AXIOM | Duplicate of QuantumMechanicsExact:316 (see followup). |
84+
| 391 | `no_cloning` | AXIOM | Duplicate of QuantumMechanicsExact:393 (see followup). |
85+
| 421 | `measure_identity_commutes` | AXIOM | Measurement postulate. |
86+
| 487 | `unitary_inverse_property` | DISCHARGE | Follows from `is_unitary` definition (`U†U = I`). |
87+
| 538 | `quantum_landauer_bound` | AXIOM | Physical postulate (quantum Landauer). |
88+
| 545 | `unitary_zero_entropy_change` | DISCHARGE | Derivable from `unitary_preserves_entropy` + entropy definition. |
89+
| 551 | `reversible_quantum_zero_dissipation` | DISCHARGE | Derivable from `quantum_landauer_bound` + unitarity. |
90+
| 584 | `fidelity_bound` | DISCHARGE | Provable from `inner_product_pos_def` + Cauchy-Schwarz. |
91+
| 587 | `approximate_cno` | AXIOM | Definitional / structural — encodes a relation, not a derivable fact. |
92+
93+
### `proofs/coq/category/CNOCategory.v` (1)
94+
95+
| Line | Identifier | Disposition | Justification |
96+
|-----:|------------|-------------|---------------|
97+
| 323 | `hom_functor` | DISCHARGE | Standard categorical construction (Hom(C,A,-)); should be a `Definition` building the functor record, not an `Axiom`. |
98+
99+
### `proofs/coq/filesystem/FilesystemCNO.v` (13)
100+
101+
| Line | Identifier | Disposition | Justification |
102+
|-----:|------------|-------------|---------------|
103+
| 96 | `fs_eq_dec` | PROPERTY-TEST | Decidable equality over a list of entries containing opaque `FileContent`; needs an oracle, or a §(b) budget over a concrete content type. |
104+
| 104 | `mkdir_rmdir_inverse` | AXIOM | POSIX-semantics specification (model-layer). |
105+
| 114 | `create_unlink_inverse` | AXIOM | POSIX-semantics specification. |
106+
| 124 | `read_write_identity` | AXIOM | POSIX-semantics specification. |
107+
| 130 | `chmod_identity` | AXIOM | POSIX-semantics specification. |
108+
| 136 | `chown_identity` | AXIOM | POSIX-semantics specification. |
109+
| 142 | `rename_identity` | AXIOM | POSIX-semantics specification. |
110+
| 147 | `rename_inverse` | AXIOM | POSIX-semantics specification. |
111+
| 300 | `mkdir_not_identity` | DISCHARGE | Existence proof; exhibit one concrete `fs` lacking the path. |
112+
| 316 | `write_different_not_identity` | DISCHARGE | Existence proof; exhibit one concrete content mismatch. |
113+
| 397 | `transaction_cno` | DISCHARGE | Composite theorem; derivable from primitive `_inverse` axioms once a `transaction` definition is in place. |
114+
| 421 | `mkdir_idempotent` | DISCHARGE | Follows from the `mkdir_rmdir_inverse` family + a stronger semantics for repeat `mkdir`. |
115+
| 453 | `snapshot_restore_identity` | DISCHARGE | Composite theorem; derivable from primitive `_identity` / `_inverse` axioms. |
116+
117+
### `proofs/coq/physics/StatMech.v` (10)
118+
119+
| Line | Identifier | Disposition | Justification |
120+
|-----:|------------|-------------|---------------|
121+
| 25 | `kB_positive` | AXIOM | Physical constant (duplicate — see consolidation followup). |
122+
| 30 | `temperature_positive` | AXIOM | Physical precondition (duplicate). |
123+
| 39 | `prob_nonneg` | AXIOM | Kolmogorov probability axiom. |
124+
| 45 | `prob_normalized` | AXIOM | Kolmogorov probability axiom (Σp = 1). |
125+
| 51 | `state_dec` | PROPERTY-TEST | Decidable equality over opaque `ProgramState`; needs oracle or §(b) budget. |
126+
| 67 | `shannon_entropy_nonneg` | AXIOM | Shannon entropy core inequality. |
127+
| 72 | `shannon_entropy_point_zero` | AXIOM | `H(δ_x) = 0`. |
128+
| 77 | `shannon_entropy_maximum` | AXIOM | `H ≤ log n` (Gibbs inequality). |
129+
| 132 | `landauer_principle` | AXIOM | Physical postulate (Landauer's principle). |
130+
| 229 | `reversible_zero_dissipation` | DISCHARGE | Derivable from `landauer_principle` + reversibility hypothesis. |
131+
132+
### `proofs/coq/physics/LandauerDerivation.v` (14)
133+
134+
| Line | Identifier | Disposition | Justification |
135+
|-----:|------------|-------------|---------------|
136+
| 28 | `kB_positive` | AXIOM | Physical constant (duplicate of StatMech:25). |
137+
| 32 | `temperature_positive` | AXIOM | Physical precondition (duplicate). |
138+
| 40 | `prob_nonneg` | AXIOM | Kolmogorov axiom (duplicate of StatMech:39). |
139+
| 43 | `prob_normalized` | AXIOM | Kolmogorov axiom (duplicate of StatMech:45). |
140+
| 48 | `state_eq_dec` | PROPERTY-TEST | Decidable equality over opaque `ProgramState` (duplicate of StatMech:51). |
141+
| 63 | `shannon_entropy_nonneg` | AXIOM | Duplicate of StatMech:67. |
142+
| 67 | `shannon_entropy_point_zero` | AXIOM | Duplicate of StatMech:72. |
143+
| 71 | `shannon_entropy_uniform_max` | AXIOM | Variant of Gibbs inequality for uniform distributions. |
144+
| 81 | `shannon_entropy_additive` | DISCHARGE | Chain rule of entropy; provable from the definition of `H(X,Y)` given independence hypothesis. |
145+
| 126 | `second_law` | AXIOM | Physical postulate (second law of thermodynamics). |
146+
| 181 | `entropy_change_erasure` | AXIOM | Landauer–Bennett result. |
147+
| 197 | `isothermal_work_bound` | AXIOM | Thermodynamic bound (Helmholtz free energy). |
148+
| 277 | `cno_preserves_shannon_entropy` | DISCHARGE | Should follow from the CNO definition (`state in = state out`) + functional Shannon entropy. |
149+
| 326 | `cno_zero_energy_dissipation_derived` | DISCHARGE | Name literally says `_derived`; the file appears to admit this rather than discharge it. |
150+
151+
### `proofs/coq/lambda/LambdaCNO.v` (2)
152+
153+
| Line | Identifier | Disposition | Justification |
154+
|-----:|------------|-------------|---------------|
155+
| 356 | `y_not_cno` | AXIOM | Non-termination claim about the Y combinator; the file's leading comment justifies axiomatisation ("requires step-indexed semantics or coinduction") and explicitly declares it safely axiomatised. |
156+
| 376 | `eta_equivalence` | AXIOM | η-equivalence is not derivable under β-only reduction; needs an extra reduction rule or extensional equality. Metatheoretic assumption. |
157+
158+
## Follow-ups surfaced by triage
159+
160+
These are concrete sub-projects that fall out of the table. Each is
161+
its own PR-sized piece of work — none of them is in scope for this
162+
triage PR.
163+
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.
171+
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`.
175+
4. **Constructively define `Cexp` in `Complex.v`.** `Complex.v` has
176+
zero axioms today; if it defines `Cexp` from a power series (or
177+
imports from a Coq reals/complex stdlib), the four `Cexp_*` axioms
178+
in QuantumCNO collapse to DISCHARGE.
179+
5. **17 DISCHARGE cluster.** The DISCHARGE column is the work backlog
180+
for subsequent proof PRs. The lowest-hanging are the four `_derived`
181+
/ `_not_identity` / `unitary_*` axioms in QuantumCNO that fall out
182+
directly from the existing definitions.
183+
184+
## Methodology
185+
186+
1. Inventory generated by:
187+
```bash
188+
grep -nE '^[[:space:]]*Axiom[[:space:]]' proofs/coq/**/*.v
189+
```
190+
2. Each axiom was classified by reading its declared type and the
191+
nearest doc-comment / section header.
192+
3. Disposition follows the standards#203 schema; the user-facing
193+
vocabulary (DISCHARGE / PROPERTY-TEST / AXIOM) maps 1:1 to
194+
§(a) / §(b) / §(c) in `docs/proof-debt.md`.
195+
4. Counts triple-checked against the per-file `Axiom` tally
196+
(`3+29+1+13+10+14+2 = 72`).
197+
198+
---
199+
200+
🤖 Phase 1 triage by Claude Code, 2026-05-27.

0 commit comments

Comments
 (0)