proofs: repair Coq keystone CNO.v, add self-contained Complex, status ledger

The "100% complete / 0 Admitted" claim was inaccurate: proofs/coq/common/
CNO.v did not compile at all. This repairs the Tier-0 keystone.

CNO.v (now compiles clean under Coq 8.20):
- eval_app (both dirs): brittle inversion-autoname -> shape/derivation
- state_eq_refl: removed dead `unfold mem_eq` ("No such goal")
- cno_composition/empty_is_cno/nop_is_cno: robust nested split, fresh names
- SOUNDNESS FIX: state_eq drops the program-counter conjunct (every
  instruction advances PC, so the old def made every non-empty CNO false;
  nop_is_cno was unprovable). state_eq = memory + registers + I/O.
- cno_equiv_sym: inline component flip (no Symmetric instance)
- cno_eval_on_equal_states: real logic bug (wrong existential witness)
- state_eq/_trans/_sym: 4 -> 3 conjunct refactor

Complex.v (new): self-contained complex numbers (C = R*R). Replaces the
non-existent Coq.Complex.Complex; Coquelicot rejected (mathcomp2 + HB +
coq-elpi weight for shallow usage). Quantum files rewired to CNO.Complex;
build convention standardized to CNO.CNO / CNO.Complex.

PROOF-STATUS-2026-05-18.md: honest per-file proof-debt ledger correcting
the prior inaccurate completion docs.

Verified: Agda proofs/agda/CNO.agda clean; common/CNO.v and
common/Complex.v compile clean.

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

Author: hyperpolymath

PROOF-STATUS-2026-05-18.md

@@ -0,0 +1,96 @@
+# Proof Status — 2026-05-18 (Review & Repair)
+
+**Author of this analysis:** Claude (review session, 2026-05-18)
+**Scope:** Independent verification + repair of the absolute-zero proof corpus.
+
+> ⚠️ **Correction of prior documentation.** `PROOF-COMPLETION-2026-02-06.md`
+> claims *"100% COMPLETE (0 Admitted)"*. That is **inaccurate**. The keystone
+> Coq file `proofs/coq/common/CNO.v` **did not compile at all** (multiple
+> broken proofs, a soundness defect, and a real logic bug); "0 Admitted" was
+> achieved partly by **axiomatization** and the remaining proofs were
+> bit-rotted/false. This document records the *true* state.
+
+## Toolchain (reproducible)
+
+- Coq **8.20.1** via `nix … github:NixOS/nixpkgs/nixos-24.11#coq`
+- Agda **2.7.0.1** + `standard-library` **2.1.1** via the same nixpkgs pin
+  (also builds clean under Agda 2.6.3 / 2.8.0 — interfaces in `_build/`)
+- Lean toolchain `leanprover/lean4:v4.16.0` + mathlib (via `elan`/`lake`)
+
+## ✅ Verified (machine-checked)
+
+| Artifact | Status |
+|---|---|
+| `proofs/agda/CNO.agda` | **type-checks clean** — 0 postulates, 0 holes, 0 unsolved metas. This is the file `echo-types` depends on (`depend: absolute-zero`). |
+| `proofs/coq/common/CNO.v` | **compiles clean** (one cosmetic `non-recursive fixpoint` warning on `verification_complexity` base case). |
+
+## Soundness fix (semantic change — deliberate)
+
+`state_eq` previously required `state_pc s1 = state_pc s2`. But `step`
+advances the program counter for **every** instruction (`step_nop` →
+`S (state_pc s)`). Therefore *no non-empty program could ever satisfy
+`is_CNO`* and `nop_is_cno` was **false as stated** — its old "proof" never
+discharged `s.pc = S s.pc`, which is the real reason `CNO.v` never compiled.
+
+**Decision (2026-05-18):** `state_eq` now compares **memory + registers +
+I/O only**; the program counter is control-flow bookkeeping, not an
+observable side effect. This makes the non-trivial CNO claims *genuinely
+provable*. All dependents must be re-verified under the new `state_eq`.
+
+## Bugs fixed in `CNO.v`
+
+1. `eval_app` (→): relied on inversion-autogenerated name `H3` (Coq-version
+   dependent) → rewritten to grab the recursive premise by shape.
+2. `eval_app` (←): same class → re-proved by induction on the derivation.
+3. `state_eq_refl`: dead `unfold mem_eq. reflexivity.` → "No such goal" →
+   version-safe finisher.
+4. `cno_composition`: fragile `repeat split` over the 4-way conjunction +
+   name reuse → explicit nested `split`, fresh names.
+5. `empty_is_cno`: same idiom → robust; reuses `state_eq_refl`.
+6. `nop_is_cno`: **false** under old `state_eq`; now genuinely provable
+   after the PC-exclusion fix; re-proved robustly.
+7. `cno_equiv_sym`: `symmetry` needs a `Symmetric` instance (none) and
+   `state_eq_sym` is defined later → inline component-wise flip.
+8. `cno_eval_on_equal_states`: **real logic bug** — both branches
+   `exists`-ed the wrong witness (`s'`/`s` instead of the end-state `sx`).
+9. `state_eq` / `state_eq_trans` / `state_eq_sym`: refactored 4→3 conjuncts.
+
+## Proof-debt ledger (honest)
+
+| File | State | Blocker |
+|---|---|---|
+| `proofs/agda/CNO.agda` | ✅ verified | — |
+| `proofs/coq/common/CNO.v` | ✅ compiles | — (cosmetic warning) |
+| `proofs/coq/common/Complex.v` | ✅ compiles | **NEW** self-contained complex numbers (`CNO.Complex`). Decision: Coquelicot rejected — drags mathcomp2 + Hierarchy-Builder + coq-elpi for shallow `C=R*R` usage. |
+| `proofs/coq/quantum/QuantumMechanicsExact.v` | ⚠️ dep resolved | now uses `CNO.Complex`; local `Cconj` redef removed; remaining = internal bit-rot (e.g. `QME.v:58`). |
+| `proofs/coq/quantum/QuantumCNO.v` | ⚠️ dep resolved | now uses `CNO.Complex`; remaining = internal bit-rot (e.g. `:45` `dim:nat` vs `R`). |
+
+**Build convention (standardized 2026-05-18):** common dir compiled with
+`-R <common> CNO`; every dependent uses `Require Import CNO.CNO.` and (for
+quantum) `Require Import CNO.Complex.` — fixes the inconsistent
+`CNO` vs `CNO.CNO` Require mismatch across files.
+| `proofs/coq/lambda/LambdaCNO.v` | ❌ | missing `Require Import Lia` + bit-rot |
+| `proofs/coq/physics/StatMech.v` | ❌ | `Require`/`-R` convention (`CNO` vs `CNO.CNO`) + likely CNO.v-class bit-rot |
+| `proofs/coq/physics/LandauerDerivation.v` | ❌ | same |
+| `proofs/coq/malbolge/MalbolgeCore.v` | ❌ | same |
+| `proofs/coq/category/CNOCategory.v` | ❌ | same |
+| `proofs/coq/filesystem/FilesystemCNO.v` | ❌ | same |
+| `proofs/lean4/CNO.lean` | ❌ | genuine incomplete proof — `cons` case of the memory-preservation lemma |
+| `proofs/lean4/{FilesystemCNO,LambdaCNO,QuantumCNO}.lean` | ✅ build | — |
+| ~121 Coq `Axiom`/`Parameter` | ⚠️ assumptions | **NOT holes.** Separate post-T0 audit (e.g. `eval_deterministic`, `cno_decidable`, `eval_respects_state_eq_left/right`). |
+
+## Tier-0 status
+
+- **Keystone complete:** `CNO.v` (Coq) + `CNO.agda` (Agda) verified.
+- **T0 remaining:** the 7 dependent Coq files + the Lean `CNO.lean` lemma.
+- **Post-T0:** the ~121-axiom audit (classify *legitimate model assumption*
+  vs *hard proof papered over*).
+
+## Position vs. before the review
+
+Before: believed "100% complete" while the keystone **did not compile**
+(false confidence). After: keystone genuinely verified + Agda verified +
+an accurate ledger. **Better in reality and epistemically**; not the
+illusory "100%". The underlying thesis is plausibly intact; the
+*formalization* required real repair — keystone delivered, remainder
+scoped above.

proofs/coq/common/CNO.v

@@ -61,10 +61,14 @@ Record ProgramState : Type := mkState {
 
 (** State equality *)
 Definition state_eq (s1 s2 : ProgramState) : Prop :=
+  (* NOTE (2026-05-18): state_pc is deliberately EXCLUDED. The program
+     counter is control-flow bookkeeping, not an observable side effect;
+     `step` advances it for every instruction, so requiring PC-equality
+     made `nop_is_cno` (and every non-empty CNO claim) FALSE. Observable
+     state = memory + registers + I/O. *)
   s1.(state_memory) =mem= s2.(state_memory) /\
   s1.(state_registers) = s2.(state_registers) /\
-  s1.(state_io) = s2.(state_io) /\
-  s1.(state_pc) = s2.(state_pc).
+  s1.(state_io) = s2.(state_io).
 
 Notation "s1 '=st=' s2" := (state_eq s1 s2) (at level 70).
 
@@ -268,27 +272,28 @@ Proof.
     + (* p1 = i :: p1' *)
       simpl in H.
       inversion H; subst.
-      apply IH in H3.
-      destruct H3 as [sm [H3a H3b]].
+      (* Grab the recursive `eval (p1' ++ p2)` premise by shape, not by the
+         inversion-autogenerated name (which is Coq-version dependent — the
+         old `H3` broke under Coq 8.20). *)
+      match goal with
+      | [ Hrec : eval (p1' ++ p2) _ _ |- _ ] =>
+          apply IH in Hrec; destruct Hrec as [sm [H3a H3b]]
+      end.
       exists sm.
       split; try assumption.
       eapply eval_step; eassumption.
-  - (* <- direction *)
+  - (* <- direction: induct on the derivation `eval p1 s sm` (robust; no
+       reliance on inversion-autogenerated hypothesis names, which broke
+       under Coq 8.20). *)
     intros [sm [H1 H2]].
-    generalize dependent s'.
-    generalize dependent sm.
-    generalize dependent s.
-    induction p1 as [| i p1' IH]; intros s sm s' H1 H2.
-    + (* p1 = [] *)
-      simpl.
-      inversion H1; subst.
-      assumption.
-    + (* p1 = i :: p1' *)
-      simpl.
-      inversion H1; subst.
-      eapply eval_step.
-      * eassumption.
-      * apply IH; eassumption.
+    revert s' H2.
+    induction H1 as [ s0 | i is s1 s2 s3 Hstep Hev IH ]; intros s' H2.
+    + (* eval_empty: p1 = [], s0 = sm *)
+      simpl. exact H2.
+    + (* eval_step: eval (i :: is) s1 s3 *)
+      simpl. eapply eval_step.
+      * exact Hstep.
+      * apply IH. exact H2.
 Qed.
 
 (** State equality is reflexive *)
@@ -297,16 +302,19 @@ Proof.
   intros s.
   unfold state_eq.
   repeat split; try reflexivity.
-  unfold mem_eq. reflexivity.
+  (* Coq 8.20: `reflexivity` already discharges the mem_eq goal (function
+     equality), so the old explicit `unfold mem_eq. reflexivity.` now raises
+     "No such goal". Make the finisher no-op-safe across Coq versions. *)
+  all: try (unfold mem_eq; reflexivity).
 Qed.
 
 (** State equality is transitive *)
 Lemma state_eq_trans :
   forall s1 s2 s3, s1 =st= s2 -> s2 =st= s3 -> s1 =st= s3.
 Proof.
-  intros s1 s2 s3 [Hm1 [Hr1 [Hi1 Hp1]]] [Hm2 [Hr2 [Hi2 Hp2]]].
-  unfold state_eq.
-  repeat split.
+  intros s1 s2 s3 [Hm1 [Hr1 Hi1]] [Hm2 [Hr2 Hi2]].
+  unfold state_eq in *.
+  split; [ | split ].
   - (* Memory *)
     unfold mem_eq in *.
     intros addr.
@@ -315,8 +323,6 @@ Proof.
     transitivity (s2.(state_registers)); auto.
   - (* I/O *)
     transitivity (s2.(state_io)); auto.
-  - (* PC *)
-    transitivity (s2.(state_pc)); auto.
 Qed.
 
 (** Purity is transitive *)
@@ -342,30 +348,29 @@ Proof.
   unfold is_CNO in *.
   destruct H1 as [T1 [I1 [P1 R1]]].
   destruct H2 as [T2 [I2 [P2 R2]]].
-  repeat split.
+  (* Robust: explicit nested split (not `repeat split`, which mis-structured
+     the 4-way is_CNO conjunction under Coq 8.20), seq_comp unfolded up front,
+     and fresh intro names (`s0`) that cannot clash with earlier hypotheses. *)
+  unfold seq_comp in *.
+  split; [ | split; [ | split ] ].
   - (* Termination *)
-    intros s.
+    intros s0.
     unfold terminates in *.
-    destruct (T1 s) as [s1 E1].
+    destruct (T1 s0) as [s1 E1].
     destruct (T2 s1) as [s2 E2].
     exists s2.
-    unfold seq_comp.
     apply eval_app.
     exists s1.
     split; assumption.
   - (* Identity *)
-    intros s s' Heval.
-    unfold seq_comp in Heval.
+    intros s0 s' Heval.
     apply eval_app in Heval.
     destruct Heval as [sm [E1 E2]].
-    (* p1 maps s to itself, so sm = s *)
-    (* p2 maps sm to itself, so s' = sm = s *)
     apply I1 in E1.
     apply I2 in E2.
     eapply state_eq_trans; eassumption.
   - (* Purity *)
-    intros s s' Heval.
-    unfold seq_comp in Heval.
+    intros s0 s' Heval.
     apply eval_app in Heval.
     destruct Heval as [sm [E1 E2]].
     apply P1 in E1.
@@ -383,23 +388,18 @@ Qed.
 Theorem empty_is_cno : is_CNO [].
 Proof.
   unfold is_CNO.
-  repeat split.
+  split; [ | split; [ | split ] ].
   - (* Termination *)
-    intros s.
-    exists s.
-    constructor.
-  - (* Identity *)
-    intros s s' Heval.
+    intros s0. exists s0. constructor.
+  - (* Identity: eval [] s0 s' forces s' = s0, so reuse state_eq_refl *)
+    intros s0 s' Heval.
     inversion Heval; subst.
-    unfold state_eq.
-    repeat split; try reflexivity.
-    unfold mem_eq. reflexivity.
+    apply state_eq_refl.
   - (* Purity *)
-    intros s s' Heval.
+    intros s0 s' Heval.
     inversion Heval; subst.
-    unfold pure, no_io, no_memory_alloc.
-    split; try reflexivity.
-    unfold mem_eq. reflexivity.
+    unfold pure, no_io, no_memory_alloc, mem_eq.
+    split; [ reflexivity | intros addr; reflexivity ].
   - (* Thermodynamic reversibility *)
     unfold thermodynamically_reversible.
     intros s1 s2 Heval.
@@ -412,27 +412,30 @@ Qed.
 Theorem nop_is_cno : is_CNO [Nop].
 Proof.
   unfold is_CNO.
-  repeat split.
+  (* Robust: explicit nested split, fresh names, and inversion hypotheses
+     grabbed by shape (match goal) so Coq-version autonaming can't break it.
+     With PC excluded from state_eq, [Nop] is genuinely a CNO. *)
+  split; [ | split; [ | split ] ].
   - (* Termination *)
-    intros s.
-    exists (mkState s.(state_memory) s.(state_registers) s.(state_io) (S s.(state_pc))).
-    apply eval_step with (s2 := mkState s.(state_memory) s.(state_registers) s.(state_io) (S s.(state_pc))).
-    + constructor.
-    + constructor.
-  - (* Identity - modulo PC increment *)
-    intros s s' Heval.
+    intros s0.
+    eexists.
+    eapply eval_step.
+    + apply step_nop.
+    + apply eval_empty.
+  - (* Identity *)
+    intros s0 s' Heval.
     inversion Heval; subst.
-    inversion H; subst.
-    inversion H0; subst.
-    unfold state_eq.
-    repeat split; try reflexivity.
-    unfold mem_eq. reflexivity.
+    match goal with H : step _ Nop _ |- _ => inversion H; subst end.
+    match goal with H : eval [] _ _ |- _ => inversion H; subst end.
+    unfold state_eq, mem_eq.
+    split; [ intros addr; reflexivity | split; reflexivity ].
   - (* Purity *)
-    intros s s' Heval.
+    intros s0 s' Heval.
     inversion Heval; subst.
-    inversion H; subst.
-    unfold pure, no_io, no_memory_alloc.
-    split; reflexivity.
+    match goal with H : step _ Nop _ |- _ => inversion H; subst end.
+    match goal with H : eval [] _ _ |- _ => inversion H; subst end.
+    unfold pure, no_io, no_memory_alloc, mem_eq.
+    split; [ reflexivity | intros addr; reflexivity ].
   - (* Thermodynamic reversibility *)
     unfold thermodynamically_reversible.
     intros s1 s2 Heval.
@@ -469,17 +472,26 @@ Theorem cno_equiv_sym : forall p1 p2, cno_equiv p1 p2 -> cno_equiv p2 p1.
 Proof.
   unfold cno_equiv.
   intros p1 p2 H s s1 s2 H1 H2.
-  symmetry.
-  apply H; assumption.
+  (* `symmetry` needs a registered Symmetric instance for =st= (none), and
+     state_eq_sym is defined later in this file. Derive s2 =st= s1 from H
+     and flip each observable component by hand. *)
+  destruct (H s s2 s1 H2 H1) as [Hm [Hr Hi]].
+  unfold state_eq, mem_eq in *.
+  split; [ | split ].
+  - intros addr; symmetry; apply Hm.
+  - symmetry; exact Hr.
+  - symmetry; exact Hi.
 Qed.
 
 (** State equality is symmetric *)
 Lemma state_eq_sym : forall s1 s2, s1 =st= s2 -> s2 =st= s1.
 Proof.
-  intros s1 s2 [Hm [Hr [Hi Hp]]].
+  intros s1 s2 [Hm [Hr Hi]].
   unfold state_eq, mem_eq in *.
-  repeat split; auto.
-  intros addr. symmetry. apply Hm.
+  split; [ | split ].
+  - intros addr. symmetry. apply Hm.
+  - symmetry. exact Hr.
+  - symmetry. exact Hi.
 Qed.
 
 Theorem cno_equiv_trans :
@@ -613,13 +625,13 @@ Lemma cno_eval_on_equal_states :
 Proof.
   intros p s s' H_cno H_eq.
   split; intros [sx H_eval].
-  - (* Forward direction *)
-    exists s'.
+  - (* Forward: eval p s sx  and  s =st= s'  ==>  eval p s' sx *)
+    exists sx.
     eapply eval_respects_state_eq_left.
     + eassumption.
     + assumption.
-  - (* Backward direction *)
-    exists s.
+  - (* Backward: eval p s' sx  and  s =st= s'  ==>  eval p s sx *)
+    exists sx.
     eapply eval_respects_state_eq_left.
     + eassumption.
     + apply state_eq_sym. assumption.