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

hyperpolymath · claude · hyperpolymath · commit c07adac435dc · 2026-05-27T08:53:48.000+01:00
Cleanup follow-on to PR #58 (Phase 1 per-axiom triage of 72 Coq Axioms): - CHANGELOG.md: add #58 under Unreleased/Documentation. - docs/proof-debt.md: link to docs/proof-debt-triage.md from the seed; update §(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; 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. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
diff --git a/.machine_readable/6a2/META.a2ml b/.machine_readable/6a2/META.a2ml
@@ -6,7 +6,7 @@
 
 [metadata]
 version = "1.0.0"
-last-updated = "2026-05-20"
+last-updated = "2026-05-27"
 
 [project-info]
 license = "MPL-2.0"
@@ -22,6 +22,8 @@ decisions = [
   { id = "ADR-006", status = "accepted", title = "state_eq excludes state_pc — PC is control-flow bookkeeping, not observable side effect (2026-05-18 rescue)" },
   { id = "ADR-007", status = "accepted", title = "Discharge eval_deterministic Axiom → Theorem via step_deterministic_strong helper (2026-05-20, PR #24); first post-T0 axiom audit win" },
   { id = "ADR-008", status = "accepted", title = "Delete unsound eval_respects_state_eq_{left,right} axioms; weaken logically_reversible definition to use =st= (observational reversibility); re-prove cno_eval_on_equal_states + cno_logically_reversible via cno_terminates + cno_preserves_state (2026-05-20); rationale: under PC-excluding state_eq the strong axioms force a syntactically-identical eval result, which is unsound because eval propagates PC deterministically while =st= ignores it" },
+  { id = "ADR-009", status = "accepted", title = "Delete unsound alignmentMatchesPlatformWord Idris2 postulate; consolidate alignedSizeCorrect into shared AbsoluteZero.ABI.Proofs.DivMod module (PR #40, Refs #27)" },
+  { id = "ADR-010", status = "accepted", title = "Phase 1 per-axiom triage of 72 Coq Axioms per standards#203 trusted-base policy (2026-05-27, PR #58): 52 §c TRUSTED-BASE + 17 §a DISCHARGE backlog + 3 §b PROPERTY-TEST; canonical disposition in docs/proof-debt-triage.md" },
 ]
 
 [development-practices]
diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml
@@ -11,7 +11,7 @@ repo = "github.com/hyperpolymath/absolute-zero"
 version = "1.0.0-alpha"
 schema-version = "1.0"
 created = "2026-01-03"
-last-updated = "2026-05-20"
+last-updated = "2026-05-27"
 status = "active"
 
 [project-context]
@@ -26,7 +26,7 @@ maturity = "experimental"
 
 [components]
 # Format: name = [percentage, "notes"]
-coq-proofs = [90, "11/11 files compile (Coq 8.18.0+8.20.1); 0 Admitted (rescue 2026-05-18); 75→73 Axioms + 42 Parameters; 3 discharges 2026-05-20 — eval_deterministic (PR #24) + eval_respects_state_eq_{left,right} (deleted as unsound, downstream refactored to use cno_terminates + weakened logically_reversible); remainder are legitimate model-layer assumptions about abstract Parameters"]
+coq-proofs = [90, "11/11 files compile (Coq 8.18.0+8.20.1); 0 Admitted (rescue 2026-05-18); 75→72 Axioms + 42 Parameters; Phase 1 triage 2026-05-27 (PR #58) classifies 72 Coq Axioms into §c TRUSTED-BASE (52) + §a DISCHARGE backlog (17) + §b PROPERTY-TEST (3); see docs/proof-debt-triage.md"]
 lean4-proofs = [95, "lake build 1631/1632 green (mathlib + 6 lean_lib targets); verified 2026-05-20"]
 z3-proofs = [90, "10 theorems encoded, needs z3 runtime"]
 agda-proofs = [60, "CNO.agda type-checks clean — 0 postulates/holes/unsolved metas (verified 2026-05-18)"]
@@ -57,18 +57,20 @@ high = [
 ]
 medium = [
   "LandauerDerivation.v needs measure theory",
-  "~120 post-T0 Coq Axiom/Parameter audit (legitimate model assumption vs avoidable proof shortcut)",
+  "17 §a DISCHARGE Coq axioms backlog (post-Phase-1 triage, see docs/proof-debt-triage.md)",
+  "Triage Phase 2 for 52 Lean axioms + 7 Idris2 postulates (#27) still pending",
 ]
 low = [
   "y_not_cno non-termination proof",
 ]
 
 [critical-next-actions]
 immediate = [
-  "PR #24 review + merge (eval_deterministic discharge + rescue rebase)",
+  "Phase 2 triage: Lean axioms (52) + Idris2 postulates (#27, 7)",
 ]
 this-week = [
-  "Begin classification sweep of remaining ~120 Axiom declarations",
+  "Begin discharging the 17 §a Coq DISCHARGE-backlog axioms (lowest-hanging: cno_zero_energy_dissipation_derived, fidelity_bound, unitary_inverse_property, *_not_identity existence pair)",
+  "Physics-constant deduplication (kB_positive/temperature_positive declared 3x across QuantumCNO/StatMech/LandauerDerivation)",
   "Migrate Python to Rust",
 ]
 this-month = [
@@ -78,6 +80,7 @@ this-month = [
 
 [session-history]
 sessions = [
+  { date = "2026-05-27", agent = "opus", summary = "Phase 1 per-axiom triage of all 72 Coq Axioms per standards#203 trusted-base policy. Classification: 52 §c TRUSTED-BASE (physics constants, quantum primitives, POSIX semantics, Kolmogorov+Shannon axioms, Cexp algebra, physical laws), 17 §a DISCHARGE (derivable theorems incl. 2 named *_derived), 3 §b PROPERTY-TEST (decidability over opaque types). Surfaced 5 follow-ups (physics-constant dedup ×3, quantum-law dedup ×2, Cexp constructive in Complex.v). PR #58 MERGED 2026-05-27 (commit e17256b). Also: traced phantom '315 Lean sorries' figure to a metric mismatch — actual local user-sorry count = 0; canonical figure is 129 (now 124) escape hatches across all proof languages per standards#195 + scripts/check-trusted-base.sh." },
   { date = "2026-05-20", agent = "opus", summary = "Post-T0 axiom audit: 117 declarations triaged into Tier A/B/C; 2 unsound axioms (eval_respects_state_eq_left/right) deleted with downstream refactor; logically_reversible weakened to =st=; cno_eval_on_equal_states + cno_logically_reversible re-proved without axioms; 75→73 Axioms total" },
   { date = "2026-05-20", agent = "opus", summary = "Rescue branch rebased onto current main (clean); eval_deterministic Axiom discharged → Theorem (via step_deterministic_strong helper); Print Assumptions Closed under global context; 11/11 Coq + 1631/1632 Lean targets green; PR #24 MERGED (admin-squash 69e7a22)" },
   { date = "2026-05-18", agent = "opus", summary = "Tier-0 rescue: CNO.v keystone re-proved (state_eq PC-exclusion fix, 9 named repairs); Complex.v self-contained complex numbers added; 11 Coq files compile under Coq 8.20.1; full Lean lake build succeeds; PROOF-STATUS-2026-05-18.md ledger added" },
@@ -86,7 +89,7 @@ sessions = [
 ]
 
 [maintenance-status]
-last-run-utc = "2026-05-20T15:00:00Z"
+last-run-utc = "2026-05-27T08:00:00Z"
 last-result = "pass"  # unknown | pass | warn | fail
 
 [migration-notes]
diff --git a/.machine_readable/META.scm b/.machine_readable/META.scm
@@ -12,7 +12,8 @@
      ("ADR-006" "accepted" "state_eq excludes state_pc — PC is control-flow bookkeeping, not observable side effect (2026-05-18 rescue)")
      ("ADR-007" "accepted" "Discharge eval_deterministic Axiom → Theorem via step_deterministic_strong helper (2026-05-20, PR #24); first post-T0 axiom audit win")
      ("ADR-008" "accepted" "Delete unsound eval_respects_state_eq_{left,right} axioms; weaken logically_reversible to =st= (observational reversibility); re-prove cno_eval_on_equal_states + cno_logically_reversible via cno_terminates + cno_preserves_state (2026-05-20)")
-     ("ADR-009" "accepted" "Delete unsound alignmentMatchesPlatformWord Idris2 postulate (HasAlignment carries no evidence; would derive So (1 mod 8 == 0) from CNOResultLayout.alignment); replace single consumer with per-Platform decidable proof. Consolidate remaining alignedSizeCorrect postulate into shared AbsoluteZero.ABI.Proofs.DivMod module as the estate-wide div/mod lemma surface (absolute-zero#27, civic-connect alignUpDivides/mkFieldsAligned/offsetInBoundsPrf migrate here)")))
+     ("ADR-009" "accepted" "Delete unsound alignmentMatchesPlatformWord Idris2 postulate (HasAlignment carries no evidence; would derive So (1 mod 8 == 0) from CNOResultLayout.alignment); replace single consumer with per-Platform decidable proof. Consolidate remaining alignedSizeCorrect postulate into shared AbsoluteZero.ABI.Proofs.DivMod module as the estate-wide div/mod lemma surface (absolute-zero#27, civic-connect alignUpDivides/mkFieldsAligned/offsetInBoundsPrf migrate here)")
+     ("ADR-010" "accepted" "Phase 1 per-axiom triage of 72 Coq Axioms per standards#203 trusted-base policy (2026-05-27, PR #58): 52 §c TRUSTED-BASE + 17 §a DISCHARGE backlog + 3 §b PROPERTY-TEST; canonical disposition in docs/proof-debt-triage.md")))
 
   (development-practices
     (code-style "Coq proof engineering")
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -37,6 +37,7 @@ this project aims to follow [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ### Documentation
 
+- docs: Phase 1 per-axiom triage of 72 Coq Axioms (#58)
 - docs: seed docs/proof-debt.md per trusted-base policy (#52)
 - docs: record tech-debt audit findings (2026-05-26) (#47)
 
diff --git a/docs/proof-debt.md b/docs/proof-debt.md
@@ -11,37 +11,53 @@ SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath)
 
 The 2026-05-26 estate proof-debt audit
 ([standards#195](https://github.com/hyperpolymath/standards/pull/195))
-detected **129 soundness-relevant escape hatches** in this
-repo. This file is the **initial seed** — every marker starts in §(d)
-DEBT and the maintainer triages each into §(a) / §(b) / §(c) / §(d) as
-classification proceeds.
+detected **129 soundness-relevant escape hatches** in this repo (now
+**124** after intervening closures). Markers were originally seeded
+in §(d) DEBT pending classification.
 
-## (a) DISCHARGED in this repo
+## Phase 1 triage — 72 Coq Axioms (2026-05-27, [#58](https://github.com/hyperpolymath/absolute-zero/pull/58))
 
-*(None yet — entries move here when the proof lands or the construct
-is removed.)*
+The per-marker classification for every Coq `Axiom` lives in
+[`docs/proof-debt-triage.md`](./proof-debt-triage.md). Summary:
 
-## (b) BUDGETED — tested with a refutation budget
+| Disposition | Count |
+|-------------|------:|
+| §(c) AXIOM (TRUSTED-BASE) | 52 |
+| §(a) DISCHARGE backlog    | 17 |
+| §(b) PROPERTY-TEST        |  3 |
+| **Total Coq Axioms**      | **72** |
 
-*(None yet — entries belong here when the construct is at an
-extraction boundary and is covered by a documented property-test
-budget.)*
+Out of scope for Phase 1 (still in §(d) pending future triage):
+52 Lean 4 `axiom` declarations and the 7 Idris2 postulates tracked by
+[#27](https://github.com/hyperpolymath/absolute-zero/issues/27).
 
-## (c) NECESSARY AXIOM
+## (a) DISCHARGE backlog (Coq, 17)
 
-*(None yet — entries belong here when the construct encodes a
-metatheoretic assumption that cannot be discharged within the working
-logic.)*
+Provable propositions currently stated as `Axiom`. Enumerated in
+[`docs/proof-debt-triage.md`](./proof-debt-triage.md) — each row marked
+`DISCHARGE` is a candidate for a future proof PR.
+
+## (b) BUDGETED — tested with a refutation budget (3)
+
+Decidability claims over opaque types: `fs_eq_dec`, `state_dec`,
+`state_eq_dec`. Belong to §(b) once a §(b) property-test budget is
+attached; otherwise treat as §(c).
+
+## (c) NECESSARY AXIOM (Coq, 52)
+
+Physics constants, quantum gate primitives, POSIX semantics,
+Kolmogorov + Shannon entropy core inequalities, complex exponential
+algebra, and fundamental physical laws (second law, Landauer, no-cloning).
+Full enumeration in [`docs/proof-debt-triage.md`](./proof-debt-triage.md).
 
 ## (d) DEBT — actively to be closed
 
-All 129 markers below start in this section. As the
-maintainer classifies each, it should be moved into §(a) / §(b) /
-§(c) as appropriate. Markers that genuinely belong in §(d) need a
-deadline and an owner.
+After Phase 1, the §(d) bucket contains only the 52 Lean axioms and
+7 Idris2 postulates that have not yet been triaged. Coq markers are
+no longer in §(d).
 
 ```
-(no markers; check-trusted-base passes already)
+(no Coq markers in §(d) post Phase 1; see triage doc for §a/§b/§c.)
 ```
 
 > If `129` > 30, the list above shows the first 30 only.
