Skip to content

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

Merged
hyperpolymath merged 1 commit into
mainfrom
proof-debt/physics-cluster-annotations
May 27, 2026
Merged

docs+annotate: Physics cluster — 38 inline AXIOM: + 4 §(d) DEBT entries (Phase 2e)#66
hyperpolymath merged 1 commit into
mainfrom
proof-debt/physics-cluster-annotations

Conversation

@hyperpolymath
Copy link
Copy Markdown
Owner

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

Test plan

  • `check-trusted-base.sh` Physics cluster errors → 0 (verified locally; cumulative 42 → 4)
  • No code semantics changed; comments + docs only
  • CI green on this branch

🤖 Generated with Claude Code

…es (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>
@hyperpolymath hyperpolymath merged commit 5650dd0 into main May 27, 2026
13 of 17 checks passed
@hyperpolymath hyperpolymath deleted the proof-debt/physics-cluster-annotations branch May 27, 2026 10:47
@github-actions
Copy link
Copy Markdown

🔍 Hypatia Security Scan

Findings: 65 issues detected

Severity Count
🔴 Critical 9
🟠 High 16
🟡 Medium 40

⚠️ Action Required: Critical security issues found!

View findings
[
  {
    "reason": "Ada pragma Suppress disables runtime checks (1 occurrences, CWE-704)",
    "type": "ada_pragma_suppress",
    "file": "/home/runner/work/absolute-zero/absolute-zero/examples/ada/balanced_ops.adb",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "high"
  },
  {
    "reason": "User-defined Coq axiom -- not verified by kernel (3 occurrences, CWE-704)",
    "type": "coq_axiom",
    "file": "/home/runner/work/absolute-zero/absolute-zero/proofs/coq/quantum/QuantumMechanicsExact.v",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "User-defined Coq axiom -- not verified by kernel (29 occurrences, CWE-704)",
    "type": "coq_axiom",
    "file": "/home/runner/work/absolute-zero/absolute-zero/proofs/coq/quantum/QuantumCNO.v",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "User-defined Coq axiom -- not verified by kernel (2 occurrences, CWE-704)",
    "type": "coq_axiom",
    "file": "/home/runner/work/absolute-zero/absolute-zero/proofs/coq/lambda/LambdaCNO.v",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "User-defined Coq axiom -- not verified by kernel (1 occurrences, CWE-704)",
    "type": "coq_axiom",
    "file": "/home/runner/work/absolute-zero/absolute-zero/proofs/coq/category/CNOCategory.v",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "User-defined Coq axiom -- not verified by kernel (13 occurrences, CWE-704)",
    "type": "coq_axiom",
    "file": "/home/runner/work/absolute-zero/absolute-zero/proofs/coq/filesystem/FilesystemCNO.v",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "Coq admit tactic leaves goal unproven (1 occurrences, CWE-704)",
    "type": "coq_admit_tactic",
    "file": "/home/runner/work/absolute-zero/absolute-zero/proofs/coq/physics/LandauerDerivation.v",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "critical"
  },
  {
    "reason": "User-defined Coq axiom -- not verified by kernel (14 occurrences, CWE-704)",
    "type": "coq_axiom",
    "file": "/home/runner/work/absolute-zero/absolute-zero/proofs/coq/physics/LandauerDerivation.v",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "User-defined Coq axiom -- not verified by kernel (10 occurrences, CWE-704)",
    "type": "coq_axiom",
    "file": "/home/runner/work/absolute-zero/absolute-zero/proofs/coq/physics/StatMech.v",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "undefined/error causes runtime crash (2 occurrences, CWE-754)",
    "type": "undefined_error",
    "file": "/home/runner/work/absolute-zero/absolute-zero/examples/haskell/Nop.hs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "high"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

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>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant