docs: Phase 1 per-axiom triage of 72 Coq Axioms by hyperpolymath · Pull Request #58 · hyperpolymath/absolute-zero

hyperpolymath · 2026-05-27T07:47:26Z

Summary

Adds docs/proof-debt-triage.md — Phase 1 of the proof-debt triage process described in the seed docs/proof-debt.md (PR #52). Classifies every Coq Axiom in the repo against the standards#203 trusted-base reduction policy:

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 postulates in src/abi/Layout.idr (tracked by audit: 2 Idris2 postulates in src/abi/Layout.idr — alignment + alignedSize correctness #27).

Follow-ups surfaced by triage

De-duplicate physics constants — kB_positive / temperature_positive declared 3x across QuantumCNO, StatMech, LandauerDerivation.
De-duplicate quantum laws — unitary_preserves_entropy and no_cloning declared twice with the same name.
De-duplicate probability + decidability + Shannon axioms between StatMech.v and LandauerDerivation.v.
Define Cexp constructively in Complex.v — collapses 4 axioms in QuantumCNO to DISCHARGE.
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

…split) Companion to docs/proof-debt.md (PR #52 seed). Classifies every Coq Axiom in the repo into the standards#203 trusted-base policy schema: - 52 AXIOM (TRUSTED-BASE: physics constants, quantum gate primitives, POSIX semantics, Kolmogorov + Shannon axioms, complex exponential algebra, fundamental physical laws) - 17 DISCHARGE (derivable theorems mistakenly stated as Axiom — the backlog for subsequent proof PRs) - 3 PROPERTY-TEST (decidability claims over opaque types) Scope is Coq Axioms only; 52 Lean 4 axioms + 7 Idris2 postulates (issue #27) are listed as out-of-scope follow-ups. Surfaces 5 concrete follow-ups, the biggest being physics-constant deduplication (kB_positive/temperature_positive each declared 3x) and constructive definition of Cexp in Complex.v (would collapse 4 axioms). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

## Summary Cleanup follow-on to #58 (Phase 1 per-axiom triage of 72 Coq Axioms). Wires the new triage doc into the existing seed and refreshes machine-readable state. - **CHANGELOG.md** — add #58 under Unreleased/Documentation. - **docs/proof-debt.md** — link to `docs/proof-debt-triage.md`; refresh §(a)/§(b)/§(c)/§(d) sections to reflect the Phase 1 disposition (52 c / 17 a / 3 b for Coq); update headline count 129 → 124 reflecting intervening closures. - **.machine_readable/6a2/STATE.a2ml** — bump `last-updated` to 2026-05-27; replace stale "begin classification sweep" next-action with the 17 §a discharge backlog + Phase 2 (Lean axioms + Idris2 postulates); add 2026-05-27 session-history entry; refresh `coq-proofs` component summary. - **.machine_readable/6a2/META.a2ml** — bump `last-updated`; add ADR-009 (was missing here vs `META.scm`) + new ADR-010 for the Phase 1 triage. - **.machine_readable/META.scm** — add ADR-010 matching `META.a2ml` for parity. No code changes; documentation + machine-readable state only. ## Test plan - [ ] Visual review of the 5 file diffs - [ ] `check-trusted-base.sh` count unchanged (124 — no axioms touched) 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

…a triage (#60) ## Summary Phase 2a of the standards#203 trusted-base reduction policy rollout (follow-up to #58 / #59 Coq triage). First cluster: `proofs/coq/lambda/` + `proofs/lean4/LambdaCNO.lean`. ### Coq (2 markers, both §(c) AXIOM per #58 triage) - `proofs/coq/lambda/LambdaCNO.v:356` `y_not_cno` — inline `(* AXIOM: ... *)` annotation added. - `proofs/coq/lambda/LambdaCNO.v:376` `eta_equivalence` — inline `(* AXIOM: ... *)` annotation added. ### Lean (3 markers — new Phase 2a triage) | Line | Identifier | Disposition | |-----:|------------|-------------| | 183 | `subst_closed_term` | §(d) DEBT (provable; INDEFINITE) | | 232 | `y_combinator_not_identity` | §(c) AXIOM (inline annotation added) | | 258 | `eta_equivalence` | §(c) AXIOM (inline annotation added) | ### docs/proof-debt.md - New "Phase 2a triage — Lean Lambda cluster" section with per-marker table. - §(d) bucket gains the Lean `subst_closed_term` DEBT entry (owner + INDEFINITE deadline). ## Verification ``` $ bash ../standards/scripts/check-trusted-base.sh . [INFO] Found 129 soundness-relevant escape hatch(es). [OK] proof-debt document(s) found: docs/proof-debt.md [ERROR] 123/129 escape hatch(es) are undocumented. ``` **Lambda-specific errors: 0** (down from 5). The remaining 123 errors are the Quantum / Filesystem / Physics clusters, scheduled for follow-up PRs (Phase 2b/2c/2d). ## Test plan - [x] check-trusted-base.sh reports 0 errors on Lambda lines. - [x] All inline annotations precede Axiom / axiom within the script's 5-line lookback. - [x] Lean §(d) DEBT entry has owner + deadline per standards#203 schema. - [ ] Coq build still green (no semantic change — only added comments). - [ ] Lean build still green (no semantic change — only added comments). Refs standards#203, #58, #59. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

## Summary Phase 2b of the standards#203 trusted-base rollout. Cluster: CNO common — `proofs/coq/category/CNOCategory.v` (1 marker). The single axiom `hom_functor` was classified **DISCHARGE** in #58 Phase 1 triage. The file's existing leading comment (L312–322) records the rationale for current axiomatisation: 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. ## Disposition - §(d) DEBT, INDEFINITE deadline (blocked on `SetCategory` scaffolding). - No inline annotation needed for §(d) per the policy schema — 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` (4 axioms) + `category/CNOCategory.v` (1). The 4 axioms in `common/CNO.v` were discharged in #24 / #32 prior to this rollout, so the cluster is effectively a one-axiom mop-up. ## Verification ``` $ bash ../standards/scripts/check-trusted-base.sh . [INFO] Found 129 soundness-relevant escape hatch(es). [ERROR] 122/129 escape hatch(es) are undocumented. ``` 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](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

…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>

…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>

…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>

… + 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>

#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>

hyperpolymath merged commit e17256b into main May 27, 2026
8 of 14 checks passed

hyperpolymath deleted the docs/proof-debt-triage-2026-05-27 branch May 27, 2026 07:47

hyperpolymath mentioned this pull request May 27, 2026

docs+meta: cleanup after #58 — proof-debt cross-refs + STATE/META #59

Merged

2 tasks

hyperpolymath mentioned this pull request May 27, 2026

docs+annotate: Lambda cluster — inline AXIOM: comments + Lean Phase 2a triage #60

Merged

5 tasks

hyperpolymath mentioned this pull request May 27, 2026

docs: enumerate CNOCategory.v hom_functor as §(d) DEBT (Phase 2b) #61

Merged

hyperpolymath mentioned this pull request May 27, 2026

docs+annotate: Filesystem cluster — 26 inline AXIOM: + 8 §(d) DEBT entries (Phase 2c) #62

Merged

hyperpolymath mentioned this pull request May 27, 2026

docs+annotate: Quantum cluster — 36 inline AXIOM: + 10 §(d) DEBT entries (Phase 2d) #63

Merged

3 tasks

hyperpolymath mentioned this pull request May 27, 2026

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

Merged

3 tasks

hyperpolymath mentioned this pull request May 27, 2026

refactor(proofs/coq): consolidate trusted-base dups (Follow-ups 1+2+3) #67

Merged

6 tasks

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

docs: Phase 1 per-axiom triage of 72 Coq Axioms#58

docs: Phase 1 per-axiom triage of 72 Coq Axioms#58
hyperpolymath merged 1 commit into
mainfrom
docs/proof-debt-triage-2026-05-27

hyperpolymath commented May 27, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Uh oh!

Conversation

hyperpolymath commented May 27, 2026

Summary

Scope

Follow-ups surfaced by triage

Method

Test plan

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant