Equation (6.2)The total OR-of-XORs extension equals Δ's bit on single-change pairs; not a character for N≥2; degree two for N=1

207theorem dSign_enc_real {B N q : ℕ} {Q Q' : List ℕ} (hQ : Q.length = N) (hQ' : Q'.length = N)208    (hw : Game.Width B Q) (hw' : Game.Width B Q') (h1 : LocalRestore.OneChange Q Q') :209    (dSign B N q (enc B N Q Q') : ℝ) = sg ((nimSum Q ^^^ nimSum Q').testBit q) :=210  dSign_enc hQ hQ' hw hw' h1

198theorem dC_not_character_real {B N q : ℕ} (hN : 2 ≤ N) (hq : q < B) :199    ¬ ∃ (S : List Bool) (c : ℝ), c * c = 1 ∧ ∀ z ∈ bitvecs (2 * (B * N)), dSign B N q z = c * chi S z :=200  dC_not_character hN hq

217theorem dC_one_exactDeg_real {B q : ℕ} (hq : q < B) : ExactDeg (2 * (B * 1)) (dSign (R := ℝ) B 1 q) 2 :=218  dC_one_exactDeg hq

723/-- B3 (MAIN): for N ≥ 2 and q < B the sign encoding of dC B N q on the FULL 2BN-bit cube is724    not ±χ_S for ANY mask S (of any degree). -/725theorem dC_not_character {B N q : Nat} (hN : 2 ≤ N) (hq : q < B) :726    ¬ ∃ (S : List Bool) (c : R), c * c = 1 ∧ ∀ z ∈ bitvecs (2 * (B * N)), dSign B N q z = c * chi S z := by727  rintro ⟨S, c, hc, hf⟩728  obtain ⟨p, hp⟩ : ∃ p, p = B - 1 - q := ⟨_, rfl⟩729  have hBN : 2 * B ≤ B * N := by730    have := Nat.mul_le_mul_left B hN; rw [Nat.mul_comm B 2] at this; exact this731  have hB : 1 ≤ B := by omega732  have hpB : p < B := by omega733  have ha : p < 2 * (B * N) := by omega734  have hb : B + p < 2 * (B * N) := by omega735  have m0 : List.replicate (2 * (B * N)) false ∈ bitvecs (2 * (B * N)) := mem_bitvecs_of_length (by simp)736  have m1 := pt_mem (2 * (B * N)) p737  have m2 := pt_mem (2 * (B * N)) (B + p)738  have m12 := twoMask_mem (2 * (B * N)) p (B + p)739  -- values of dSign at the four points740  have v0 : (dSign B N q (List.replicate (2 * (B * N)) false) : R) = 1 := by741    unfold dSign742    rw [eval_dC_any hq hp]743    have : (List.range N).any (fun i => xor (vfun (List.replicate (2 * (B * N)) false) (B * i + p))744        (vfun (List.replicate (2 * (B * N)) false) (B * N + (B * i + p)))) = false := by745      simp only [vfun, getD_replicate_false, Bool.xor_false, List.any_eq_false]; simp746    rw [this]; rfl747  have v1 : (dSign B N q (pt (2 * (B * N)) p) : R) = -1 := by748    apply dSign_true hq hp (i := 0) (by omega)749    rw [pt_getD, pt_getD]750    have e1 : decide (B * 0 + p = p) = true := by simp751    have e2 : decide (B * 0 + p < 2 * (B * N)) = true := by simp; omega752    have e3 : decide (B * N + (B * 0 + p) = p) = false := by simp; omega753    rw [e1, e2, e3]; rfl754  have v2 : (dSign B N q (pt (2 * (B * N)) (B + p)) : R) = -1 := by755    apply dSign_true hq hp (i := 1) (by omega)756    rw [pt_getD, pt_getD]757    have e1 : decide (B * 1 + p = B + p) = true := by simp758    have e2 : decide (B * 1 + p < 2 * (B * N)) = true := by simp; omega759    have e3 : decide (B * N + (B * 1 + p) = B + p) = false := by simp; omega760    rw [e1, e2, e3]; rfl761  have v12 : (dSign B N q (twoMask (2 * (B * N)) p (B + p)) : R) = -1 := by762    apply dSign_true hq hp (i := 0) (by omega)763    rw [twoMask_getD, twoMask_getD]764    have e1 : decide (B * 0 + p = p) = true := by simp765    have e2 : decide (B * 0 + p < 2 * (B * N)) = true := by simp; omega766    have e3 : decide (B * 0 + p = B + p) = false := by simp; omega767    have e4 : decide (B * N + (B * 0 + p) = p) = false := by simp; omega768    have e5 : decide (B * N + (B * 0 + p) = B + p) = false := by simp; omega769    rw [e1, e2, e3, e4, e5]; rfl770  have c0 := hf _ m0771  have c1 := hf _ m1772  have c2 := hf _ m2773  have c12 := hf _ m12774  have hmul : (chi S (twoMask (2 * (B * N)) p (B + p)) : R) = chi S (pt (2 * (B * N)) p) * chi S (pt (2 * (B * N)) (B + p)) :=775    (chi_mul_right S (by simp [pt])).symm776  rw [chi_zeros, v0] at c0777  rw [v1] at c1; rw [v2] at c2; rw [v12, hmul] at c12778  -- 1 = c, −1 = c χ₁, −1 = c χ₂, −1 = c χ₁ χ₂  ⇒  −1 = 1779  have hc1 : c = 1 := by grind780  subst hc1781  have : (-1 : R) = 1 := by grind782  exact one_ne_neg_one this.symm

977/-- EXISTENCE: the global parity character (degree 2N) agrees with the delta bit on EVERY978    encoded pair of B-bit boards (no promise needed). -/979theorem gMask_delta {B N q : Nat} (hq : q < B) {Q Q' : List Nat} (hQ : Q.length = N) (hQ' : Q'.length = N)980    (hw : Game.Width B Q) (hw' : Game.Width B Q') :981    (chi (gMask B N q) (enc B N Q Q') : R) = sg ((nimSum Q ^^^ nimSum Q').testBit q) := by982  unfold chi gMask983  rw [enc_split, pm_append (by rw [length_maskU, frame_length]),984    ← (Misc.nimsum_bit_character hq (frame_mem B N Q)).1, ← (Misc.nimsum_bit_character hq (frame_mem B N Q')).1,985    decode_frame hQ hw, decode_frame hQ' hw', Nat.testBit_xor]

1121/-- UNIQUENESS: a character that agrees with the delta bit q on every single-change pair of1122    B-bit boards is the global parity character.  So, for N ≥ 2, no character of degree1123    less than 2N (in particular no degree-two character) agrees with the delta map on the1124    promised single-change domain; the local circuit dC is a different total extension,1125    and is not a character at all (dC_not_character). -/1126theorem char_unique {B N q : Nat} (hq : q < B) {S : List Bool} (hS : S ∈ bitvecs (2 * (B * N)))1127    (h : ∀ Q Q', Q.length = N → Q'.length = N → Game.Width B Q → Game.Width B Q' → LocalRestore.OneChange Q Q' →1128      (chi S (enc B N Q Q') : R) = sg ((nimSum Q ^^^ nimSum Q').testBit q)) :1129    S = gMask B N q := by1130  have hSl := mem_bitvecs_length hS1131  have hB : 0 < B := by omega1132  apply mask_ext hS (gMask_mem B N q)1133  intro a ha1134  by_cases ha1 : a < B * N1135  · -- first frame: the pair (unit board, empty board)1136    have hi : a / B < N := by rw [Nat.div_lt_iff_lt_mul hB, Nat.mul_comm]; exact ha11137    have hm : a % B < B := Nat.mod_lt _ hB1138    have hr : B - 1 - a % B < B := by omega1139    have hpos : a = B * (a / B) + (B - 1 - (B - 1 - a % B)) := by1140      have := Nat.div_add_mod a B; omega1141    obtain ⟨pre, post, h0, h1⟩ := unitBoard_split hi (B - 1 - a % B)1142    have hc := h (unitBoard N (a / B) (B - 1 - a % B)) (List.replicate N 0) (unitBoard_length _ _ _) (by simp)1143      (unitBoard_width hr) (zero_width B N) (Or.inr ⟨pre, 2 ^ (B - 1 - a % B), post, 0, h1, h0⟩)1144    rw [enc_unit_left hi hr, h1, h0, LocalRestore.delta_oneChange, ← hpos] at hc1145    unfold chi at hc1146    rw [pm_pt_left hSl ha] at hc1147    have e1 := sg_inj hc1148    rw [e1, Nat.xor_zero, Nat.testBit_two_pow]1149    unfold gMask1150    rw [List.getD_eq_getElem?_getD, List.getElem?_append_left (by rw [length_maskU]; exact ha1),1151      ← List.getD_eq_getElem?_getD]1152    conv => rhs; rw [show a = B * (a / B) + a % B from (Nat.div_add_mod a B).symm]1153    rw [maskU_getD (2 ^ q) hm N (a / B) hi, Nat.testBit_two_pow]1154    simp only [decide_eq_decide]; omega1155  · -- second frame: the pair (empty board, unit board)1156    have hb : a - B * N < B * N := by omega1157    have hi : (a - B * N) / B < N := by rw [Nat.div_lt_iff_lt_mul hB, Nat.mul_comm N B]; exact hb1158    have hm : (a - B * N) % B < B := Nat.mod_lt _ hB1159    have hr : B - 1 - (a - B * N) % B < B := by omega1160    have hpos : a = B * N + (B * ((a - B * N) / B) + (B - 1 - (B - 1 - (a - B * N) % B))) := by1161      have := Nat.div_add_mod (a - B * N) B; omega1162    obtain ⟨pre, post, h0, h1⟩ := unitBoard_split hi (B - 1 - (a - B * N) % B)1163    have hc := h (List.replicate N 0) (unitBoard N ((a - B * N) / B) (B - 1 - (a - B * N) % B)) (by simp)1164      (unitBoard_length _ _ _) (zero_width B N) (unitBoard_width hr) (Or.inr ⟨pre, 0, post, _, h0, h1⟩)1165    rw [enc_unit_right hi hr, h1, h0, LocalRestore.delta_oneChange, ← hpos] at hc1166    unfold chi at hc1167    rw [pm_pt_left hSl ha] at hc1168    have e1 := sg_inj hc1169    rw [e1, Nat.zero_xor, Nat.testBit_two_pow]1170    unfold gMask1171    rw [List.getD_eq_getElem?_getD, List.getElem?_append_right (by rw [length_maskU]; omega), length_maskU,1172      ← List.getD_eq_getElem?_getD]1173    conv => rhs; rw [show a - B * N = B * ((a - B * N) / B) + (a - B * N) % B from (Nat.div_add_mod _ B).symm]1174    rw [maskU_getD (2 ^ q) hm N _ hi, Nat.testBit_two_pow]1175    simp only [decide_eq_decide]; omega

1210/-- COROLLARY: for N ≥ 2 no character of degree two (indeed of degree < 2N) agrees with the1211    delta bit on the promised single-change domain, while the global character of degree1212    2N does. -/1213theorem no_low_degree_extension {B N q : Nat} (hq : q < B) {S : List Bool} (hS : S ∈ bitvecs (2 * (B * N)))1214    (hdeg : ones S < 2 * N)1215    (h : ∀ Q Q', Q.length = N → Q'.length = N → Game.Width B Q → Game.Width B Q' → LocalRestore.OneChange Q Q' →1216      (chi S (enc B N Q Q') : R) = sg ((nimSum Q ^^^ nimSum Q').testBit q)) : False := by1217  have := char_unique hq hS h1218  rw [this, ones_gMask hq] at hdeg; omega