docs: enumerate CNOCategory.v hom_functor as §(d) DEBT (Phase 2b)#61
Merged
Conversation
Phase 2b of the standards#203 trusted-base rollout. Cluster: CNO common — `proofs/coq/category/CNOCategory.v` (1 marker). The single axiom `hom_functor : forall (C : Category) (A : @obj C), Functor C C` was classified DISCHARGE in #58 Phase 1 triage. The file's leading comment (L312-322) already records why it's axiomatised today: 1. `yoneda_cno` is already proven without it. 2. The proper signature `Functor C SetCategory` needs a SetCategory instance, which requires universe-polymorphism machinery. 3. The conceptual result (CNOs = identity under Yoneda) stands. This PR adds the corresponding §(d) DEBT entry with owner + INDEFINITE deadline (blocked on SetCategory scaffolding). The Coq common namespace `proofs/coq/common/CNO.v` has zero axioms (the 4 historical ones were discharged in #24 / #32). Verification: `check-trusted-base.sh` now reports 122 undocumented (down from 123). The CNOCategory.v entry is documented via file-path mention in `docs/proof-debt.md` (no inline annotation needed for §(d) DEBT items per the policy schema). Refs standards#203, #58. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
hyperpolymath
added a commit
that referenced
this pull request
May 27, 2026
…tries (Phase 2c) (#62) ## Summary Phase 2c of the standards#203 trusted-base rollout. Largest single cluster: Coq + Lean Filesystem (**34 markers total** — 13 Coq + 21 Lean). ## Coq side (13 markers — classifications from #58 Phase 1 triage) ### 8 §(c) AXIOM inline annotations | Line | Identifier | Note | |-----:|------------|------| | 96 | `fs_eq_dec` | Treat as §(c) until property-test budget lands; promote to §(b) then. | | 104 | `mkdir_rmdir_inverse` | POSIX semantics | | 114 | `create_unlink_inverse` | POSIX semantics | | 124 | `read_write_identity` | POSIX semantics | | 130 | `chmod_identity` | POSIX semantics | | 136 | `chown_identity` | POSIX semantics | | 142 | `rename_identity` | POSIX semantics | | 147 | `rename_inverse` | POSIX semantics | ### 5 §(d) DEBT entries (no inline; enumerated in proof-debt.md) - `mkdir_not_identity` (L300), `write_different_not_identity` (L316), `transaction_cno` (L397), `mkdir_idempotent` (L421), `snapshot_restore_identity` (L453). All DISCHARGE candidates per #58. ## Lean side (21 markers — new Phase 2c triage) ### 18 §(c) AXIOM inline annotations - **10 POSIX primitives** (opaque ops): `mkdir`, `rmdir`, `create`, `unlink`, `readFile`, `writeFile`, `stat`, `chmod`, `chown`, `rename`. - **6 POSIX semantics axioms** (mirror Coq §(c)): `mkdir_rmdir_inverse`, `create_unlink_inverse`, `read_write_identity`, `chmod_identity`, `rename_identity`, `rename_inverse`. - **2 snapshot primitives** (opaque ops): `snapshot`, `restore`. ### 3 §(d) DEBT entries (mirror Coq DISCHARGE) - `mkdir_not_identity` (L233), `snapshot_restore_identity` (L288), `mkdir_idempotent` (L309). ## docs/proof-debt.md - New "Phase 2c triage — Lean Filesystem cluster" section with full per-marker tables (primitives / semantics / snapshot / discharge). - §(d) DEBT bucket gains 8 new Filesystem entries (5 Coq + 3 Lean), each with owner + INDEFINITE deadline. - "Lean — pending triage" count updates from 49 → 28. ## Verification ``` $ bash ../standards/scripts/check-trusted-base.sh . [INFO] Found 129 soundness-relevant escape hatch(es). [ERROR] 88/129 escape hatch(es) are undocumented. ``` Down from 122 (after #61) and 123 (after #60). Δ = 34 = the cluster size exactly. **0 Filesystem-specific errors remain.** ## Cumulative progress | PR | Cluster | Markers | Cumulative documented | |-----|---------------|--------:|----------------------:| | #60 | Lambda | 5 | 5 | | #61 | CNO common | 1 | 7 (+1 already-passing) | | #62 | Filesystem | 34 | 41 | Remaining clusters (untriaged Lean + already-triaged Coq): Quantum (50), Physics (39). Out of scope for this PR. Refs standards#203, #58, #60, #61. 🤖 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
…ies (Phase 2d) (#63) ## Summary Phase 2d of the standards#203 trusted-base annotation rollout. Annotates the **Quantum cluster** (Coq `QuantumCNO.v` + `QuantumMechanicsExact.v` + Lean `QuantumCNO.lean`) so its 46 escape hatches are policy-compliant under `scripts/check-trusted-base.sh`. ### Changes - **22 inline `(* AXIOM: ... *)`** in `proofs/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). - **3 inline `(* AXIOM: ... *)`** in `proofs/coq/quantum/QuantumMechanicsExact.v` (X-gate unitarity, unitary-preserves-entropy, no-cloning). - **11 inline `-- AXIOM:`** in `proofs/lean4/QuantumCNO.lean` (mirrors Coq §(c) classifications). - **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 candidates (`QuantumCNO.v:258/283/296/487/545/551/584`). - 3 Lean DEBT mirroring Coq sites (`QuantumCNO.lean:134/144/235`). ### Verification `bash ~/developer/repos/standards/scripts/check-trusted-base.sh .` results: | | Undocumented | |---|---:| | Before this PR | 88/129 | | After this PR | 42/129 | | Drop | **−46** (22 Coq §c + 3 Coq §c + 11 Lean §c + 7 Coq §(d) DISCHARGE-mention + 3 Lean §(d) DEBT mention) | 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's `docs/proof-debt.md` section. ### Refs - Phase 1 triage: #58 - Phase 2a (Lambda): #60 - Phase 2b (CNOCategory): #61 - Phase 2c (Filesystem): #62 - Policy: [standards#203](hyperpolymath/standards#203) - CI enforcement: [standards#211](hyperpolymath/standards#211) ## Test plan - [x] `check-trusted-base.sh` Quantum cluster errors → 0 (verified locally; cumulative 88 → 42) - [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>
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 2b of the standards#203 trusted-base rollout. Cluster: CNO common
—
proofs/coq/category/CNOCategory.v(1 marker).The single axiom
hom_functorwas classified DISCHARGE in #58Phase 1 triage. The file's existing leading comment (L312–322) records
the rationale for current axiomatisation:
yoneda_cnois already proven without it.Functor C SetCategoryneeds aSetCategoryinstance, which requires universe-polymorphism machinery.
Disposition
SetCategoryscaffolding).documentation is via file-path mention in
docs/proof-debt.md.Note on cluster size
The picked "CNO common" cluster was originally Coq
common/CNO.v(4axioms) +
category/CNOCategory.v(1). The 4 axioms incommon/CNO.vwere discharged in #24 / #32 prior to this rollout, so the cluster is
effectively a one-axiom mop-up.
Verification
Down from 123 after PR #60 (Lambda). Cumulative: 7 markers now
documented (Lambda 5 + CNOCategory 1 + 1 other already-passing).
Refs standards#203, #58, #60.
🤖 Generated with Claude Code