Unrestricted depth-three lower bound: language bit reduction loop

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/DepthThree/LanguageBitReductionLoop.lean

Imports, namespaces, module visibility, documentation, and formatting are adapted for complexitylib. The source theorem statements and mathematical proofs are retained.

def Complexity.DepthThreeLowerBound.modulusUpdateLoop (p : List Bool) (v : Bool) (shift : ℕ) : ℕ → List Bool → List Bool

Apply the shifted-modulus updates used in coefficient cancellation.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.DepthThreeLowerBound.modulusUpdateLoop p v shift 0 x✝ = x✝

@[simp]

theorem Complexity.DepthThreeLowerBound.modulusUpdateLoop_zero (p : List Bool) (v : Bool) (shift : ℕ) (c : List Bool) : modulusUpdateLoop p v shift 0 c = c

theorem Complexity.DepthThreeLowerBound.modulusUpdateLoop_step (p : List Bool) (v : Bool) (shift j : ℕ) (c : List Bool) : modulusUpdateLoop p v shift (j + 1) c = xorListAt (modulusUpdateLoop p v shift j c) (shift + j) (v && p.getD j false)

@[simp]

theorem Complexity.DepthThreeLowerBound.modulusUpdateLoop_length (p : List Bool) (v : Bool) (shift j : ℕ) (c : List Bool) : (modulusUpdateLoop p v shift j c).length = c.length

theorem Complexity.DepthThreeLowerBound.modulusUpdateLoop_getD (p : List Bool) (v : Bool) (shift j : ℕ) (c : List Bool) (hbound : shift + j ≤ c.length) (k : ℕ) : (modulusUpdateLoop p v shift j c).getD k false = (c.getD k false ^^ if shift ≤ k ∧ k < shift + j then v && p.getD (k - shift) false else false)

theorem Complexity.DepthThreeLowerBound.modulusUpdateLoop_above (p : List Bool) (v : Bool) (shift j : ℕ) (c : List Bool) (hbound : shift + j ≤ c.length) (k : ℕ) (hk : shift + j ≤ k) : (modulusUpdateLoop p v shift j c).getD k false = c.getD k false

theorem Complexity.DepthThreeLowerBound.modulusUpdateLoop_high (p : List Bool) (v : Bool) (shift : ℕ) (c : List Bool) (hbound : shift + p.length ≤ c.length) : (modulusUpdateLoop p v shift p.length c).getD (shift + p.length) false = c.getD (shift + p.length) false

def Complexity.DepthThreeLowerBound.cancelByUpdates (p c : List Bool) (shift : ℕ) : List Bool

Cancel a leading coefficient through list updates.

Equations

• Complexity.DepthThreeLowerBound.cancelByUpdates p c shift = (Complexity.DepthThreeLowerBound.modulusUpdateLoop p (c.getD (shift + p.length) false) shift p.length c).set (shift + p.length) false

@[simp]

theorem Complexity.DepthThreeLowerBound.cancelByUpdates_length (p c : List Bool) (shift : ℕ) : (cancelByUpdates p c shift).length = c.length

theorem Complexity.DepthThreeLowerBound.cancelByUpdates_getD (p c : List Bool) (shift : ℕ) (hbound : shift + p.length < c.length) (k : ℕ) : (cancelByUpdates p c shift).getD k false = if shift + p.length = k then false else c.getD k false ^^ if shift ≤ k ∧ k < shift + p.length then c.getD (shift + p.length) false && p.getD (k - shift) false else false

def Complexity.DepthThreeLowerBound.reduceByUpdates (p : List Bool) : ℕ → List Bool → List Bool

Compute the polynomial remainder through cancellation updates.

Equations

• Complexity.DepthThreeLowerBound.reduceByUpdates p 0 x✝ = x✝
• Complexity.DepthThreeLowerBound.reduceByUpdates p j.succ x✝ = Complexity.DepthThreeLowerBound.reduceByUpdates p j (Complexity.DepthThreeLowerBound.cancelByUpdates p x✝ j)

@[simp]

theorem Complexity.DepthThreeLowerBound.reduceByUpdates_zero (p c : List Bool) : reduceByUpdates p 0 c = c

theorem Complexity.DepthThreeLowerBound.reduceByUpdates_step (p c : List Bool) (s : ℕ) : reduceByUpdates p (s + 1) c = reduceByUpdates p s (cancelByUpdates p c s)

@[simp]

theorem Complexity.DepthThreeLowerBound.reduceByUpdates_length (p c : List Bool) (s : ℕ) : (reduceByUpdates p s c).length = c.length

theorem Complexity.DepthThreeLowerBound.cancelStep_read {r m : ℕ} (p : BitWord r) (a : BitWord m) (shift : ℕ) (hbound : shift + r < m) (i : Fin m) : cancelStep p (shift + r) a i = if shift + r = ↑i then false else a i ^^ if shift ≤ ↑i ∧ ↑i < shift + r then a ⟨shift + r, hbound⟩ && wordGet p (↑i - shift) else false

theorem Complexity.DepthThreeLowerBound.cancelByUpdates_eq_cancelStep {r m : ℕ} (p : BitWord r) (a : BitWord m) (shift : ℕ) (hbound : shift + r < m) : cancelByUpdates (wordList p) (wordList a) shift = wordList (cancelStep p (shift + r) a)

theorem Complexity.DepthThreeLowerBound.reduceLoop_below {r m : ℕ} (p : BitWord r) (k : ℕ) (a : BitWord m) (hk : k ≤ r) : reduceLoop p k a = a

theorem Complexity.DepthThreeLowerBound.reduceByUpdates_word_eq {r m : ℕ} (p : BitWord r) (s : ℕ) (a : BitWord m) (hbound : r + s ≤ m) : reduceByUpdates (wordList p) s (wordList a) = wordList (reduceLoop p (r + s) a)

theorem Complexity.DepthThreeLowerBound.reduceByUpdates_eq_reduceLoop (p c : List Bool) (s : ℕ) (hbound : p.length + s ≤ c.length) : reduceByUpdates p s c = wordList (reduceLoop (listWord p.length p) (p.length + s) (listWord c.length c))

theorem Complexity.DepthThreeLowerBound.reduceByUpdates_tail_false (p c : List Bool) (s : ℕ) (hfull : p.length + s = c.length) (i : ℕ) (hi : p.length ≤ i) : (reduceByUpdates p s c).getD i false = false

theorem Complexity.DepthThreeLowerBound.wordList_wordResize_take {r m : ℕ} (a : BitWord m) (hr : r ≤ m) : wordList (wordResize r a) = List.take r (wordList a)

theorem Complexity.DepthThreeLowerBound.reduceByUpdates_take_eq_wordReduce (p c : List Bool) (hwidth : c.length = p.length + p.length) : List.take p.length (reduceByUpdates p p.length c) = wordList (wordReduce (listWord p.length p) (listWord c.length c))

theorem Complexity.DepthThreeLowerBound.reduceByUpdates_convolve_eq_multiplyBitLists (r : ℕ) (p a b : List Bool) (hp : p.length = r) (ha : a.length = r) (hb : b.length = r) : List.take r (reduceByUpdates p r (convolveBitLists a b)) = multiplyBitLists r p a b

theorem Complexity.DepthThreeLowerBound.reduceByUpdates_convolveByUpdates_eq_multiplyBitLists (r : ℕ) (p a b : List Bool) (hp : p.length = r) (ha : a.length = r) (hb : b.length = r) : List.take r (reduceByUpdates p r (convolveByUpdates a b)) = multiplyBitLists r p a b