docs(proof-status): reconcile post-T0 axiom audit ledger + machine state (#133)

Updates the human + machine documentation to reflect the 2026-05-20
discharge of `eval_deterministic` (PR #24, this branch):

- PROOF-STATUS-2026-05-18.md
  - axiom row: ~121 → ~120; `eval_deterministic` removed from the
    "example post-T0 audit" list with an explicit discharge note.
  - Tier-0 status: post-T0 marked "in progress" (1/~120 discharged).
  - "RESUME HERE" preamble: status block summarising the rebase + the
    proof shape + Print Assumptions report.
  - "Next frontier": ~121 → ~120, eval_deterministic noted as
    1 discharged.

- .machine_readable/6a2/STATE.a2ml
  - last-updated: 2026-02-05 → 2026-05-20.
  - components.coq-proofs: replaced the stale "81 Qed, 19 Admitted, 6
    Defined, 63 Axioms" line (pre-rescue snapshot) with current state
    — 11/11 files compile, 0 Admitted, ~120 axioms with 1 discharged.
  - components.lean4-proofs: "syntax-complete, needs verification"
    replaced with "lake build 1631/1632 green, verified 2026-05-20".
  - components.agda-proofs: 40 → 60 (CNO.agda type-checks clean per
    PROOF-STATUS-2026-05-18 verification).
  - blockers.high: dropped "19 Admitted proofs" (rescue resolved them)
    and "No local coqc" (resolved); kept "Python interpreters violate
    RSR".
  - blockers.medium: added the ~120 axiom audit as a tracked item.
  - critical-next-actions: rotated to "PR #24 review + merge" then
    "Begin classification sweep of remaining ~120 axioms".
  - session-history: prepended 2026-05-20 (this work) and 2026-05-18
    (rescue work) entries.
  - maintenance-status: refreshed to 2026-05-20, last-result = pass.

- .machine_readable/META.scm + .machine_readable/6a2/META.a2ml
  - last-updated bumped to 2026-05-20 (A2ML side).
  - Architecture decisions: added ADR-006 (state_eq PC-exclusion, the
    semantic decision underpinning the rescue) and ADR-007 (this PR's
    discharge of eval_deterministic via step_deterministic_strong).

No content changes outside docs; this is documentation-only and stacks
on the proof commit `6f93e98` already in this PR.

Refs hyperpolymath/standards#124
Refs hyperpolymath/standards#133

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

.machine_readable/6a2/META.a2ml

@@ -6,7 +6,7 @@
 
 [metadata]
 version = "1.0.0"
-last-updated = "2026-02-05"
+last-updated = "2026-05-20"
 
 [project-info]
 license = "PMPL-1.0-or-later"
@@ -19,6 +19,8 @@ decisions = [
   { id = "ADR-003", status = "accepted", title = "Lambda CNO = identity property only, not termination" },
   { id = "ADR-004", status = "accepted", title = "post_execution_dist specialized for CNOs (identity on distributions)" },
   { id = "ADR-005", status = "proposed", title = "Fix QuantumCNO.v Cexp: real exp -> complex phase factor" },
+  { 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" },
 ]
 
 [development-practices]

.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-02-05"
+last-updated = "2026-05-20"
 status = "active"
 
 [project-context]
@@ -26,10 +26,10 @@ maturity = "experimental"
 
 [components]
 # Format: name = [percentage, "notes"]
-coq-proofs = [81, "81 Qed, 19 Admitted, 6 Defined, 63 Axioms"]
-lean4-proofs = [70, "syntax-complete, needs verification"]
+coq-proofs = [88, "11/11 files compile (Coq 8.18.0+8.20.1); 0 Admitted (rescue 2026-05-18); ~120 Axiom/Parameter as post-T0 audit, 1 discharged (eval_deterministic, PR #24, 2026-05-20)"]
+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 = [40, "phase 1 complete"]
+agda-proofs = [60, "CNO.agda type-checks clean — 0 postulates/holes/unsolved metas (verified 2026-05-18)"]
 isabelle-proofs = [40, "phase 1 complete"]
 mizar-proofs = [10, "stub, needs installation"]
 
@@ -53,26 +53,22 @@ milestones = [
 [blockers-and-issues]
 critical = []
 high = [
-  "19 Admitted proofs in Coq",
   "Python interpreters violate RSR",
-  "No local coqc for compilation",
 ]
 medium = [
-  "QuantumCNO.v Cexp real-vs-phase bug",
   "LandauerDerivation.v needs measure theory",
+  "~120 post-T0 Coq Axiom/Parameter audit (legitimate model assumption vs avoidable proof shortcut)",
 ]
 low = [
   "y_not_cno non-termination proof",
 ]
 
 [critical-next-actions]
 immediate = [
-  "Complete QuantumCNO.v proofs",
-  "Classify FilesystemCNO.v proofs",
-  "Classify MalbolgeCore.v proof",
+  "PR #24 review + merge (eval_deterministic discharge + rescue rebase)",
 ]
 this-week = [
-  "Target 12-15 of 19 Admitted proofs",
+  "Begin classification sweep of remaining ~120 Axiom declarations",
   "Migrate Python to Rust",
 ]
 this-month = [
@@ -82,13 +78,15 @@ this-month = [
 
 [session-history]
 sessions = [
+  { 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 filed (draft, Refs standards#124+#133)" },
+  { 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" },
   { date = "2026-02-05", agent = "opus", summary = "Completed 8 proofs, created PROOF-INSIGHTS.md" },
   { date = "2026-02-04", agent = "opus", summary = "Completed cno_logically_reversible, added axioms" },
 ]
 
 [maintenance-status]
-last-run-utc = "2026-02-05T00:00:00Z"
-last-result = "unknown"  # unknown | pass | warn | fail
+last-run-utc = "2026-05-20T15:00:00Z"
+last-result = "pass"  # unknown | pass | warn | fail
 
 [migration-notes]
 # Fields from STATE.scm that map cleanly:

.machine_readable/META.scm

@@ -8,7 +8,9 @@
      ("ADR-002" "accepted" "Dual Landauer formalization: axiom (StatMech.v) + derivation (LandauerDerivation.v)")
      ("ADR-003" "accepted" "Lambda CNO = identity property only, not termination")
      ("ADR-004" "accepted" "post_execution_dist specialized for CNOs (identity on distributions)")
-     ("ADR-005" "proposed" "Fix QuantumCNO.v Cexp: real exp -> complex phase factor")))
+     ("ADR-005" "proposed" "Fix QuantumCNO.v Cexp: real exp -> complex phase factor")
+     ("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")))
 
   (development-practices
     (code-style "Coq proof engineering")

PROOF-STATUS-2026-05-18.md

@@ -78,14 +78,14 @@ quantum) `Require Import CNO.Complex.` — fixes the inconsistent
 | `proofs/coq/filesystem/FilesystemCNO.v` | ✅ compiles | fixed `CNO.CNO` import and `fold_left` argument order. |
 | `proofs/lean4/CNO.lean` | ✅ builds | completed `loadStore_preserves_memory` cons case with rewrite helper lemmas; no proof holes. |
 | `proofs/lean4/{FilesystemCNO,LambdaCNO,QuantumCNO,StatMech,CNOCategory}.lean` | ✅ build | full `lake build` succeeds. |
-| ~121 Coq `Axiom`/`Parameter` | ⚠️ assumptions | **NOT holes.** Separate post-T0 audit (e.g. `eval_deterministic`, `cno_decidable`, `eval_respects_state_eq_left/right`). |
+| ~120 Coq `Axiom`/`Parameter` | ⚠️ assumptions | **NOT holes.** Separate post-T0 audit (e.g. `cno_decidable`, `eval_respects_state_eq_left/right`). `eval_deterministic` was on this list — **discharged 2026-05-20** (PR `#24`, `Print Assumptions` "Closed under the global context"). |
 
 ## Tier-0 status
 
 - **Keystone complete:** `CNO.v` (Coq) + `CNO.agda` (Agda) verified.
 - **T0 complete:** dependent Coq files, `StatMech_helpers.v`, and full Lean package build.
-- **Post-T0:** the ~121-axiom audit (classify *legitimate model assumption*
-  vs *hard proof papered over*).
+- **Post-T0 (in progress):** the ~120-axiom audit (classify *legitimate model assumption*
+  vs *hard proof papered over*). 1 axiom discharged so far (`eval_deterministic`).
 
 ## Position vs. before the review
 
@@ -100,6 +100,15 @@ scoped above.
 
 # RESUME HERE — post-T0 axiom audit
 
+**Status update 2026-05-20.** Rescue work rebased onto current `main` and
+the first post-T0 axiom (`eval_deterministic`) discharged in PR
+[`#24`](https://github.com/hyperpolymath/absolute-zero/pull/24) — replaced
+by `Theorem eval_deterministic` proved from a new helper `Lemma
+step_deterministic_strong`. `Print Assumptions` on both reports "Closed
+under the global context". Re-verified on Coq 8.18.0 + 8.20.1 (proof is
+portable). Full `lake build` 1631/1632 green; all 11 Coq files
+recompile clean. ~120 other `Axiom`/`Parameter` declarations remain.
+
 **Branch:** `repair/proofs-tier0-2026-05-18` (not pushed). Repo:
 `~/dev/repos/absolute-zero`.
 
@@ -132,5 +141,6 @@ scoped above.
 - Coq: every file under `proofs/coq/{common,quantum,lambda,physics,malbolge,category,filesystem}` compiles with Coq 8.20.1 via `build-coq.sh`.
 - Lean: `lake build` succeeds for all Lean targets.
 
-**Next frontier:** the ~121 Coq `Axiom`/`Parameter` audit (legitimate model
-assumption vs avoidable proof shortcut).
+**Next frontier:** the ~120 Coq `Axiom`/`Parameter` audit (legitimate model
+assumption vs avoidable proof shortcut). 1 discharged (`eval_deterministic`,
+PR `#24`, 2026-05-20).