[P2] absolute-zero: finish Lean CNO cons-case + Coq tier-0 rebuild

[hyperpolymath]

Soundness repair in flight 2026-05-18. Complete Lean CNO.lean cons-case + Coq tier-0 rebuild.

Sub-issue of #124. PRs Refs hyperpolymath/standards#124. Joint-close only on explicit agreement.

🤖 Generated with Claude Code

[hyperpolymath]

Reconciliation (licence → proof → tech) + licence P0 shipped

• Licence: was NOT clean. Authorship check (read-only): 100% owner-own, nothing third-party/AGPL-by-intent — drift is scaffold-placeholder leak.
• Proof: main is unsound (state_eq includes state_pc → is_CNO unsatisfiable); the unmerged rescue branch proof-debt/standards-133-coq-rescue-wip fixes it. Top prover-tractable P0 = eval_deterministic (Coq, ~30 lines) — gated on the rescue branch being the base.
• Tech: _CoqProject wires only 2/11 .v; no Coq/Lean CI; Complex.v compiled-but-uncommitted.

Licence ruling APPLIED → absolute-zero#22 (draft, Refs not Closes). 13 drift files → PMPL-1.0-or-later; 4 missing headers added; deleted the 0-byte LICENSE-PALIMPS.txt stub (the repo's own audit trail prescribes removal — not populate).

Residual OWED: the proof-debt arm (merge rescue branch → main unsound until then; eval_deterministic).

[hyperpolymath]

Status update 2026-05-20:

Rescue branch proof-debt/standards-133-coq-rescue-wip (head 1a7d7c2, last touched 2026-05-18 in [UNVERIFIED] state) rebased onto current origin/main — clean, no conflicts. The named eval_deterministic axiom is discharged as part of the same PR:

• Axiom eval_deterministic in proofs/coq/common/CNO.v → real Theorem (same name + type), via a new helper Lemma step_deterministic_strong : forall s i s1 s2, step s i s1 → step s i s2 → s1 = s2 (syntactic step determinism — step constructors emit mkState … whose components are functions of the start state + instruction; the auxiliary witnesses in step_load/step_store/step_add are pinned by their hypotheses).
• Print Assumptions eval_deterministic / step_deterministic_strong / cno_equiv_refl → "Closed under the global context" (no axioms, no admits).
• Build oracle (Coq 8.18.0, not the 8.20.1 the original repair used — proof is portable):
  • all 11 Coq files under proofs/coq/{common,quantum,lambda,physics,malbolge,category,filesystem} recompile clean.
  • full lake build over proofs/lean4 → 1631/1632 green (Lean side untouched by this change).

Draft PR: hyperpolymath/absolute-zero#24 (Refs #124, Refs #133, NOT Closes — joint-close on agreement).

The ~120 other Coq Axiom/Parameter declarations across the corpus (cno_decidable, eval_respects_state_eq_left/right, physics/quantum model assumptions) remain as separate audit work — classify legitimate model assumptions vs avoidable proof shortcuts. They are not in this PR.

🤖 Generated with Claude Code