docs+annotate: Quantum cluster — 36 inline AXIOM: + 10 §(d) DEBT entries (Phase 2d)#63
Merged
Merged
Conversation
…ies (Phase 2d) Annotates the Quantum cluster per standards#203 trusted-base policy: - 22 inline `(* AXIOM: ... *)` in `proofs/coq/quantum/QuantumCNO.v` - 3 inline `(* AXIOM: ... *)` in `proofs/coq/quantum/QuantumMechanicsExact.v` - 11 inline `-- AXIOM:` in `proofs/lean4/QuantumCNO.lean` - New "Phase 2d triage — Lean Quantum cluster" section in docs/proof-debt.md classifying all 14 Lean axioms (11 §(c) + 3 §(d)) - 10 new §(d) DEBT entries in docs/proof-debt.md (7 Coq DISCHARGE-class + 3 Lean DEBT mirroring Coq sites) `check-trusted-base.sh`: 88/129 → 42/129 undocumented (46-drop, matching 22 + 3 + 11 + 7 + 3 = 46 newly documented markers). Quantum cluster is 0 errors. Remaining 42 = Physics cluster (Phase 2e) + 4 Idris2 BoJ markers in `src/abi/Proofs/`. Refs: docs/proof-debt-triage.md (Phase 1 #58); Phase 2a (#60), Phase 2b (#61), Phase 2c (#62). 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
3 tasks
hyperpolymath
added a commit
that referenced
this pull request
May 27, 2026
…es (Phase 2e) (#66) ## Summary Phase 2e of the standards#203 trusted-base annotation rollout. Annotates the **Physics cluster** (Coq `LandauerDerivation.v` + `StatMech.v` + Lean `StatMech.lean`) so its 42 escape hatches are policy-compliant under \`scripts/check-trusted-base.sh\`. ### Changes - **11 inline \`(* AXIOM: ... *)\`** in \`proofs/coq/physics/LandauerDerivation.v\` (kB, temperature, Kolmogorov probability axioms, Shannon entropy postulates, 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 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)). - **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 now fully classified per standards#203. ### Verification \`bash ~/developer/repos/standards/scripts/check-trusted-base.sh .\` results: | | Undocumented | |---|---:| | Before this PR | 42/129 | | After this PR | 4/129 | | Drop | **−38** (11 Coq Landauer + 9 Coq StatMech + 14 Lean + 4 Coq §(d) DISCHARGE-mention) | Physics cluster errors → 0. Remaining 4 = Idris2 \`src/abi/Proofs/DivMod.idr\` (out of Phase 2 scope; BoJ vendored proofs). ### Note on Lean \`reversible_zero_dissipation\` The Coq counterpart (\`StatMech.v:229\`) is triaged DISCHARGE; the Lean side keeps it as §(c) AXIOM because no Lean-side derivation chain is in place yet. When the Coq DISCHARGE lands, the Lean side can be reclassified. ### Refs - Phase 1 triage: #58 - Phase 2a (Lambda): #60 - Phase 2b (CNOCategory): #61 - Phase 2c (Filesystem): #62 - Phase 2d (Quantum): #63 - Policy: [standards#203](hyperpolymath/standards#203) - CI enforcement: [standards#211](hyperpolymath/standards#211) ## Test plan - [x] \`check-trusted-base.sh\` Physics cluster errors → 0 (verified locally; cumulative 42 → 4) - [x] No code semantics changed; comments + docs only - [ ] 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>
6 tasks
hyperpolymath
added a commit
that referenced
this pull request
May 27, 2026
… + statmech basis
Builds on Follow-up 1 (PhysicsConstants.v) with the remaining two
mechanical dedupes from docs/proof-debt-triage.md.
Follow-up 2 — dead duplicate axioms removed from QuantumMechanicsExact.v:
- `unitary_preserves_entropy` (line 323) — was dead code; canonical lives
in QuantumCNO.v (which uses an unindexed `QuantumGate`, the only form
with downstream callers).
- `no_cloning` (line 404) — was dead code AND its statement `forall ψ,
False` was trivially `True`-equivalent. Canonical in QuantumCNO.v.
Follow-up 3 — statmech basis consolidated:
- New file `proofs/coq/common/StatMechBasis.v` declares once:
`StateDistribution`, `prob_nonneg`, `prob_normalized`, `state_dec`,
`point_dist`, `shannon_entropy` (parameter), `shannon_entropy_nonneg`,
`shannon_entropy_point_zero`.
- `StatMech.v` and `LandauerDerivation.v` import via
`Require Import CNO.StatMechBasis` and drop their local copies.
- `state_eq_dec` aliased into canonical `state_dec` (LandauerDerivation
only used the local name internally; no external callers).
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 output.
- `_CoqProject`: adds `common/StatMechBasis.v` to the build manifest
(alongside PhysicsConstants.v from Follow-up 1).
- `.machine_readable/META.scm`: ADR-011 (Phase 2a–2e Lean triage) and
ADR-012 (Follow-ups 1–3 consolidation) recorded.
- `docs/proof-debt-triage.md`: Follow-ups 2 + 3 marked DONE.
Verification:
- `coqc -R common CNO common/{PhysicsConstants,Complex,CNO,StatMechBasis}.v`
— OK
- `coqc -R common CNO physics/{StatMech,LandauerDerivation}.v` — OK
- `coqc -R common CNO quantum/{QuantumCNO,QuantumMechanicsExact}.v` — OK
- `check-trusted-base.sh` — 4/118 undocumented (remaining 4 are Idris2
`src/abi/Proofs/DivMod.idr`; out of Phase 2 scope). Net change since
Phase 2e closeout (#66): 129 → 118 markers, −11.
Refs: docs/proof-debt-triage.md (Phase 1 #58); Phase 2a (#60),
Phase 2b (#61), Phase 2c (#62), Phase 2d (#63), Phase 2e (#66).
🤖 Generated with [Claude Code](https://claude.com/claude-code)
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
hyperpolymath
added a commit
that referenced
this pull request
May 27, 2026
#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>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Phase 2d of the standards#203 trusted-base annotation rollout. Annotates the Quantum cluster (Coq
QuantumCNO.v+QuantumMechanicsExact.v+ LeanQuantumCNO.lean) so its 46 escape hatches are policy-compliant underscripts/check-trusted-base.sh.Changes
(* AXIOM: ... *)inproofs/coq/quantum/QuantumCNO.v(§(c) — Boltzmann constant, temperature, dim, inner-product axioms, Pauli/H/CNOT gate primitives, Cexp algebra, von Neumann entropy postulates, no-cloning, Landauer bound, measurement postulate, approximate-CNO).(* AXIOM: ... *)inproofs/coq/quantum/QuantumMechanicsExact.v(X-gate unitarity, unitary-preserves-entropy, no-cloning).-- AXIOM:inproofs/lean4/QuantumCNO.lean(mirrors Coq §(c) classifications).docs/proof-debt.mdclassifying all 14 Lean axioms (11 §(c) + 3 §(d)).docs/proof-debt.md:QuantumCNO.v:258/283/296/487/545/551/584).QuantumCNO.lean:134/144/235).Verification
bash ~/developer/repos/standards/scripts/check-trusted-base.sh .results:Quantum cluster errors → 0. Remaining 42 = Physics cluster (Phase 2e, next PR) + 4 Idris2 BoJ markers in
src/abi/Proofs/(out of scope; tracked separately).Triage source
Per-marker classifications come from
docs/proof-debt-triage.md(Phase 1, #58) for the Coq side. Lean Quantum classifications are added in this PR'sdocs/proof-debt.mdsection.Refs
Test plan
check-trusted-base.shQuantum cluster errors → 0 (verified locally; cumulative 88 → 42)🤖 Generated with Claude Code