Unrestricted depth-three lower bound: language bit loop invariants

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

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

def Complexity.DepthThreeLowerBound.xorScan : Bool → List Bool → Bool

Scan a bit list while applying the specified XOR update.

Equations

• Complexity.DepthThreeLowerBound.xorScan x✝ [] = x✝
• Complexity.DepthThreeLowerBound.xorScan x✝ (b :: bs) = Complexity.DepthThreeLowerBound.xorScan (x✝ ^^ b) bs

@[simp]

theorem Complexity.DepthThreeLowerBound.xorScan_nil (acc : Bool) : xorScan acc [] = acc

theorem Complexity.DepthThreeLowerBound.xorScan_step (acc b : Bool) (bs : List Bool) : xorScan acc (b :: bs) = xorScan (acc ^^ b) bs

theorem Complexity.DepthThreeLowerBound.xorScan_eq (acc : Bool) (bs : List Bool) : xorScan acc bs = (acc ^^ xorBits bs)

theorem Complexity.DepthThreeLowerBound.xorBits_append (a b : List Bool) : xorBits (a ++ b) = (xorBits a ^^ xorBits b)

theorem Complexity.DepthThreeLowerBound.xorScan_prefix_invariant (done todo : List Bool) : xorScan (xorBits done) todo = xorBits (done ++ todo)

theorem Complexity.DepthThreeLowerBound.ofFn_nat_eq_map_range {α : Type uDepth1} (n : ℕ) (f : ℕ → α) : (List.ofFn fun (i : Fin n) => f ↑i) = List.map f (List.range n)

def Complexity.DepthThreeLowerBound.convolutionRow (a b : List Bool) (i k : ℕ) : List Bool

The partial convolution after processing one input row.

Equations

• Complexity.DepthThreeLowerBound.convolutionRow a b i k = List.map (fun (j : ℕ) => if i + j = k then a.getD i false && b.getD j false else false) (List.range b.length)

def Complexity.DepthThreeLowerBound.convolutionRows (a b : List Bool) (k : ℕ) : List Bool

The convolution accumulator after processing successive rows.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.DepthThreeLowerBound.convolutionBit (a b : List Bool) (k : ℕ) : Bool

The contribution of the input bit pair to the convolution accumulator.

Equations

• Complexity.DepthThreeLowerBound.convolutionBit a b k = Complexity.DepthThreeLowerBound.xorBits (Complexity.DepthThreeLowerBound.convolutionRows a b k)

theorem Complexity.DepthThreeLowerBound.convolutionRow_scan (a b : List Bool) (i k : ℕ) : xorScan false (convolutionRow a b i k) = xorBits (convolutionRow a b i k)

theorem Complexity.DepthThreeLowerBound.convolutionRows_scan (a b : List Bool) (k : ℕ) : xorScan false (convolutionRows a b k) = convolutionBit a b k

theorem Complexity.DepthThreeLowerBound.convolutionBit_eq_wordConvolve (a b : List Bool) (k : ℕ) (hk : k < a.length + b.length) : convolutionBit a b k = wordConvolve (listWord a.length a) (listWord b.length b) ⟨k, hk⟩

def Complexity.DepthThreeLowerBound.convolveBitLists (a b : List Bool) : List Bool

Compute the convolution of two polynomial coefficient lists.

Equations

• Complexity.DepthThreeLowerBound.convolveBitLists a b = List.map (Complexity.DepthThreeLowerBound.convolutionBit a b) (List.range (a.length + b.length))

@[simp]

theorem Complexity.DepthThreeLowerBound.convolveBitLists_length (a b : List Bool) : (convolveBitLists a b).length = a.length + b.length

theorem Complexity.DepthThreeLowerBound.convolveBitLists_eq (a b : List Bool) : convolveBitLists a b = wordList (wordConvolve (listWord a.length a) (listWord b.length b))

theorem Complexity.DepthThreeLowerBound.hornerBitLists_nil (r : ℕ) (p h : List Bool) : hornerBitLists r p h [] = wordList fun (x : Fin r) => false

theorem Complexity.DepthThreeLowerBound.hornerBitLists_cons (r : ℕ) (p h b : List Bool) (bs : List (List Bool)) : hornerBitLists r p h (b :: bs) = wordList (wordXor (listWord r b) (wordMulMod (listWord r p) (listWord r h) (listWord r (hornerBitLists r p h bs))))