proof(coq): discharge eval_respects_state_eq_{left,right} via deletion + downstream refactor (#31)

Audit of the remaining ~120 Axiom/Parameter declarations after PR #24
identified TWO genuinely unsound axioms (the rest are legitimate
model-layer assumptions about abstract Parameters — physics constants,
quantum gate primitives, POSIX semantics, Y combinator non-termination,
the intentionally-typed hom_functor).

The unsound pair:

    Axiom eval_respects_state_eq_right :
      forall p s s' s'', eval p s s' -> s' =st= s'' -> eval p s s''.

    Axiom eval_respects_state_eq_left :
      forall p s s' s'', eval p s' s'' -> s =st= s' -> eval p s s''.

These cannot hold under the rescue branch's PC-excluding [state_eq]
(memory + registers + I/O — see ADR-006): two states can be [=st=] yet
carry different [state_pc], while [eval] deterministically propagates
PC through every step constructor. The axiomatised conclusion would
force a syntactically-identical eval result, which is impossible
without coincidental PC match. The TODO comment in CNO.v acknowledged
"prove this axiom by induction on eval structure" — a proof attempt
hits the PC mismatch and fails.

This commit *deletes* both axioms outright and refactors the only two
consumers:

- [cno_eval_on_equal_states] (CNO.v, line ~662) — previously chose the
  same existential witness for both forward and backward directions,
  needing [eval_respects_state_eq_left]. The lemma states a
  termination *iff*; different witnesses suffice. Re-proved using
  [cno_terminates] alone (witnesses from is_CNO p, no axiom).
  `Print Assumptions cno_eval_on_equal_states.` →
  "Closed under the global context".

- [cno_logically_reversible] (StatMech.v, line ~296) — previously
  produced [eval p s' s] from [eval p s' s''] + [s'' =st= s] via
  [eval_respects_state_eq_right]. Cannot hold; reflects the dual
  unsoundness. Resolved by weakening the *definition* of
  [logically_reversible] to observational reversibility:

      Definition logically_reversible (p : Program) : Prop :=
        exists p_inv,
          forall s s', eval p s s' ->
            exists s'', eval p_inv s' s'' /\ s'' =st= s.

  This is the level at which thermodynamic reversibility actually
  holds: memory + registers + I/O are the bits of physical record;
  the PC is bookkeeping. No theory is lost — the only theorem citing
  the strong [logically_reversible] form is
  [bennett_logical_implies_thermodynamic], whose proof body never
  uses its hypothesis (explicit "the logically_reversible hypothesis
  is not used" comment in the source). `Print Assumptions
  cno_logically_reversible.` → "Closed under the global context".

Verification (build-is-oracle):
- `coqc -R common CNO common/CNO.v` exit 0 (Coq 8.18.0).
- All 11 Coq files under proofs/coq/{common,quantum,lambda,physics,
  malbolge,category,filesystem} recompile clean.
- `Print Assumptions {cno_eval_on_equal_states, cno_logically_reversible,
  bennett_logical_implies_thermodynamic}` — first two report "Closed
  under the global context"; the third reports only the abstract
  Parameter [shannon_entropy] (legitimate model layer, not a proof
  escape).

Net effect on the axiom ledger: 75 → 73 Axioms (deleted 2, no
replacement). 42 Parameters unchanged.

Docs reconciled in the same commit:
- PROOF-STATUS-2026-05-18.md: post-T0 audit table refreshed; 3
  discharges shipped (eval_deterministic + the 2 unsound ones);
  remainder classified as legitimate model-layer assumptions.
- .machine_readable/6a2/STATE.a2ml: components.coq-proofs note
  rebuilt; session-history prepended.
- .machine_readable/6a2/META.a2ml + META.scm: ADR-008 added recording
  the deletion + refactor + rationale.

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