proof(coq): #133 rescue rebase + discharge eval_deterministic

[hyperpolymath]

Summary

Two-part deliverable under hyperpolymath/standards#133 (the absolute-zero arm of the estate proof-debt epic standards#124):

1. Rebase the long-standing proof-debt/standards-133-coq-rescue-wip branch onto current origin/main (it was 4 ahead / 7 behind; rebase was clean, no conflicts). This restores main soundness eligibility — the rescue work was originally committed 2026-05-18 in an [UNVERIFIED] state with PROOF-STATUS-2026-05-18.md noting "the keystone Coq file CNO.v did not compile at all" before the repair.

2. Discharge eval_deterministic — the file's standout proof-debt postulate. CNO.v previously declared it as an Axiom with an in-file admission that it "could be proven by induction on the evaluation relation". This PR does that proof:

   • New Lemma step_deterministic_strong — syntactic equality of step results given matching inputs (step s i s1 → step s i s2 → s1 = s2). Holds because step constructors emit mkState … whose components are functions of the start state + instruction, and the auxiliary witnesses in step_load/step_store/step_add are pinned by their hypotheses (e.g. state_memory s addr = val).
   • New Theorem eval_deterministic (replacing the prior Axiom, same name and type — the sole in-tree caller cno_equiv_refl is unchanged) — induction on the eval derivation; step_deterministic_strong forces the intermediate state to coincide so the IH closes the tail.

Verification (build-is-oracle)

• coqc -R common CNO common/CNO.v → exit 0 on Coq 8.18.0 (rescue branch was originally repaired against 8.20.1; the new proof is portable).
• Print Assumptions eval_deterministic. → "Closed under the global context" (no axioms, no admits).
• Print Assumptions step_deterministic_strong. → likewise closed.
• Print Assumptions cno_equiv_refl. → likewise closed (downstream consumer).
• All 11 Coq proof files under proofs/coq/{common,quantum,lambda,physics,malbolge,category,filesystem} recompile clean.
• Full lake build over proofs/lean4 → 1631/1632 targets green (Lean untouched by this change; re-verified for absence of regression).

What this does NOT close

Per the rescue branch's own PROOF-STATUS-2026-05-18.md, there are still ~120 other Coq Axiom/Parameter declarations across the corpus (cno_decidable, eval_respects_state_eq_left/right, the physics/quantum model assumptions, etc.). That is a separate audit task — classify legitimate model assumptions vs avoidable proof shortcuts. This PR addresses the single most-cited one and the only one the file itself flagged as "could be proven".

Test plan

• coqc -R common CNO common/CNO.v exit 0 (verified locally)
• Print Assumptions eval_deterministic. reports "Closed under the global context" (verified locally)
• All 11 Coq dependents compile (verified locally)
• lake build green (verified locally, 1631/1632)

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

🤖 Generated with Claude Code

[github-actions]

🔍 Hypatia Security Scan

Findings: 65 issues detected

Severity	Count
🔴 Critical	7
🟠 High	11
🟡 Medium	47

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "Stray AI.a2ml in root -- use 0-AI-MANIFEST.a2ml only",
    "type": "banned",
    "file": "AI.a2ml",
    "action": "delete",
    "rule_module": "root_hygiene",
    "severity": "high"
  },
  {
    "reason": "Superseded by 0-AI-MANIFEST.a2ml",
    "type": "banned",
    "file": "AI.djot",
    "action": "delete",
    "rule_module": "root_hygiene",
    "severity": "high"
  },
  {
    "reason": "No test directory or test files found",
    "type": "no_tests",
    "file": "/home/runner/work/absolute-zero/absolute-zero",
    "action": "flag",
    "rule_module": "honest_completion",
    "severity": "high",
    "deduction": 20
  },
  {
    "reason": "Issue in quality.yml",
    "type": "missing_workflow",
    "file": "quality.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Issue in security-policy.yml",
    "type": "missing_workflow",
    "file": "security-policy.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Action hyperpolymath/standards/.github/workflows/governance-reusable.yml@main needs attention",
    "type": "unpinned_action",
    "file": "governance.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Action actions/checkout@v6.0.2 needs attention",
    "type": "unpinned_action",
    "file": "jekyll-gh-pages.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Action actions/configure-pages@v6 needs attention",
    "type": "unpinned_action",
    "file": "jekyll-gh-pages.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Action actions/jekyll-build-pages@v1 needs attention",
    "type": "unpinned_action",
    "file": "jekyll-gh-pages.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Action actions/upload-pages-artifact@v5 needs attention",
    "type": "unpinned_action",
    "file": "jekyll-gh-pages.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence