Unrestricted depth-three lower bound: language bit convolution updates

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

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

def Complexity.DepthThreeLowerBound.xorListAt (c : List Bool) (k : ℕ) (v : Bool) : List Bool

XOR a bit into a selected list position.

Equations

• Complexity.DepthThreeLowerBound.xorListAt c k v = c.set k (c.getD k false ^^ v)

@[simp]

theorem Complexity.DepthThreeLowerBound.xorListAt_length (c : List Bool) (k : ℕ) (v : Bool) : (xorListAt c k v).length = c.length

theorem Complexity.DepthThreeLowerBound.xorListAt_getD (c : List Bool) (j : ℕ) (v : Bool) (hj : j < c.length) (k : ℕ) : (xorListAt c j v).getD k false = (c.getD k false ^^ if j = k then v else false)

theorem Complexity.DepthThreeLowerBound.xorListAt_split («prefix» suffix : List Bool) (old v : Bool) : xorListAt («prefix» ++ old :: suffix) «prefix».length v = «prefix» ++ (old ^^ v) :: suffix

def Complexity.DepthThreeLowerBound.convolutionUpdateRow (a b : List Bool) (i : ℕ) : List ℕ → List Bool → List Bool

Accumulate one row of bitwise convolution updates.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.DepthThreeLowerBound.convolutionUpdateRow a b i [] x✝ = x✝

@[simp]

theorem Complexity.DepthThreeLowerBound.convolutionUpdateRow_nil (a b : List Bool) (i : ℕ) (c : List Bool) : convolutionUpdateRow a b i [] c = c

theorem Complexity.DepthThreeLowerBound.convolutionUpdateRow_step (a b : List Bool) (i j : ℕ) (js : List ℕ) (c : List Bool) : convolutionUpdateRow a b i (j :: js) c = convolutionUpdateRow a b i js (xorListAt c (i + j) (a.getD i false && b.getD j false))

@[simp]

theorem Complexity.DepthThreeLowerBound.convolutionUpdateRow_length (a b : List Bool) (i : ℕ) (js : List ℕ) (c : List Bool) : (convolutionUpdateRow a b i js c).length = c.length

theorem Complexity.DepthThreeLowerBound.convolutionUpdateRow_getD (a b : List Bool) (i : ℕ) (js : List ℕ) (c : List Bool) (k : ℕ) (hbound : ∀ j ∈ js, i + j < c.length) : (convolutionUpdateRow a b i js c).getD k false = (c.getD k false ^^ xorBits (List.map (fun (j : ℕ) => if i + j = k then a.getD i false && b.getD j false else false) js))

def Complexity.DepthThreeLowerBound.convolutionUpdateRows (a b : List Bool) : List ℕ → List Bool → List Bool

Accumulate all rows of bitwise convolution updates.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.DepthThreeLowerBound.convolutionUpdateRows a b [] x✝ = x✝

@[simp]

theorem Complexity.DepthThreeLowerBound.convolutionUpdateRows_nil (a b c : List Bool) : convolutionUpdateRows a b [] c = c

theorem Complexity.DepthThreeLowerBound.convolutionUpdateRows_step (a b : List Bool) (i : ℕ) (is : List ℕ) (c : List Bool) : convolutionUpdateRows a b (i :: is) c = convolutionUpdateRows a b is (convolutionUpdateRow a b i (List.range b.length) c)

@[simp]

theorem Complexity.DepthThreeLowerBound.convolutionUpdateRows_length (a b : List Bool) (is : List ℕ) (c : List Bool) : (convolutionUpdateRows a b is c).length = c.length

theorem Complexity.DepthThreeLowerBound.convolutionUpdateRows_getD (a b : List Bool) (is : List ℕ) (c : List Bool) (k : ℕ) (hbound : ∀ i ∈ is, ∀ j < b.length, i + j < c.length) : (convolutionUpdateRows a b is c).getD k false = (c.getD k false ^^ xorBits (List.map (fun (i : ℕ) => xorBits (convolutionRow a b i k)) is))

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

Compute bit-list convolution by successive updates.

Equations

• Complexity.DepthThreeLowerBound.convolveByUpdates a b = Complexity.DepthThreeLowerBound.convolutionUpdateRows a b (List.range a.length) (List.replicate (a.length + b.length) false)

@[simp]

theorem Complexity.DepthThreeLowerBound.convolveByUpdates_length (a b : List Bool) : (convolveByUpdates a b).length = a.length + b.length

theorem Complexity.DepthThreeLowerBound.convolutionUpdate_index_lt (a b : List Bool) {i j : ℕ} (hi : i < a.length) (hj : j < b.length) : i + j < a.length + b.length

theorem Complexity.DepthThreeLowerBound.convolveByUpdates_getD (a b : List Bool) (k : ℕ) : (convolveByUpdates a b).getD k false = convolutionBit a b k

theorem Complexity.DepthThreeLowerBound.convolveByUpdates_eq (a b : List Bool) : convolveByUpdates a b = convolveBitLists a b