Fourier

Comment and keyword shading is a reading aid only. It is not a verification marker; the evidence is the build record on the Build page.

1import NoiseModel23/- Phase 8, part B: Fourier analysis on the Boolean cube, tails, the parity spectrum, and the4   unknown-index delta.  Written by Claude (10 October 2026).  Lean 4.26.0, core/Std only.56   Paper target: Section sec:spectral-view (Walsh–Hadamard characters, Fourier coefficients,7   inversion, the Fourier tail and (k, ε)-band-limited functions, parity as a pure8   character, nim-sum bits and delta bits).  Everything is proved for an arbitrary linearly9   ordered field R (Lean core's interface, as in NoiseModel); RealFourier.lean instantiates10   the results at Mathlib's ℝ.1112   B1  The cube {0,1}^n is `bitvecs n` (no duplicates, exactly the lists of length n,13       2^n elements); characters are indexed by masks S ∈ bitvecs n (S ↔ the subset14       {i : S_i = 1}, a bijection, `mask_ext`/`ofPred_mem`).  χ_S(x) = (−1)^{|S ∩ x|}.15       Normalised inner product ⟨f,g⟩ = 2^{−n} Σ_x f(x)g(x) (uniform distribution),16       coefficients f̂(S) = ⟨f, χ_S⟩.  Orthonormality, inversion f = Σ_S f̂(S)χ_S for EVERY17       f on the cube, uniqueness of the expansion, Parseval, all n including n = 0;18       agreement with Misc.char_orth at ℚ.19   B2  |S| = number of ones; Tail_{>k}(f) = Σ_{|S|>k} f̂(S)²; (k, ε)-band-limited;20       exact degree.  χ_S has coefficient 1 at S and 0 elsewhere, exact degree |S|, tail21       1 below |S| and 0 from |S| on.  Nim-sum bit j is the character of a mask with N ones;22       the fixed-heap delta bit is a two-coordinate character.  Coefficient-versus-tail and23       sign-versus-indicator conventions; the classical spectral-tail theorem enters only24       as the named premise `TailPremise` (not proved, not assumed anywhere else).25   B3  The unknown-index delta, via the implemented total circuit LocalRestore.dC B N q26       on the FULL 2BN-bit cube: it agrees with the delta bit on every single-change27       transition, equals the two-coordinate character of heap i on transitions that28       change heap i, and for N ≥ 2, q < B its sign encoding is NOT ±(any character) and29       has at least two nonzero Fourier coefficients.  N = 1: it IS the two-coordinate30       character; N = 0 or q ≥ B: it is the constant character.  No claim is made about31       other total extensions of the promised-domain map. -/3233namespace NimAudit34namespace Fourier3536set_option linter.unusedSectionVars false3738open Lean.Grind Std Bridge Noise AC0 AC0.Circ3940/-! ## Boolean facts about masked parity (no field needed) -/4142theorem pm_comm : ∀ (S x : List Bool), S.length = x.length → pm S x = pm x S43  | [], [], _ => rfl44  | s :: S, b :: x, h => by45    simp only [pm]; rw [pm_comm S x (by simpa using h), Bool.and_comm]46  | [], _ :: _, h => by simp at h47  | _ :: _, [], h => by simp at h4849theorem pm_xor_right : ∀ (S x y : List Bool), x.length = y.length →50    pm S (List.zipWith xor x y) = xor (pm S x) (pm S y)51  | [], _, _, _ => by simp [pm]52  | _ :: _, [], [], _ => by simp [pm]53  | s :: S, b :: x, c :: y, h => by54    simp only [List.zipWith_cons_cons, pm]55    rw [pm_xor_right S x y (by simpa using h)]56    cases s <;> cases b <;> cases c <;> cases pm S x <;> cases pm S y <;> rfl57  | _ :: _, [], _ :: _, h => by simp at h58  | _ :: _, _ :: _, [], h => by simp at h5960theorem pm_of_false : ∀ (S x : List Bool), (∀ s ∈ S, s = false) → pm S x = false61  | [], _, _ => rfl62  | _ :: _, [], _ => rfl63  | s :: S, b :: x, h => by64    simp only [pm]65    rw [h s (by simp), pm_of_false S x (fun t ht => h t (by simp [ht]))]; rfl6667theorem pm_zeros_right : ∀ (S : List Bool) (n : Nat), pm S (List.replicate n false) = false68  | [], _ => rfl69  | _ :: _, 0 => rfl70  | s :: S, n + 1 => by71    simp only [List.replicate_succ, pm, Bool.and_false, Bool.false_xor]; exact pm_zeros_right S n7273/-- Number of coordinates selected by S at which x is 1, i.e. |S ∩ supp x|. -/74def selCount : List Bool → List Bool → Nat75  | m :: ms, b :: bs => (if m && b then 1 else 0) + selCount ms bs76  | _, _ => 07778theorem pm_selCount : ∀ (S x : List Bool), pm S x = decide (selCount S x % 2 = 1)79  | [], _ => by simp [pm, selCount]80  | _ :: _, [] => by simp [pm, selCount]81  | m :: ms, b :: bs => by82    simp only [pm, selCount]83    rw [pm_selCount ms bs]84    cases m <;> cases b <;> by_cases h : selCount ms bs % 2 = 1 <;> simp [h] <;> omega8586/-! ### Masks as subsets: the character index set -/8788theorem cube_mem {n : Nat} {x : List Bool} : x ∈ bitvecs n ↔ x.length = n :=89  ⟨mem_bitvecs_length, mem_bitvecs_of_length⟩9091theorem nodup_map_cons (b : Bool) : ∀ l : List (List Bool), l.Nodup → (l.map (b :: ·)).Nodup92  | [], _ => by simp93  | a :: l, h => by94    rw [List.nodup_cons] at h95    rw [List.map_cons, List.nodup_cons]96    refine ⟨fun hm => ?_, nodup_map_cons b l h.2⟩97    obtain ⟨x, hx, e⟩ := List.mem_map.1 hm98    injection e with _ e299    exact h.1 (e2 ▸ hx)100101theorem cube_nodup : ∀ n, (bitvecs n).Nodup102  | 0 => by simp [bitvecs]103  | n + 1 => by104    simp only [bitvecs]105    rw [List.nodup_append]106    refine ⟨?_, ?_, ?_⟩107    · exact nodup_map_cons false _ (cube_nodup n)108    · exact nodup_map_cons true _ (cube_nodup n)109    · intro a ha b hb hab110      simp only [List.mem_map] at ha hb111      obtain ⟨u, _, rfl⟩ := ha112      obtain ⟨v, _, rfl⟩ := hb113      simp at hab114115theorem cube_card (n : Nat) : (bitvecs n).length = 2 ^ n := length_bitvecs n116117/-- The mask of a subset given by its characteristic predicate on [n]. -/118def ofPred (n : Nat) (A : Nat → Bool) : List Bool := (List.range n).map A119120theorem ofPred_mem (n : Nat) (A : Nat → Bool) : ofPred n A ∈ bitvecs n :=121  cube_mem.2 (by simp [ofPred])122123theorem ofPred_getD (n : Nat) (A : Nat → Bool) (j : Nat) :124    (ofPred n A).getD j false = (decide (j < n) && A j) := by125  simp only [ofPred, List.getD_eq_getElem?_getD, List.getElem?_map, List.getElem?_range]126  by_cases h : j < n <;> simp [h]127128/-- Masks are determined by their membership predicate (no duplicate indices). -/129theorem mask_ext {n : Nat} {S T : List Bool} (hS : S ∈ bitvecs n) (hT : T ∈ bitvecs n)130    (h : ∀ j, j < n → S.getD j false = T.getD j false) : S = T := by131  have hl1 := mem_bitvecs_length hS132  have hl2 := mem_bitvecs_length hT133  apply List.ext_getElem (by omega)134  intro j h1 h2135  have := h j (by omega)136  simp only [List.getD_eq_getElem?_getD, List.getElem?_eq_getElem h1, List.getElem?_eq_getElem h2,137    Option.getD_some] at this138  exact this139140/-- Every subset of [n] has its mask (no missing indices). -/141theorem mask_of_subset (n : Nat) (A : Nat → Bool) :142    ∃ S ∈ bitvecs n, ∀ j, j < n → S.getD j false = A j :=143  ⟨ofPred n A, ofPred_mem n A, fun j hj => by rw [ofPred_getD]; simp [hj]⟩144145section Generic146147variable {R : Type} [Field R] [LE R] [LT R] [LawfulOrderLT R] [IsLinearOrder R] [OrderedRing R]148149attribute [local instance] Semiring.natCast150151/-! ## Elementary field facts -/152153theorem two_pos' : (0 : R) < 2 := by154  have := OrderedRing.zero_lt_one (R := R); grind155156theorem two_pow_pos'' : ∀ n : Nat, (0 : R) < 2 ^ n157  | 0 => by rw [Semiring.pow_zero]; exact OrderedRing.zero_lt_one158  | n + 1 => by rw [Semiring.pow_succ]; exact OrderedRing.mul_pos (two_pow_pos'' n) two_pos'159160theorem two_pow_ne (n : Nat) : (2 : R) ^ n ≠ 0 := fun h => by161  have := two_pow_pos'' (R := R) n; rw [h] at this; exact Preorder.lt_irrefl _ this162163theorem pow_mul_inv (n : Nat) : (2 : R) ^ n * ((2 : R) ^ n)⁻¹ = 1 := Field.mul_inv_cancel (two_pow_ne n)164165theorem one_ne_neg_one : (1 : R) ≠ -1 := by166  intro h; have := two_pos' (R := R); grind167168theorem sg_xor (a b : Bool) : (sg (xor a b) : R) = sg a * sg b := by169  cases a <;> cases b <;> simp only [sg, Bool.xor_false, Bool.xor_true, Bool.not_false, Bool.not_true,170    Bool.false_eq_true, if_true, if_false] <;> grind171172theorem sg_mul_self (b : Bool) : (sg b : R) * sg b = 1 := by173  cases b <;> simp only [sg, Bool.false_eq_true, if_true, if_false] <;> grind174175theorem gs_mul_right {α : Type} (l : List α) (c : R) (f : α → R) :176    gs l (fun a => f a * c) = gs l f * c := by177  rw [show (fun a => f a * c) = (fun a => c * f a) by funext a; grind, gs_mul_left]; grind178179theorem gs_count (n : Nat) : gs (bitvecs n) (fun _ => (1 : R)) = 2 ^ n := by180  induction n with181  | zero => simp only [bitvecs, gs_cons, gs_nil, Semiring.pow_zero]; grind182  | succ n ih => rw [gs_bitvecs_succ, ih, Semiring.pow_succ]; grind183184theorem gs_single_le {α : Type} {l : List α} {g : α → R} (h : ∀ a ∈ l, 0 ≤ g a) {x : α} (hx : x ∈ l) :185    g x ≤ gs l g := by186  induction l with187  | nil => simp at hx188  | cons a l ih =>189    simp only [gs_cons]190    have hrest : 0 ≤ gs l g := gs_nonneg (fun b hb => h b (by simp [hb]))191    rcases List.mem_cons.mp hx with rfl | hx192    · grind193    · have := ih (fun b hb => h b (by simp [hb])) hx194      have := h a (by simp); grind195196/-! ## B1. Characters, inner product, coefficients -/197198/-- The Walsh–Hadamard character χ_S(x) = (−1)^{⟨S,x⟩}. -/199def chi (S x : List Bool) : R := sg (pm S x)200201/-- χ_S(x) = (−1)^{Σ_{i∈S} x_i} (the paper's formula). -/202theorem chi_pow (S x : List Bool) : (chi S x : R) = (-1) ^ selCount S x := by203  unfold chi; rw [pm_selCount]204  generalize selCount S x = k205  induction k with206  | zero => simp [sg, Semiring.pow_zero]207  | succ k ih =>208    rw [Semiring.pow_succ, ← ih]209    by_cases h : k % 2 = 1210    · have : ¬ ((k + 1) % 2 = 1) := by omega211      simp only [sg, decide_eq_true_eq, h, this, if_true, if_false]; grind212    · have : (k + 1) % 2 = 1 := by omega213      simp only [sg, decide_eq_true_eq, h, this, if_true, if_false]; grind214215/-- Normalised inner product under the uniform distribution on {0,1}^n. -/216def ip (n : Nat) (f g : List Bool → R) : R := gs (bitvecs n) (fun x => f x * g x) * ((2 : R) ^ n)⁻¹217218/-- Fourier coefficient f̂(S) = E_x[f(x) χ_S(x)]. -/219def coef (n : Nat) (f : List Bool → R) (S : List Bool) : R := ip n f (chi S)220221theorem coef_congr {n : Nat} {f g : List Bool → R} (h : ∀ x ∈ bitvecs n, f x = g x) (S : List Bool) :222    coef n f S = coef n g S := by223  unfold coef ip; rw [gs_congr (fun x hx => by rw [h x hx])]224225theorem chi_mul_left {S T : List Bool} (h : S.length = T.length) (x : List Bool) :226    (chi S x : R) * chi T x = chi (List.zipWith xor S T) x := by227  unfold chi; rw [Misc.pm_zipWith S T x h, sg_xor]228229theorem chi_mul_right (S : List Bool) {x y : List Bool} (h : x.length = y.length) :230    (chi S x : R) * chi S y = chi S (List.zipWith xor x y) := by231  unfold chi; rw [pm_xor_right S x y h, sg_xor]232233theorem chi_zeros (S : List Bool) (n : Nat) : (chi S (List.replicate n false) : R) = 1 := by234  unfold chi; rw [pm_zeros_right]; simp [sg]235236/-- Character sums: Σ_x χ_U(x) = 2^n if U = 0 and 0 otherwise. -/237theorem char_sum_gen : ∀ U : List Bool,238    gs (bitvecs U.length) (fun x => (chi U x : R)) = if U.all (fun b => b == false) then (2 : R) ^ U.length else 0239  | [] => by simp only [List.length_nil, bitvecs, gs_cons, gs_nil, chi, pm, sg, List.all_nil,240      Bool.false_eq_true, if_false, if_true, Semiring.pow_zero]; grind241  | u :: U => by242    simp only [List.length_cons]243    rw [gs_bitvecs_succ]244    have ih := char_sum_gen U245    cases u246    · have e1 : ∀ v, (chi (false :: U) (false :: v) : R) = chi U v := by intro v; simp [chi, pm]247      have e2 : ∀ v, (chi (false :: U) (true :: v) : R) = chi U v := by intro v; simp [chi, pm]248      rw [gs_congr (fun v _ => e1 v), gs_congr (fun v _ => e2 v), ih]249      simp only [List.all_cons, beq_self_eq_true, Bool.true_and]250      split251      · rw [Semiring.pow_succ]; grind252      · grind253    · have e1 : ∀ v, (chi (true :: U) (false :: v) : R) = chi U v := by intro v; simp [chi, pm]254      have e2 : ∀ v, (chi (true :: U) (true :: v) : R) = (-1) * chi U v := by255        intro v; simp only [chi, pm, Bool.true_and]; rw [sg_xor]; simp only [sg, if_true]256      rw [gs_congr (fun v _ => e1 v), gs_congr (fun v _ => e2 v), gs_mul_left, ih]257      simp only [List.all_cons]258      simp only [show ((true == false) && U.all (fun b => b == false)) = false by rfl, Bool.false_eq_true, if_false]259      split <;> grind260261theorem zipWith_length_eq {S T : List Bool} (h : S.length = T.length) : (List.zipWith xor S T).length = S.length := by262  simp [h]263264/-- Unnormalised orthogonality. -/265theorem orth_sum {n : Nat} {S T : List Bool} (hS : S ∈ bitvecs n) (hT : T ∈ bitvecs n) :266    gs (bitvecs n) (fun x => (chi S x : R) * chi T x) = if S = T then (2 : R) ^ n else 0 := by267  have h1 := mem_bitvecs_length hS268  have h2 := mem_bitvecs_length hT269  have hl : S.length = T.length := by omega270  rw [gs_congr (fun x _ => chi_mul_left hl x)]271  have hs := char_sum_gen (R := R) (List.zipWith xor S T)272  rw [zipWith_length_eq hl, h1] at hs273  rw [hs]274  by_cases hST : S = T275  · rw [if_pos ((Misc.zipWith_xor_all_false S T hl).2 hST), if_pos hST]276  · rw [if_neg (fun h' => hST ((Misc.zipWith_xor_all_false S T hl).1 h')), if_neg hST]277278/-- B1. ORTHONORMALITY of the characters under the uniform distribution. -/279theorem orthonormal {n : Nat} {S T : List Bool} (hS : S ∈ bitvecs n) (hT : T ∈ bitvecs n) :280    ip n (chi S) (chi T) = (if S = T then 1 else 0 : R) := by281  unfold ip; rw [orth_sum hS hT]282  split283  · exact pow_mul_inv n284  · grind285286/-- Dual orthogonality: Σ_S χ_S(x) χ_S(y) = 2^n [x = y]. -/287theorem dual_sum {n : Nat} {x y : List Bool} (hx : x ∈ bitvecs n) (hy : y ∈ bitvecs n) :288    gs (bitvecs n) (fun S => (chi S x : R) * chi S y) = if x = y then (2 : R) ^ n else 0 := by289  have h1 := mem_bitvecs_length hx290  have h2 := mem_bitvecs_length hy291  have hl : x.length = y.length := by omega292  have e : ∀ S ∈ bitvecs n, (chi S x : R) * chi S y = chi (List.zipWith xor x y) S := by293    intro S hS294    have hS' := mem_bitvecs_length hS295    rw [chi_mul_right S hl]; unfold chi296    rw [pm_comm S _ (by rw [zipWith_length_eq hl]; omega)]297  rw [gs_congr e]298  have hs := char_sum_gen (R := R) (List.zipWith xor x y)299  rw [zipWith_length_eq hl, h1] at hs300  rw [hs]301  by_cases hxy : x = y302  · rw [if_pos ((Misc.zipWith_xor_all_false x y hl).2 hxy), if_pos hxy]303  · rw [if_neg (fun h' => hxy ((Misc.zipWith_xor_all_false x y hl).1 h')), if_neg hxy]304305/-- B1. FOURIER INVERSION (completeness): every f on the cube is the sum of its Fourier306    series, f(x) = Σ_S f̂(S) χ_S(x). -/307theorem inversion (n : Nat) (f : List Bool → R) {x : List Bool} (hx : x ∈ bitvecs n) :308    gs (bitvecs n) (fun S => coef n f S * chi S x) = f x := by309  have hlx := mem_bitvecs_length hx310  have e1 : ∀ S, coef n f S * chi S x =311      gs (bitvecs n) (fun y => (((2 : R) ^ n)⁻¹ * f y) * (chi S y * chi S x)) := by312    intro S313    unfold coef ip314    rw [show (fun y => (((2 : R) ^ n)⁻¹ * f y) * (chi S y * chi S x)) =315      (fun y => (f y * chi S y) * (((2 : R) ^ n)⁻¹ * chi S x)) by funext y; grind, gs_mul_right]316    grind317  rw [gs_congr (fun S _ => e1 S), gs_comm]318  have e2 : ∀ y ∈ bitvecs n, gs (bitvecs n) (fun S => (((2 : R) ^ n)⁻¹ * f y) * (chi S y * chi S x)) =319      Noise.ind (decide (x = y)) * (((2 : R) ^ n)⁻¹ * f y * 2 ^ n) := by320    intro y hy321    rw [gs_mul_left, dual_sum hy hx]322    by_cases hxy : x = y323    · subst hxy; simp only [if_true, decide_true, Noise.ind]; grind324    · rw [if_neg (fun h => hxy h.symm)]; simp only [decide_eq_true_eq, hxy, decide_false, Noise.ind,325        Bool.false_eq_true, if_false]; grind326  rw [gs_congr e2, gs_point n x hlx (fun y => ((2 : R) ^ n)⁻¹ * f y * 2 ^ n)]327  have := pow_mul_inv (R := R) n328  grind329330/-- B1. UNIQUENESS of the expansion: any coefficient family representing f on the cube is331    the family of Fourier coefficients. -/332theorem uniqueness (n : Nat) (f : List Bool → R) (c : List Bool → R)333    (h : ∀ x ∈ bitvecs n, f x = gs (bitvecs n) (fun T => c T * chi T x)) :334    ∀ S ∈ bitvecs n, coef n f S = c S := by335  intro S hS336  have hlS := mem_bitvecs_length hS337  unfold coef ip338  rw [gs_congr (fun x hx => by rw [h x hx])]339  have e1 : ∀ x, gs (bitvecs n) (fun T => c T * chi T x) * chi S x =340      gs (bitvecs n) (fun T => c T * (chi T x * chi S x)) := by341    intro x; rw [← gs_mul_right]; apply gs_congr; intro T _; grind342  rw [gs_congr (fun x _ => e1 x), gs_comm]343  have e2 : ∀ T ∈ bitvecs n, gs (bitvecs n) (fun x => c T * (chi T x * chi S x)) =344      Noise.ind (decide (S = T)) * (c T * 2 ^ n) := by345    intro T hT346    rw [gs_mul_left, orth_sum hT hS]347    by_cases hST : S = T348    · subst hST; simp only [if_true, decide_true, Noise.ind]; grind349    · rw [if_neg (fun h => hST h.symm)]; simp only [decide_eq_true_eq, hST, decide_false, Noise.ind,350        Bool.false_eq_true, if_false]; grind351  rw [gs_congr e2, gs_point n S hlS (fun T => c T * 2 ^ n)]352  have := pow_mul_inv (R := R) n353  grind354355/-- B1. PARSEVAL: ⟨f, g⟩ = Σ_S f̂(S) ĝ(S). -/356theorem parseval (n : Nat) (f g : List Bool → R) :357    ip n f g = gs (bitvecs n) (fun S => coef n f S * coef n g S) := by358  unfold ip359  rw [gs_congr (fun x hx => by rw [← inversion n g hx])]360  have e1 : ∀ x, f x * gs (bitvecs n) (fun S => coef n g S * chi S x) =361      gs (bitvecs n) (fun S => coef n g S * (f x * chi S x)) := by362    intro x; rw [← gs_mul_left]; apply gs_congr; intro S _; grind363  rw [gs_congr (fun x _ => e1 x), gs_comm, ← gs_mul_right]364  apply gs_congr; intro S _365  rw [gs_mul_left]; unfold coef ip; grind366367theorem plancherel (n : Nat) (f : List Bool → R) :368    ip n f f = gs (bitvecs n) (fun S => coef n f S ^ 2) := by369  rw [parseval]; apply gs_congr; intro S _; grind370371/-- n = 0: the cube is {[]}, χ_[] = 1 and f̂([]) = f([]). -/372theorem dim_zero (f : List Bool → R) : bitvecs 0 = [[]] ∧ coef 0 f [] = f [] := by373  refine ⟨rfl, ?_⟩374  simp only [coef, ip, bitvecs, gs_cons, gs_nil, chi, pm, sg, Bool.false_eq_true, if_false, Semiring.pow_zero]375  have := pow_mul_inv (R := R) 0376  rw [Semiring.pow_zero] at this; grind377378/-! ## B2. Degrees, tails, band-limited functions -/379380/-- Degree-> k Fourier tail Tail_{>k}(f) = Σ_{|S| > k} f̂(S)². -/381def tail (n : Nat) (f : List Bool → R) (k : Nat) : R :=382  gs (bitvecs n) (fun S => if k < ones S then coef n f S ^ 2 else 0)383384/-- (k, ε)-spectrally band-limited. -/385def BandLimited (n : Nat) (f : List Bool → R) (k : Nat) (ε : R) : Prop := tail n f k ≤ ε386387/-- Fourier degree at most k. -/388def DegLe (n : Nat) (f : List Bool → R) (k : Nat) : Prop := ∀ T ∈ bitvecs n, k < ones T → coef n f T = 0389390/-- Exact Fourier degree d. -/391def ExactDeg (n : Nat) (f : List Bool → R) (d : Nat) : Prop :=392  DegLe n f d ∧ ∃ T ∈ bitvecs n, ones T = d ∧ coef n f T ≠ 0393394theorem tail_nonneg (n : Nat) (f : List Bool → R) (k : Nat) : 0 ≤ tail n f k :=395  gs_nonneg (fun S _ => by split; exact OrderedRing.sq_nonneg; exact Std.le_refl _)396397theorem tail_congr {n : Nat} {f g : List Bool → R} (h : ∀ x ∈ bitvecs n, f x = g x) (k : Nat) :398    tail n f k = tail n g k := by399  unfold tail; apply gs_congr; intro S _; rw [coef_congr h]400401theorem exactDeg_unique {n : Nat} {f : List Bool → R} {d d' : Nat} (h : ExactDeg n f d) (h' : ExactDeg n f d') :402    d = d' := by403  obtain ⟨hd, T, hT, hTd, hne⟩ := h404  obtain ⟨hd', T', hT', hTd', hne'⟩ := h'405  have a : ¬ d < d' := fun hlt => hne' (hd T' hT' (by omega))406  have b : ¬ d' < d := fun hlt => hne (hd' T hT (by omega))407  omega408409theorem tail_of_degLe {n : Nat} {f : List Bool → R} {k : Nat} (h : DegLe n f k) : tail n f k = 0 := by410  unfold tail411  rw [gs_congr (fun S hS => by412    show (if k < ones S then coef n f S ^ 2 else 0) = (fun _ => (0 : R)) S413    split414    · next hk => rw [h S hS hk]; grind415    · rfl), gs_zero]416417/-- COEFFICIENT VERSUS TAIL: every coefficient above degree k is bounded by the tail. -/418theorem coef_sq_le_tail {n : Nat} (f : List Bool → R) {k : Nat} {S : List Bool} (hS : S ∈ bitvecs n)419    (hk : k < ones S) : coef n f S ^ 2 ≤ tail n f k := by420  have := gs_single_le (l := bitvecs n) (g := fun T => if k < ones T then coef n f T ^ 2 else 0)421    (fun T _ => by dsimp only; split; exact OrderedRing.sq_nonneg; exact Std.le_refl _) hS422  simp only [hk, if_true] at this423  exact this424425/-- A (k, ε)-band-limited function has squared correlation ≤ ε with every character of426    degree > k. -/427theorem bandLimited_corr {n : Nat} {f : List Bool → R} {k : Nat} {ε : R} (hb : BandLimited n f k ε)428    {S : List Bool} (hS : S ∈ bitvecs n) (hk : k < ones S) : ip n f (chi S) ^ 2 ≤ ε :=429  Std.le_trans (coef_sq_le_tail f hS hk) hb430431/-- ±1-valued functions have total Fourier mass 1. -/432theorem sign_mass (n : Nat) (f : List Bool → R) (h : ∀ x ∈ bitvecs n, f x * f x = 1) :433    gs (bitvecs n) (fun S => coef n f S ^ 2) = 1 := by434  rw [← plancherel]; unfold ip435  rw [gs_congr h, gs_count, pow_mul_inv]436437theorem tail_le_one (n : Nat) (f : List Bool → R) (h : ∀ x ∈ bitvecs n, f x * f x = 1) (k : Nat) :438    tail n f k ≤ 1 := by439  rw [← sign_mass n f h]440  apply gs_le; intro S _441  split442  · exact Std.le_refl _443  · exact OrderedRing.sq_nonneg444445/-- PARITY IS A PURE CHARACTER: the coefficient of χ_S is 1 at S and 0 elsewhere. -/446theorem coef_chi {n : Nat} {S T : List Bool} (hS : S ∈ bitvecs n) (hT : T ∈ bitvecs n) :447    coef n (chi S) T = (if T = S then 1 else 0 : R) := by448  unfold coef; rw [orthonormal hS hT]449  by_cases h : S = T450  · subst h; simp451  · rw [if_neg h, if_neg (fun e => h e.symm)]452453/-- … hence its tail is 1 below degree |S| and 0 from |S| on. -/454theorem tail_chi {n : Nat} {S : List Bool} (hS : S ∈ bitvecs n) (k : Nat) :455    tail n (chi S) k = (if k < ones S then 1 else 0 : R) := by456  unfold tail457  have hl := mem_bitvecs_length hS458  rw [gs_congr (fun T hT => by459    show (if k < ones T then coef n (chi S) T ^ 2 else 0) =460      Noise.ind (decide (S = T)) * (if k < ones T then (1 : R) else 0)461    rw [coef_chi hS hT]462    by_cases hTS : T = S463    · subst hTS; simp only [if_true, decide_true, Noise.ind]; split <;> grind464    · simp only [hTS, if_false, show decide (S = T) = false from decide_eq_false (fun e => hTS e.symm), Noise.ind,465        Bool.false_eq_true]; split <;> grind)]466  rw [gs_point n S hl (fun T => if k < ones T then (1 : R) else 0)]467468/-- … and its exact degree is |S|. -/469theorem chi_exactDeg {n : Nat} {S : List Bool} (hS : S ∈ bitvecs n) : ExactDeg n (chi (R := R) S) (ones S) := by470  refine ⟨fun T hT hk => ?_, S, hS, rfl, ?_⟩471  · rw [coef_chi hS hT, if_neg (fun e => by subst e; omega)]472  · rw [coef_chi hS hS, if_pos rfl]473    intro h; have := OrderedRing.zero_lt_one (R := R); rw [h] at this; exact Preorder.lt_irrefl _ this474475theorem bandLimited_chi {n : Nat} {S : List Bool} (hS : S ∈ bitvecs n) (k : Nat) (ε : R) :476    BandLimited n (chi S) k ε ↔ (if k < ones S then 1 else 0 : R) ≤ ε := by477  unfold BandLimited; rw [tail_chi hS]478479/-! ### Signed versus indicator conventions -/480481theorem sg_eq_ind (b : Bool) : (sg b : R) = 1 - 2 * Noise.ind b := by482  cases b <;> simp only [sg, Noise.ind, Bool.false_eq_true, if_true, if_false] <;> grind483484theorem coef_one {n : Nat} {S : List Bool} (hS : S ∈ bitvecs n) :485    coef n (fun _ => (1 : R)) S = if S.all (fun b => b == false) then 1 else 0 := by486  have hl := mem_bitvecs_length hS487  unfold coef ip488  rw [show (fun x => (1 : R) * chi S x) = (fun x => chi S x) by funext x; grind]489  have := char_sum_gen (R := R) S490  rw [hl] at this; rw [this]491  split492  · exact pow_mul_inv n493  · grind494495/-- SIGNED VERSUS INDICATOR: for a Boolean function g, the sign encoding (−1)^g and the496    0/1 indicator have coefficients related by f̂_sign(S) = [S = 0] − 2·f̂_ind(S); in497    particular f̂_sign(S) = −2·f̂_ind(S) for every nonempty S. -/498theorem sign_indicator (n : Nat) (g : List Bool → Bool) {S : List Bool} (hS : S ∈ bitvecs n) :499    coef n (fun x => (sg (g x) : R)) S =500      (if S.all (fun b => b == false) then 1 else 0) - 2 * coef n (fun x => (Noise.ind (g x) : R)) S := by501  rw [← coef_one hS]502  unfold coef ip503  rw [← gs_mul_right, ← gs_mul_right, ← gs_mul_right]504  rw [show (2 : R) * gs (bitvecs n) (fun x => Noise.ind (g x) * chi S x * ((2 : R) ^ n)⁻¹) =505      gs (bitvecs n) (fun x => 2 * (Noise.ind (g x) * chi S x * ((2 : R) ^ n)⁻¹)) by rw [gs_mul_left], ← gs_sub]506  apply gs_congr; intro x _; dsimp only; rw [sg_eq_ind]; grind507508theorem par_eq_pm : ∀ y : List Bool, par y = pm (List.replicate y.length true) y509  | [] => rfl510  | b :: y => by simp only [par, List.length_cons, List.replicate_succ, pm, Bool.true_and]; rw [par_eq_pm y]511512/-! ### The named external spectral-tail input (LMN / Tal type), as a premise only -/513514/-- NAMED EXTERNAL PREMISE (not proved here, not assumed by any other theorem): every515    formula of depth ≤ d and size ≤ M reading only inputs below n has degree-> k tail of its516    sign encoding at most η.  Classical results of Linial–Mansour–Nisan and Tal give such η. -/517def TailPremise (n d M k : Nat) (η : R) : Prop :=518  ∀ C : Circ, depth C ≤ d → size C ≤ M → maxInput C ≤ n → tail n (fun x => sg (eval (vfun x) C)) k ≤ η519520/-! ## B2. Nim-sum bits and delta bits as characters -/521522/-- Sign encoding of bit j of the nim-sum of the decoded board. -/523def nimBitSign (B N j : Nat) (x : List Bool) : R := sg ((nimSum (decodeBoard B N x)).testBit j)524525theorem maskU_mem (B N u : Nat) : maskU B N u ∈ bitvecs (B * N) :=526  mem_bitvecs_of_length (length_maskU B N u)527528theorem nimBitSign_chi {B N j : Nat} (hj : j < B) {x : List Bool} (hx : x ∈ bitvecs (B * N)) :529    (nimBitSign B N j x : R) = chi (maskU B N (2 ^ j)) x := by530  unfold nimBitSign chi; rw [(Misc.nimsum_bit_character hj hx).1]531532/-- NIM-SUM BIT j: Fourier coefficient 1 at the mask with exactly N ones (one per heap) and 0533    elsewhere; exact degree N; tail 1 below N and 0 from N on. -/534theorem nimBit_spectrum {B N j : Nat} (hj : j < B) :535    (∀ T ∈ bitvecs (B * N), coef (B * N) (nimBitSign (R := R) B N j) T = if T = maskU B N (2 ^ j) then 1 else 0) ∧536    ones (maskU B N (2 ^ j)) = N ∧537    ExactDeg (B * N) (nimBitSign (R := R) B N j) N ∧538    ∀ k, tail (B * N) (nimBitSign (R := R) B N j) k = if k < N then 1 else 0 := by539  have hc : ∀ x ∈ bitvecs (B * N), (nimBitSign B N j x : R) = chi (maskU B N (2 ^ j)) x :=540    fun x hx => nimBitSign_chi hj hx541  have hones : ones (maskU B N (2 ^ j)) = N := (Misc.nimsum_bit_character hj (x := maskU B N (2 ^ j))542    (maskU_mem B N _)).2543  refine ⟨fun T hT => by rw [coef_congr hc, coef_chi (maskU_mem B N _) hT], hones, ?_, fun k => ?_⟩544  · have h := chi_exactDeg (R := R) (maskU_mem B N (2 ^ j))545    rw [hones] at h546    exact ⟨fun T hT hk => by rw [coef_congr hc]; exact h.1 T hT hk,547      let ⟨T, hT, h1, h2⟩ := h.2; ⟨T, hT, h1, by rw [coef_congr hc]; exact h2⟩⟩548  · rw [tail_congr hc, tail_chi (maskU_mem B N _), hones]549550/-- A paper-specific application of the named tail premise, with the actual support size: a551    formula of depth ≤ d and size ≤ M reading the B·N board bits has squared correlation at552    most η with nim-sum bit j (a character of degree N), provided the premise holds at some553    k < N. -/554theorem nimBit_corr_of_tail {B N j d M k : Nat} {η : R} (hj : j < B) (hk : k < N)555    (hT : TailPremise (B * N) d M k η) (C : Circ) (hd : depth C ≤ d) (hs : size C ≤ M) (hm : maxInput C ≤ B * N) :556    ip (B * N) (fun x => sg (eval (vfun x) C)) (nimBitSign B N j) ^ 2 ≤ η := by557  have hc : ∀ x ∈ bitvecs (B * N), (nimBitSign B N j x : R) = chi (maskU B N (2 ^ j)) x :=558    fun x hx => nimBitSign_chi hj hx559  have e : ip (B * N) (fun x => sg (eval (vfun x) C)) (nimBitSign B N j) =560      coef (R := R) (B * N) (fun x => sg (eval (vfun x) C)) (maskU B N (2 ^ j)) := by561    unfold coef ip; apply congrArg (· * _); apply gs_congr; intro x hx; rw [hc x hx]562  rw [e]563  have hones := (Misc.nimsum_bit_character hj (x := maskU B N (2 ^ j)) (maskU_mem B N _)).2564  exact Std.le_trans (coef_sq_le_tail _ (maskU_mem B N _) (by rw [hones]; exact hk)) (hT C hd hs hm)565566/-- Sign of bit j of a ⊕ b, as a function of the two B-bit blocks (u, v) of a = old and567    b = new value of one heap. -/568def deltaSign (B j : Nat) (w : List Bool) : R := sg ((toNatBE (w.take B) ^^^ toNatBE (w.drop B)).testBit j)569570theorem decode_two (B : Nat) {w : List Bool} (hw : w ∈ bitvecs (B * 2)) :571    nimSum (decodeBoard B 2 w) = toNatBE (w.take B) ^^^ toNatBE (w.drop B) := by572  have hl := mem_bitvecs_length hw573  have : (w.drop B).take B = w.drop B := List.take_of_length_le (by rw [List.length_drop]; omega)574  simp only [decodeBoard, nimSum, this, Nat.xor_zero]575576/-- FIXED-HEAP DELTA BITS ARE TWO-COORDINATE CHARACTERS: on the 2B-bit cube of the changed577    heap's old and new blocks, the sign of delta bit j is χ of a mask with exactly two ones;578    its exact degree is 2.  With Misc.delta_bit_local this is the delta of every legal move579    that changes that heap. -/580theorem delta_spectrum {B j : Nat} (hj : j < B) :581    (∀ w ∈ bitvecs (B * 2), (deltaSign B j w : R) = chi (maskU B 2 (2 ^ j)) w) ∧582    ones (maskU B 2 (2 ^ j)) = 2 ∧ ExactDeg (B * 2) (deltaSign (R := R) B j) 2 := by583  have hc : ∀ w ∈ bitvecs (B * 2), (deltaSign B j w : R) = chi (maskU B 2 (2 ^ j)) w := by584    intro w hw585    have := nimBitSign_chi (R := R) (N := 2) hj hw586    unfold nimBitSign at this; unfold deltaSign; rw [← decode_two B hw]; exact this587  have hones := (Misc.nimsum_bit_character hj (N := 2) (x := maskU B 2 (2 ^ j)) (maskU_mem B 2 _)).2588  refine ⟨hc, hones, ?_⟩589  have h := chi_exactDeg (R := R) (maskU_mem B 2 (2 ^ j))590  rw [hones] at h591  exact ⟨fun T hT hk => by rw [coef_congr hc]; exact h.1 T hT hk,592    let ⟨T, hT, h1, h2⟩ := h.2; ⟨T, hT, h1, by rw [coef_congr hc]; exact h2⟩⟩593594theorem delta_move_chi {B j : Nat} (hj : j < B) {u v : List Bool} (hu : u ∈ bitvecs B) (hv : v ∈ bitvecs B)595    {pre post : List Nat} :596    (sg ((nimSum (pre ++ toNatBE u :: post) ^^^ nimSum (pre ++ toNatBE v :: post)).testBit j) : R) =597      chi (maskU B 2 (2 ^ j)) (u ++ v) := by598  have hlu := mem_bitvecs_length hu599  have huv : u ++ v ∈ bitvecs (B * 2) := mem_bitvecs_of_length (by simp [hlu, mem_bitvecs_length hv]; omega)600  rw [← (delta_spectrum (R := R) hj).1 _ huv]601  unfold deltaSign602  rw [LocalRestore.delta_oneChange, List.take_left' hlu, List.drop_left' hlu]603604/-! ## B3. The unknown-index delta: the total circuit LocalRestore.dC on the full cube -/605606/-- Single-point mask. -/607def pt (n a : Nat) : List Bool := (List.range n).map (fun i => decide (i = a))608609theorem pt_mem (n a : Nat) : pt n a ∈ bitvecs n := mem_bitvecs_of_length (by simp [pt])610611theorem pt_getD (n a j : Nat) : (pt n a).getD j false = (decide (j = a) && decide (j < n)) := by612  simp only [pt, List.getD_eq_getElem?_getD, List.getElem?_map, List.getElem?_range]613  by_cases h : j < n <;> simp [h]614615theorem pm_pt : ∀ (z : List Bool) (n a : Nat), z.length = n → a < n → pm (pt n a) z = z.getD a false616  | [], n, a, hz, ha => by simp at hz; omega617  | b :: z, n, a, hz, ha => by618    obtain ⟨m, rfl⟩ : ∃ m, n = m + 1 := ⟨n - 1, by simp at hz; omega⟩619    have hz' : z.length = m := by simpa using hz620    have hsplit : pt (m + 1) a = decide (0 = a) :: (List.range m).map (fun i => decide (i + 1 = a)) := by621      simp [pt, List.range_succ_eq_map, List.map_map, Function.comp_def]622    rw [hsplit]623    cases a with624    | zero =>625      simp only [pm, decide_true, Bool.true_and, List.getD_cons_zero]626      rw [pm_of_false _ _ (fun s hs => by simp only [List.mem_map] at hs; obtain ⟨i, _, rfl⟩ := hs; simp)]627      simp628    | succ a =>629      have e : (List.range m).map (fun i => decide (i + 1 = a + 1)) = pt m a := by630        simp [pt]631      simp only [pm, show decide (0 = a + 1) = false by simp, Bool.false_and, Bool.false_xor, e,632        List.getD_cons_succ]633      exact pm_pt z m a hz' (by omega)634635/-- Two-point mask. -/636def twoMask (n a b : Nat) : List Bool := List.zipWith xor (pt n a) (pt n b)637638theorem twoMask_mem (n a b : Nat) : twoMask n a b ∈ bitvecs n := mem_bitvecs_of_length (by simp [twoMask, pt])639640theorem pm_twoMask {z : List Bool} {n a b : Nat} (hz : z.length = n) (ha : a < n) (hb : b < n) :641    pm (twoMask n a b) z = xor (z.getD a false) (z.getD b false) := by642  unfold twoMask643  rw [Misc.pm_zipWith _ _ z (by simp [pt]), pm_pt z n a hz ha, pm_pt z n b hz hb]644645theorem twoMask_eq_map (n a b : Nat) :646    twoMask n a b = (List.range n).map (fun i => xor (decide (i = a)) (decide (i = b))) := by647  apply List.ext_getElem (by simp [twoMask, pt])648  intro i h1 h2649  simp [twoMask, pt, List.getElem_zipWith]650651theorem ones_map_range (n : Nat) (p : Nat → Bool) : ones ((List.range n).map p) = ((List.range n).filter p).length := by652  unfold ones653  rw [List.filter_map, List.length_map]654  rfl655656theorem ite_lt_succ (a n : Nat) :657    (if a < n + 1 then 1 else 0) = (if a < n then 1 else 0) + (if n = a then 1 else 0) := by658  by_cases h1 : a < n659  · have : ¬ n = a := by omega660    simp [h1, this, show a < n + 1 by omega]661  · by_cases h2 : n = a662    · subst h2; simp663    · simp [h1, h2, show ¬ a < n + 1 by omega]664665theorem count_two {a b : Nat} (hab : a ≠ b) : ∀ n : Nat,666    ((List.range n).filter (fun i => xor (decide (i = a)) (decide (i = b)))).length =667      (if a < n then 1 else 0) + (if b < n then 1 else 0)668  | 0 => by simp669  | n + 1 => by670    rw [List.range_succ, List.filter_append, List.length_append, count_two hab n, ite_lt_succ a n, ite_lt_succ b n]671    have e : ([n].filter (fun i => xor (decide (i = a)) (decide (i = b)))).length =672        (if n = a then 1 else 0) + (if n = b then 1 else 0) := by673      by_cases h1 : n = a674      · subst h1; simp [hab]675      · by_cases h2 : n = b676        · subst h2; simp [h1, Ne.symm h1]677        · simp [h1, h2]678    rw [e]; omega679680theorem ones_twoMask {n a b : Nat} (hab : a ≠ b) (ha : a < n) (hb : b < n) : ones (twoMask n a b) = 2 := by681  rw [twoMask_eq_map, ones_map_range, count_two hab, if_pos ha, if_pos hb]682683theorem twoMask_getD (n a b j : Nat) :684    (twoMask n a b).getD j false = xor (decide (j = a) && decide (j < n)) (decide (j = b) && decide (j < n)) := by685  rw [twoMask_eq_map]686  simp only [List.getD_eq_getElem?_getD, List.getElem?_map, List.getElem?_range]687  by_cases h : j < n <;> simp [h]688689/-- The sign encoding of the total single-change delta circuit, on the full cube. -/690def dSign (B N q : Nat) (z : List Bool) : R := sg (eval (vfun z) (LocalRestore.dC B N q))691692theorem eval_yC (B N i p : Nat) (z : Nat → Bool) :693    eval z (LocalRestore.yC B N i p) = xor (z (B * i + p)) (z (B * N + (B * i + p))) := by694  simp only [LocalRestore.yC, CorrBridge.eval_xor2, eval_input]695696/-- THE PER-HEAP XOR IS A TWO-COORDINATE CHARACTER on the full 2BN-bit cube. -/697theorem yC_chi {B N i p : Nat} (hi : i < N) (hp : p < B) {z : List Bool} (hz : z ∈ bitvecs (2 * (B * N))) :698    (sg (eval (vfun z) (LocalRestore.yC B N i p)) : R) =699      chi (twoMask (2 * (B * N)) (B * i + p) (B * N + (B * i + p))) z := by700  have hl := mem_bitvecs_length hz701  have h1 : B * i + p < B * N := SelectCircuit.heap_lt hi hp702  rw [eval_yC]; unfold chi703  rw [pm_twoMask hl (by omega) (by omega)]; rfl704705theorem eval_dC_any {B N q p : Nat} (hq : q < B) (hp : p = B - 1 - q) (z : Nat → Bool) :706    eval z (LocalRestore.dC B N q) =707      (List.range N).any (fun i => xor (z (B * i + p)) (z (B * N + (B * i + p)))) := by708  subst hp709  simp only [LocalRestore.dC, hq, if_true, eval_or, List.any_map]710  congr 1; funext i; simp only [Function.comp_apply, eval_yC]711712theorem getD_replicate_false (n j : Nat) : (List.replicate n false).getD j false = false := by713  simp only [List.getD_eq_getElem?_getD, List.getElem?_replicate]; split <;> rfl714715theorem dSign_true {B N q p : Nat} (hq : q < B) (hp : p = B - 1 - q) {z : List Bool} {i : Nat} (hi : i < N)716    (h : xor (z.getD (B * i + p) false) (z.getD (B * N + (B * i + p)) false) = true) : (dSign B N q z : R) = -1 := by717  unfold dSign718  rw [eval_dC_any hq hp]719  have : (List.range N).any (fun i => xor (vfun z (B * i + p)) (vfun z (B * N + (B * i + p)))) = true :=720    List.any_eq_true.2 ⟨i, List.mem_range.2 hi, h⟩721  rw [this]; rfl722723/-- 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.symm783784/-- … hence its Fourier expansion has at least two nonzero coefficients. -/785theorem dC_two_coefs {B N q : Nat} (hN : 2 ≤ N) (hq : q < B) :786    ∃ S ∈ bitvecs (2 * (B * N)), ∃ T ∈ bitvecs (2 * (B * N)), S ≠ T ∧787      coef (2 * (B * N)) (dSign (R := R) B N q) S ≠ 0 ∧ coef (2 * (B * N)) (dSign (R := R) B N q) T ≠ 0 := by788  let n := 2 * (B * N)789  let f := dSign (R := R) B N q790  have hsq : ∀ z ∈ bitvecs n, f z * f z = 1 := fun z _ => sg_mul_self _791  apply Classical.byContradiction; intro hno792  -- some coefficient is nonzero793  have hex : ∃ S ∈ bitvecs n, coef n f S ≠ 0 := by794    apply Classical.byContradiction; intro hall795    have h0 : gs (bitvecs n) (fun S => coef n f S ^ 2) = 0 := by796      rw [gs_congr (fun S hS => by797        show coef n f S ^ 2 = (fun _ => (0 : R)) S798        have : coef n f S = 0 := Classical.byContradiction (fun h => hall ⟨S, hS, h⟩)799        rw [this]; grind), gs_zero]800    rw [sign_mass n f hsq] at h0801    have := OrderedRing.zero_lt_one (R := R); rw [h0] at this; exact Preorder.lt_irrefl _ this802  obtain ⟨S, hS, hSne⟩ := hex803  have honly : ∀ T ∈ bitvecs n, T ≠ S → coef n f T = 0 := by804    intro T hT hTS805    apply Classical.byContradiction; intro h806    exact hno ⟨S, hS, T, hT, fun e => hTS e.symm, hSne, h⟩807  -- then f = coef(S) χ_S on the cube, with coef(S)² = 1808  have hrep : ∀ z ∈ bitvecs n, f z = coef n f S * chi S z := by809    intro z hz810    rw [← inversion n f hz]811    have hl := mem_bitvecs_length hS812    rw [gs_congr (fun T hT => by813      show coef n f T * chi T z = Noise.ind (decide (S = T)) * (coef n f T * chi T z)814      by_cases hTS : T = S815      · subst hTS; simp only [decide_true, Noise.ind, if_true]; grind816      · rw [honly T hT hTS]; grind), gs_point n S hl (fun T => coef n f T * chi T z)]817  have hmass := sign_mass n f hsq818  rw [gs_congr (fun T hT => by819    show coef n f T ^ 2 = Noise.ind (decide (S = T)) * coef n f T ^ 2820    by_cases hTS : T = S821    · subst hTS; simp only [decide_true, Noise.ind, if_true]; grind822    · rw [honly T hT hTS]; grind), gs_point n S (mem_bitvecs_length hS) (fun T => coef n f T ^ 2)] at hmass823  exact dC_not_character hN hq ⟨S, coef n f S, by grind, hrep⟩824825/-- N = 1: dC IS the two-coordinate character (old and new value of the only heap). -/826theorem dC_one {B q : Nat} (hq : q < B) {z : List Bool} (hz : z ∈ bitvecs (2 * (B * 1))) :827    (dSign B 1 q z : R) = chi (twoMask (2 * (B * 1)) (B * 0 + (B - 1 - q)) (B * 1 + (B * 0 + (B - 1 - q)))) z := by828  unfold dSign829  rw [← yC_chi (by omega) (by omega) hz]830  have : eval (vfun z) (LocalRestore.dC B 1 q) = eval (vfun z) (LocalRestore.yC B 1 0 (B - 1 - q)) := by831    simp [LocalRestore.dC, hq]832  rw [this]833834theorem dC_one_exactDeg {B q : Nat} (hq : q < B) : ExactDeg (2 * (B * 1)) (dSign (R := R) B 1 q) 2 := by835  have hc : ∀ z ∈ bitvecs (2 * (B * 1)), (dSign B 1 q z : R) =836      chi (twoMask (2 * (B * 1)) (B * 0 + (B - 1 - q)) (B * 1 + (B * 0 + (B - 1 - q)))) z := fun z hz => dC_one hq hz837  have hm := twoMask_mem (2 * (B * 1)) (B * 0 + (B - 1 - q)) (B * 1 + (B * 0 + (B - 1 - q)))838  have hones : ones (twoMask (2 * (B * 1)) (B * 0 + (B - 1 - q)) (B * 1 + (B * 0 + (B - 1 - q)))) = 2 :=839    ones_twoMask (by omega) (by omega) (by omega)840  have h := chi_exactDeg (R := R) hm841  rw [hones] at h842  exact ⟨fun T hT hk => by rw [coef_congr hc]; exact h.1 T hT hk,843    let ⟨T, hT, h1, h2⟩ := h.2; ⟨T, hT, h1, by rw [coef_congr hc]; exact h2⟩⟩844845/-- N = 0 or q ≥ B: dC is constant false, i.e. the constant character χ_0. -/846theorem dC_trivial {B N q : Nat} (h : N = 0 ∨ B ≤ q) (z : List Bool) :847    (dSign B N q z : R) = chi (List.replicate (2 * (B * N)) false) z := by848  have hz : (chi (List.replicate (2 * (B * N)) false) z : R) = 1 := by849    unfold chi; rw [pm_of_false _ _ (fun s hs => (List.eq_of_mem_replicate hs))]; rfl850  rw [hz]; unfold dSign851  rcases h with rfl | hq852  · by_cases hq : q < B853    · simp [LocalRestore.dC, hq, sg]854    · simp [LocalRestore.dC, hq, sg]855  · simp [LocalRestore.dC, show ¬ q < B by omega, sg]856857/-! ### Agreement on the promised domain -/858859/-- The two frames as a point of the full cube. -/860def enc (B N : Nat) (Q Q' : List Nat) : List Bool := (List.range (2 * (B * N))).map (LocalRestore.tf B N Q Q')861862theorem enc_mem (B N : Nat) (Q Q' : List Nat) : enc B N Q Q' ∈ bitvecs (2 * (B * N)) :=863  mem_bitvecs_of_length (by simp [enc])864865theorem vfun_enc {B N : Nat} {Q Q' : List Nat} {j : Nat} (hj : j < 2 * (B * N)) :866    vfun (enc B N Q Q') j = LocalRestore.tf B N Q Q' j := by867  simp [vfun, enc, List.getD_eq_getElem?_getD, List.getElem?_map, List.getElem?_range, hj]868869theorem eval_enc {B N : Nat} {Q Q' : List Nat} (C : Circ) (hC : maxInput C ≤ 2 * (B * N)) :870    eval (vfun (enc B N Q Q')) C = eval (LocalRestore.tf B N Q Q') C :=871  eval_congr_below _ _ C (fun i hi => vfun_enc (by omega))872873/-- AGREEMENT WITH THE DELTA on every single-change transition (in particular on every legal874    move): the sign of dC at the encoded pair is the sign of delta bit q. -/875theorem dSign_enc {B N q : Nat} {Q Q' : List Nat} (hQ : Q.length = N) (hQ' : Q'.length = N)876    (hw : Game.Width B Q) (hw' : Game.Width B Q') (h1 : LocalRestore.OneChange Q Q') :877    (dSign B N q (enc B N Q Q') : R) = sg ((nimSum Q ^^^ nimSum Q').testBit q) := by878  unfold dSign879  rw [eval_enc _ (LocalRestore.dC_res (B := B) (N := N) q).2.2, LocalRestore.dC_eval hQ hQ',880    LocalRestore.localDelta_eq hQ hQ' hw hw' h1]881882theorem set_split (Q : List Nat) {i : Nat} (hi : i < Q.length) (y : Nat) :883    Q = Q.take i ++ Q[i] :: Q.drop (i + 1) ∧ Q.set i y = Q.take i ++ y :: Q.drop (i + 1) := by884  constructor885  · simp886  · rw [List.set_eq_take_append_cons_drop]; simp [hi]887888/-- KNOWN CHANGED HEAP: on transitions that change only heap i (Q' = Q.set i y), the sign of889    dC equals the two-coordinate character of heap i (old and new bit q).  So, conditional on890    the changed index, the delta bit is a degree-two character, as the paper states. -/891theorem dSign_known_heap {B N q i : Nat} (hq : q < B) (hi : i < N) {Q : List Nat} (hQ : Q.length = N)892    (y : Nat) :893    (dSign B N q (enc B N Q (Q.set i y)) : R) =894      chi (twoMask (2 * (B * N)) (B * i + (B - 1 - q)) (B * N + (B * i + (B - 1 - q)))) (enc B N Q (Q.set i y)) := by895  have hQ' : (Q.set i y).length = N := by simp [hQ]896  rw [← yC_chi hi (by omega) (enc_mem B N Q (Q.set i y))]897  unfold dSign898  rw [eval_enc _ (LocalRestore.dC_res (B := B) (N := N) q).2.2,899    eval_enc _ (LocalRestore.yC_max (B := B) (N := N) hi (by omega))]900  congr 1901  rw [LocalRestore.dC_eval hQ hQ', LocalRestore.yC_eval hQ hQ' hi (by omega),902    show B - 1 - (B - 1 - q) = q by omega]903  unfold LocalRestore.localDelta904  rw [Game.testBit_ofBits]905  simp only [hq, decide_true, Bool.true_and]906  apply Bool.eq_iff_iff.mpr907  simp only [List.any_eq_true, List.mem_range]908  constructor909  · rintro ⟨k, hk, h⟩910    by_cases hki : k = i911    · subst hki; exact h912    · rw [Misc.getD_set_ne' Q y hki] at h; simp at h913  · intro h; exact ⟨i, hi, h⟩914915/-! ### The characters that agree with the delta bit on the single-change domain -/916917/-- The bit list of one frame. -/918def frame (B N : Nat) (Q : List Nat) : List Bool := (List.range (B * N)).map (CorrBridge.boardBits B Q)919920theorem frame_length (B N : Nat) (Q : List Nat) : (frame B N Q).length = B * N := by simp [frame]921922theorem frame_mem (B N : Nat) (Q : List Nat) : frame B N Q ∈ bitvecs (B * N) :=923  mem_bitvecs_of_length (frame_length B N Q)924925theorem frame_getD {B N : Nat} {Q : List Nat} {j : Nat} (hj : j < B * N) :926    (frame B N Q).getD j false = CorrBridge.boardBits B Q j := by927  simp [frame, List.getD_eq_getElem?_getD, List.getElem?_map, List.getElem?_range, hj]928929theorem enc_split (B N : Nat) (Q Q' : List Nat) : enc B N Q Q' = frame B N Q ++ frame B N Q' := by930  unfold enc frame931  rw [show 2 * (B * N) = B * N + B * N by omega, List.range_add, List.map_append, List.map_map]932  congr 1933  · apply List.map_congr_left; intro j hj; exact LocalRestore.tf_left (List.mem_range.1 hj)934  · apply List.map_congr_left; intro j _; simp only [Function.comp_apply]; exact LocalRestore.tf_right j935936/-- Decoding a board's frame returns the board. -/937theorem decode_frame {B N : Nat} {Q : List Nat} (hQ : Q.length = N) (hw : Game.Width B Q) :938    decodeBoard B N (frame B N Q) = Q := by939  have key : ∀ i, i < N → (decodeBoard B N (frame B N Q)).getD i 0 = Q.getD i 0 := by940    intro i hi941    rw [CorrBridge.decodeBoard_getD B N _ i hi]942    have hlen : ((frame B N Q).drop (B * i)).take B = ((frame B N Q).drop (B * i)).take B := rfl943    have hl : (((frame B N Q).drop (B * i)).take B).length = B := by944      simp only [List.length_take, List.length_drop, frame_length]945      have := Nat.mul_le_mul_left B (show i + 1 ≤ N by omega)946      rw [Nat.mul_succ] at this; omega947    apply Nat.eq_of_testBit_eq; intro k948    by_cases hk : k < B949    · have := testBit_toNatBE (((frame B N Q).drop (B * i)).take B) (B - 1 - k) (by omega)950      rw [hl, show B - 1 - (B - 1 - k) = k by omega] at this951      rw [this, CorrBridge.getD_take_drop _ _ _ _ (by omega), frame_getD (SelectCircuit.heap_lt hi (by omega)),952        CorrBridge.boardBits_heap hQ hi (by omega), show B - 1 - (B - 1 - k) = k by omega]953    · have h1 := toNatBE_lt (((frame B N Q).drop (B * i)).take B)954      rw [hl] at h1955      have h2 := SelectCircuit.getD_lt_of_width hQ hw hi956      rw [Nat.testBit_lt_two_pow (Nat.lt_of_lt_of_le h1 (Nat.pow_le_pow_right (by decide) (by omega))),957        Nat.testBit_lt_two_pow (Nat.lt_of_lt_of_le h2 (Nat.pow_le_pow_right (by decide) (by omega)))]958  apply List.ext_getElem (by rw [length_decodeBoard, hQ])959  intro i h1 h2960  have h1' := h1961  rw [length_decodeBoard] at h1'962  have := key i h1'963  simp only [List.getD_eq_getElem?_getD, List.getElem?_eq_getElem h1, List.getElem?_eq_getElem h2,964    Option.getD_some] at this965  exact this966967/-- The global mask: bit q of every heap, in both frames (2N coordinates). -/968def gMask (B N q : Nat) : List Bool := maskU B N (2 ^ q) ++ maskU B N (2 ^ q)969970theorem gMask_mem (B N q : Nat) : gMask B N q ∈ bitvecs (2 * (B * N)) :=971  mem_bitvecs_of_length (by simp [gMask, length_maskU]; omega)972973theorem ones_gMask {B N q : Nat} (hq : q < B) : ones (gMask B N q) = 2 * N := by974  have h := (Misc.nimsum_bit_character hq (x := maskU B N (2 ^ q)) (maskU_mem B N _)).2975  unfold gMask; rw [ones_append, h]; omega976977/-- 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]986987theorem toBitsBE_getD : ∀ (B : Nat) (u p : Nat), p < B → (toBitsBE B u).getD p false = u.testBit (B - 1 - p)988  | 0, _, _, hp => by omega989  | B + 1, u, 0, _ => by simp [toBitsBE]990  | B + 1, u, p + 1, hp => by991    simp only [toBitsBE, List.getD_cons_succ]992    rw [toBitsBE_getD B u p (by omega)]; congr 1; omega993994theorem maskU_getD {B : Nat} (u : Nat) {p : Nat} (hp : p < B) : ∀ (N i : Nat), i < N →995    (maskU B N u).getD (B * i + p) false = u.testBit (B - 1 - p)996  | 0, _, hi => by omega997  | N + 1, 0, _ => by998    simp only [maskU, Nat.mul_zero, Nat.zero_add, List.getD_eq_getElem?_getD]999    rw [List.getElem?_append_left (by rw [length_toBitsBE]; exact hp)]1000    have := toBitsBE_getD B u p hp1001    rwa [List.getD_eq_getElem?_getD] at this1002  | N + 1, i + 1, hi => by1003    simp only [maskU, List.getD_eq_getElem?_getD]1004    rw [List.getElem?_append_right (by rw [length_toBitsBE]; rw [Nat.mul_succ]; omega), length_toBitsBE,1005      show B * (i + 1) + p - B = B * i + p by rw [Nat.mul_succ]; omega]1006    have := maskU_getD u hp N i (by omega)1007    rwa [List.getD_eq_getElem?_getD] at this10081009/-- The board with heap i equal to 2^r and all other heaps empty. -/1010def unitBoard (N i r : Nat) : List Nat := (List.replicate N 0).set i (2 ^ r)10111012theorem unitBoard_length (N i r : Nat) : (unitBoard N i r).length = N := by simp [unitBoard]10131014theorem zero_width (B N : Nat) : Game.Width B (List.replicate N 0) := by1015  intro x hx; rw [List.eq_of_mem_replicate hx]; exact Nat.two_pow_pos B10161017theorem unitBoard_width {B N i r : Nat} (hr : r < B) : Game.Width B (unitBoard N i r) := by1018  intro x hx1019  unfold unitBoard at hx1020  rcases List.mem_or_eq_of_mem_set hx with h | h1021  · rw [List.eq_of_mem_replicate h]; exact Nat.two_pow_pos B1022  · rw [h]; exact Nat.pow_lt_pow_right (by decide) hr10231024theorem unitBoard_split {N i : Nat} (hi : i < N) (r : Nat) :1025    ∃ pre post, List.replicate N 0 = pre ++ 0 :: post ∧ unitBoard N i r = pre ++ 2 ^ r :: post := by1026  have h := set_split (List.replicate N 0) (i := i) (by simp; exact hi) (2 ^ r)1027  refine ⟨(List.replicate N 0).take i, (List.replicate N 0).drop (i + 1), ?_, h.2⟩1028  have e : (List.replicate N 0)[i]'(by simp; exact hi) = 0 := by simp1029  have h1 := h.11030  rw [e] at h1; exact h110311032theorem boardBits_zero (B N j : Nat) : CorrBridge.boardBits B (List.replicate N 0) j = false := by1033  unfold CorrBridge.boardBits1034  split1035  · simp [List.getD_eq_getElem?_getD, List.getElem?_replicate]; split <;> simp1036  · rfl10371038theorem boardBits_unit {B N i r : Nat} (hi : i < N) (hr : r < B) {j : Nat} (hj : j < B * N) :1039    CorrBridge.boardBits B (unitBoard N i r) j = decide (j = B * i + (B - 1 - r)) := by1040  have hB : 0 < B := by omega1041  have hjB : j / B < N := by rw [Nat.div_lt_iff_lt_mul hB, Nat.mul_comm]; exact hj1042  have hm : j % B < B := Nat.mod_lt _ hB1043  have e := CorrBridge.boardBits_heap (B := B) (unitBoard_length N i r) hjB hm1044  rw [show B * (j / B) + j % B = j from Nat.div_add_mod j B] at e1045  rw [e]1046  have hget : (unitBoard N i r).getD (j / B) 0 = if j / B = i then 2 ^ r else 0 := by1047    unfold unitBoard1048    by_cases h : j / B = i1049    · subst h; rw [if_pos rfl, Misc.getD_set_eq' _ _ (by simp; exact hi)]1050    · rw [if_neg h, Misc.getD_set_ne' _ _ h]1051      simp only [List.getD_eq_getElem?_getD, List.getElem?_replicate]; split <;> rfl1052  rw [hget]1053  apply Bool.eq_iff_iff.mpr1054  simp only [decide_eq_true_eq]1055  constructor1056  · intro h1057    by_cases h1 : j / B = i1058    · rw [if_pos h1, Nat.testBit_two_pow] at h1059      simp only [decide_eq_true_eq] at h1060      have := Nat.div_add_mod j B1061      rw [h1] at this; omega1062    · rw [if_neg h1] at h; simp at h1063  · intro h1064    have h1 : j / B = i := by1065      rw [h, Nat.mul_comm, Nat.add_comm, Nat.add_mul_div_right _ _ hB, Nat.div_eq_of_lt (by omega)]; omega1066    have h2 : j % B = B - 1 - r := by1067      rw [h, Nat.mul_comm, Nat.add_comm, Nat.add_mul_mod_self_right, Nat.mod_eq_of_lt (by omega)]1068    rw [if_pos h1, Nat.testBit_two_pow]; simp only [decide_eq_true_eq]; omega10691070theorem enc_unit_left {B N i r : Nat} (hi : i < N) (hr : r < B) :1071    enc B N (unitBoard N i r) (List.replicate N 0) = pt (2 * (B * N)) (B * i + (B - 1 - r)) := by1072  have ha : B * i + (B - 1 - r) < B * N := SelectCircuit.heap_lt hi (by omega)1073  apply mask_ext (enc_mem _ _ _ _) (pt_mem _ _)1074  intro j hj1075  have e := vfun_enc (B := B) (N := N) (Q := unitBoard N i r) (Q' := List.replicate N 0) hj1076  unfold vfun at e1077  rw [e, pt_getD]1078  by_cases hj1 : j < B * N1079  · rw [LocalRestore.tf_left hj1, boardBits_unit hi hr hj1]; simp [hj]1080  · have e2 : LocalRestore.tf B N (unitBoard N i r) (List.replicate N 0) j =1081        CorrBridge.boardBits B (List.replicate N 0) (j - B * N) := by1082      have := LocalRestore.tf_right (B := B) (N := N) (Q := unitBoard N i r) (Q' := List.replicate N 0) (j - B * N)1083      rwa [show B * N + (j - B * N) = j by omega] at this1084    rw [e2, boardBits_zero]1085    have : ¬ j = B * i + (B - 1 - r) := by omega1086    simp [this]10871088theorem enc_unit_right {B N i r : Nat} (hi : i < N) (hr : r < B) :1089    enc B N (List.replicate N 0) (unitBoard N i r) = pt (2 * (B * N)) (B * N + (B * i + (B - 1 - r))) := by1090  have ha : B * i + (B - 1 - r) < B * N := SelectCircuit.heap_lt hi (by omega)1091  apply mask_ext (enc_mem _ _ _ _) (pt_mem _ _)1092  intro j hj1093  have e := vfun_enc (B := B) (N := N) (Q := List.replicate N 0) (Q' := unitBoard N i r) hj1094  unfold vfun at e1095  rw [e, pt_getD]1096  by_cases hj1 : j < B * N1097  · rw [LocalRestore.tf_left hj1, boardBits_zero]1098    have : ¬ j = B * N + (B * i + (B - 1 - r)) := by omega1099    simp [this]1100  · have e2 : LocalRestore.tf B N (List.replicate N 0) (unitBoard N i r) j =1101        CorrBridge.boardBits B (unitBoard N i r) (j - B * N) := by1102      have := LocalRestore.tf_right (B := B) (N := N) (Q := List.replicate N 0) (Q' := unitBoard N i r) (j - B * N)1103      rwa [show B * N + (j - B * N) = j by omega] at this1104    rw [e2, boardBits_unit hi hr (by omega)]1105    by_cases hja : j = B * N + (B * i + (B - 1 - r))1106    · have : j - B * N = B * i + (B - 1 - r) := by omega1107      simp [this, hja]; omega1108    · have : ¬ (j - B * N = B * i + (B - 1 - r)) := by omega1109      simp [this, hja]11101111theorem pm_pt_left {S : List Bool} {n a : Nat} (hS : S.length = n) (ha : a < n) : pm S (pt n a) = S.getD a false := by1112  rw [pm_comm S (pt n a) (by simp [pt, hS]), pm_pt S n a hS ha]11131114theorem sg_inj {b c : Bool} (h : (sg b : R) = sg c) : b = c := by1115  cases b <;> cases c <;> simp only [sg, Bool.false_eq_true, if_true, if_false] at h1116  · rfl1117  · exact absurd h one_ne_neg_one1118  · exact absurd h.symm one_ne_neg_one1119  · rfl11201121/-- 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]; omega11761177theorem nimSum_zeros : ∀ N : Nat, nimSum (List.replicate N 0) = 01178  | 0 => rfl1179  | N + 1 => by simp only [List.replicate_succ, nimSum, nimSum_zeros N, Nat.zero_xor]11801181theorem enc_zeros (B N : Nat) :1182    enc B N (List.replicate N 0) (List.replicate N 0) = List.replicate (2 * (B * N)) false := by1183  apply mask_ext (enc_mem _ _ _ _) (mem_bitvecs_of_length (by simp))1184  intro j hj1185  have e := vfun_enc (B := B) (N := N) (Q := List.replicate N 0) (Q' := List.replicate N 0) hj1186  unfold vfun at e1187  rw [e, getD_replicate_false]1188  by_cases hj1 : j < B * N1189  · rw [LocalRestore.tf_left hj1, boardBits_zero]1190  · have := LocalRestore.tf_right (B := B) (N := N) (Q := List.replicate N 0) (Q' := List.replicate N 0) (j - B * N)1191    rw [show B * N + (j - B * N) = j by omega, boardBits_zero] at this1192    exact this11931194/-- SIGNED VERSION: if c·χ_S (c = ±1) agrees with the sign of the delta bit on the1195    single-change domain, then c = 1 (test pair Q = Q′ = 0) and S is the global mask. -/1196theorem char_unique_signed {B N q : Nat} (hq : q < B) {S : List Bool} (hS : S ∈ bitvecs (2 * (B * N)))1197    {c : R} (h : ∀ Q Q', Q.length = N → Q'.length = N → Game.Width B Q → Game.Width B Q' → LocalRestore.OneChange Q Q' →1198      c * chi S (enc B N Q Q') = sg ((nimSum Q ^^^ nimSum Q').testBit q)) :1199    c = 1 ∧ S = gMask B N q := by1200  have h0 := h (List.replicate N 0) (List.replicate N 0) (by simp) (by simp) (zero_width B N) (zero_width B N) (Or.inl rfl)1201  rw [enc_zeros, chi_zeros, nimSum_zeros, Nat.xor_zero, Nat.zero_testBit] at h01202  have hc : c = 1 := by simp only [sg, Bool.false_eq_true, if_false] at h0; grind1203  subst hc1204  refine ⟨rfl, char_unique (R := R) hq hS (fun Q Q' a b c' d e => ?_)⟩1205  have := h Q Q' a b c' d e1206  clear h h01207  have e1 : (1 : R) * chi S (enc B N Q Q') = chi S (enc B N Q Q') := by grind1208  rw [e1] at this; exact this12091210/-- 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; omega12191220end Generic12211222/-! ## Agreement with the phase-6 rational statements -/12231224section RatCheck1225open Prob12261227attribute [local instance] Semiring.natCast12281229theorem chi_rat (S x : List Bool) : (chi S x : Rat) = sgn (pm S x) := by1230  unfold chi; cases pm S x <;> rfl12311232/-- At ℚ the normalised inner product of two characters is exactly the expression of1233    Misc.char_orth, so `orthonormal` instantiates and agrees with it. -/1234theorem ip_chi_rat (S T : List Bool) :1235    ip (R := Rat) S.length (chi S) (chi T) = rsum (bitvecs S.length) (fun x => sgn (pm S x) * sgn (pm T x)) / 2 ^ S.length := by1236  unfold ip1237  rw [gs_rat, Rat.div_def]1238  congr 112391240theorem orthonormal_rat_agrees (S T : List Bool) (h : S.length = T.length) :1241    ip (R := Rat) S.length (chi S) (chi T) = if S = T then 1 else 0 := by1242  rw [ip_chi_rat]; exact Misc.char_orth S T h12431244/-- The paper's parity-correlation quantity in the indicator convention (as in the premise1245    Bridge.ParityCorrPremise) is the Fourier coefficient of the indicator at the full mask. -/1246theorem parity_corr_coef (m : Nat) (g : List Bool → Bool) :1247    rsum (bitvecs m) (fun y => Bridge.ind (g y) * sgn (par y)) / 2 ^ m =1248      coef (R := Rat) m (fun y => Noise.ind (g y)) (List.replicate m true) := by1249  unfold coef ip1250  rw [gs_rat, Rat.div_def]1251  congr 11252  apply rsum_congr; intro y hy1253  rw [chi_rat, par_eq_pm y, mem_bitvecs_length hy]1254  show Bridge.ind (g y) * _ = Noise.ind (g y) * _1255  cases g y <;> rfl12561257end RatCheck12581259/-! ## Axiom checks -/1260#print axioms pm_comm1261#print axioms pm_xor_right1262#print axioms pm_of_false1263#print axioms pm_zeros_right1264#print axioms pm_selCount1265#print axioms cube_mem1266#print axioms nodup_map_cons1267#print axioms cube_nodup1268#print axioms cube_card1269#print axioms ofPred_mem1270#print axioms ofPred_getD1271#print axioms mask_ext1272#print axioms mask_of_subset1273#print axioms two_pos'1274#print axioms two_pow_pos''1275#print axioms two_pow_ne1276#print axioms pow_mul_inv1277#print axioms one_ne_neg_one1278#print axioms sg_xor1279#print axioms sg_mul_self1280#print axioms gs_mul_right1281#print axioms gs_count1282#print axioms gs_single_le1283#print axioms chi_pow1284#print axioms coef_congr1285#print axioms chi_mul_left1286#print axioms chi_mul_right1287#print axioms chi_zeros1288#print axioms char_sum_gen1289#print axioms zipWith_length_eq1290#print axioms orth_sum1291#print axioms orthonormal1292#print axioms dual_sum1293#print axioms inversion1294#print axioms uniqueness1295#print axioms parseval1296#print axioms plancherel1297#print axioms dim_zero1298#print axioms tail_nonneg1299#print axioms tail_congr1300#print axioms exactDeg_unique1301#print axioms tail_of_degLe1302#print axioms coef_sq_le_tail1303#print axioms bandLimited_corr1304#print axioms sign_mass1305#print axioms tail_le_one1306#print axioms coef_chi1307#print axioms tail_chi1308#print axioms chi_exactDeg1309#print axioms bandLimited_chi1310#print axioms sg_eq_ind1311#print axioms coef_one1312#print axioms sign_indicator1313#print axioms par_eq_pm1314#print axioms maskU_mem1315#print axioms nimBitSign_chi1316#print axioms nimBit_spectrum1317#print axioms nimBit_corr_of_tail1318#print axioms decode_two1319#print axioms delta_spectrum1320#print axioms delta_move_chi1321#print axioms pt_mem1322#print axioms pt_getD1323#print axioms pm_pt1324#print axioms twoMask_mem1325#print axioms pm_twoMask1326#print axioms twoMask_eq_map1327#print axioms ones_map_range1328#print axioms ite_lt_succ1329#print axioms count_two1330#print axioms ones_twoMask1331#print axioms twoMask_getD1332#print axioms eval_yC1333#print axioms yC_chi1334#print axioms eval_dC_any1335#print axioms getD_replicate_false1336#print axioms dSign_true1337#print axioms dC_not_character1338#print axioms dC_two_coefs1339#print axioms dC_one1340#print axioms dC_one_exactDeg1341#print axioms dC_trivial1342#print axioms enc_mem1343#print axioms vfun_enc1344#print axioms eval_enc1345#print axioms dSign_enc1346#print axioms set_split1347#print axioms dSign_known_heap1348#print axioms frame_length1349#print axioms frame_mem1350#print axioms frame_getD1351#print axioms enc_split1352#print axioms decode_frame1353#print axioms gMask_mem1354#print axioms ones_gMask1355#print axioms gMask_delta1356#print axioms toBitsBE_getD1357#print axioms maskU_getD1358#print axioms unitBoard_length1359#print axioms zero_width1360#print axioms unitBoard_width1361#print axioms unitBoard_split1362#print axioms boardBits_zero1363#print axioms boardBits_unit1364#print axioms enc_unit_left1365#print axioms enc_unit_right1366#print axioms pm_pt_left1367#print axioms sg_inj1368#print axioms char_unique1369#print axioms nimSum_zeros1370#print axioms enc_zeros1371#print axioms char_unique_signed1372#print axioms no_low_degree_extension1373#print axioms chi_rat1374#print axioms ip_chi_rat1375#print axioms orthonormal_rat_agrees1376#print axioms parity_corr_coef13771378end Fourier1379end NimAudit