Unrestricted depth-three lower bound: language bit hash updates

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

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

def Complexity.DepthThreeLowerBound.hashUpdateRow (u x : List Bool) (i : ℕ) : List ℕ → List Bool → List Bool

Accumulate one row of the bit-level hash computation.

Equations

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

@[simp]

theorem Complexity.DepthThreeLowerBound.hashUpdateRow_nil (u x : List Bool) (i : ℕ) (c : List Bool) : hashUpdateRow u x i [] c = c

theorem Complexity.DepthThreeLowerBound.hashUpdateRow_step (u x : List Bool) (i j : ℕ) (js : List ℕ) (c : List Bool) : hashUpdateRow u x i (j :: js) c = hashUpdateRow u x i js (xorListAt c i (u.getD (i + j) false && x.getD j false))

@[simp]

theorem Complexity.DepthThreeLowerBound.hashUpdateRow_length (u x : List Bool) (i : ℕ) (js : List ℕ) (c : List Bool) : (hashUpdateRow u x i js c).length = c.length

theorem Complexity.DepthThreeLowerBound.hashUpdateRow_append (u x : List Bool) (i : ℕ) (js ks : List ℕ) (c : List Bool) : hashUpdateRow u x i (js ++ ks) c = hashUpdateRow u x i ks (hashUpdateRow u x i js c)

theorem Complexity.DepthThreeLowerBound.hashUpdateRow_getD (u x : List Bool) (i : ℕ) (js : List ℕ) (c : List Bool) (k : ℕ) (hi : i < c.length) : (hashUpdateRow u x i js c).getD k false = (c.getD k false ^^ if i = k then xorBits (List.map (fun (j : ℕ) => u.getD (i + j) false && x.getD j false) js) else false)

theorem Complexity.DepthThreeLowerBound.hashUpdateRow_getD_self (u x : List Bool) (i : ℕ) (js : List ℕ) (c : List Bool) (hi : i < c.length) : (hashUpdateRow u x i js c).getD i false = (c.getD i false ^^ xorBits (List.map (fun (j : ℕ) => u.getD (i + j) false && x.getD j false) js))

theorem Complexity.DepthThreeLowerBound.hashUpdateRow_getD_ne (u x : List Bool) (i : ℕ) (js : List ℕ) (c : List Bool) (k : ℕ) (hi : i < c.length) (hik : i ≠ k) : (hashUpdateRow u x i js c).getD k false = c.getD k false

def Complexity.DepthThreeLowerBound.hashRowBit (u x : List Bool) (i : ℕ) : Bool

The bit contributed by one hash row at a selected output coordinate.

Equations

• Complexity.DepthThreeLowerBound.hashRowBit u x i = Complexity.DepthThreeLowerBound.xorBits (List.map (fun (j : ℕ) => u.getD (i + j) false && x.getD j false) (List.range x.length))

def Complexity.DepthThreeLowerBound.hashUpdateRows (u x : List Bool) : List ℕ → List Bool → List Bool

Accumulate the rows of the bit-level hash computation.

Equations

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

@[simp]

theorem Complexity.DepthThreeLowerBound.hashUpdateRows_nil (u x c : List Bool) : hashUpdateRows u x [] c = c

theorem Complexity.DepthThreeLowerBound.hashUpdateRows_step (u x : List Bool) (i : ℕ) (is : List ℕ) (c : List Bool) : hashUpdateRows u x (i :: is) c = hashUpdateRows u x is (hashUpdateRow u x i (List.range x.length) c)

@[simp]

theorem Complexity.DepthThreeLowerBound.hashUpdateRows_length (u x : List Bool) (is : List ℕ) (c : List Bool) : (hashUpdateRows u x is c).length = c.length

theorem Complexity.DepthThreeLowerBound.hashUpdateRows_append (u x : List Bool) (is ks : List ℕ) (c : List Bool) : hashUpdateRows u x (is ++ ks) c = hashUpdateRows u x ks (hashUpdateRows u x is c)

theorem Complexity.DepthThreeLowerBound.hashUpdateRows_getD (u x : List Bool) (is : List ℕ) (c : List Bool) (k : ℕ) (hbound : ∀ i ∈ is, i < c.length) : (hashUpdateRows u x is c).getD k false = (c.getD k false ^^ xorBits (List.map (fun (i : ℕ) => if i = k then hashRowBit u x i else false) is))

theorem Complexity.DepthThreeLowerBound.hashUpdateRow_range'_append (u x : List Bool) (i s m n : ℕ) (c : List Bool) : hashUpdateRow u x i (List.range' s (m + n)) c = hashUpdateRow u x i (List.range' (s + m) n) (hashUpdateRow u x i (List.range' s m) c)

theorem Complexity.DepthThreeLowerBound.hashUpdateRow_range'_prefix (u x : List Bool) (i s m n : ℕ) (c : List Bool) (hm : m ≤ n) : hashUpdateRow u x i (List.range' (s + m) (n - m)) (hashUpdateRow u x i (List.range' s m) c) = hashUpdateRow u x i (List.range' s n) c

theorem Complexity.DepthThreeLowerBound.hashUpdateRow_range'_step (u x : List Bool) (i s n : ℕ) (c : List Bool) : hashUpdateRow u x i (List.range' s (n + 1)) c = hashUpdateRow u x i (List.range' (s + 1) n) (xorListAt c i (u.getD (i + s) false && x.getD s false))

theorem Complexity.DepthThreeLowerBound.hashUpdateRow_range'_snoc (u x : List Bool) (i s n : ℕ) (c : List Bool) : hashUpdateRow u x i (List.range' s (n + 1)) c = xorListAt (hashUpdateRow u x i (List.range' s n) c) i (u.getD (i + (s + n)) false && x.getD (s + n) false)

theorem Complexity.DepthThreeLowerBound.hashUpdateRows_range'_append (u x : List Bool) (s m n : ℕ) (c : List Bool) : hashUpdateRows u x (List.range' s (m + n)) c = hashUpdateRows u x (List.range' (s + m) n) (hashUpdateRows u x (List.range' s m) c)

theorem Complexity.DepthThreeLowerBound.hashUpdateRows_range'_prefix (u x : List Bool) (s m n : ℕ) (c : List Bool) (hm : m ≤ n) : hashUpdateRows u x (List.range' (s + m) (n - m)) (hashUpdateRows u x (List.range' s m) c) = hashUpdateRows u x (List.range' s n) c

theorem Complexity.DepthThreeLowerBound.hashUpdateRows_range'_step (u x : List Bool) (s n : ℕ) (c : List Bool) : hashUpdateRows u x (List.range' s (n + 1)) c = hashUpdateRows u x (List.range' (s + 1) n) (hashUpdateRow u x s (List.range x.length) c)

theorem Complexity.DepthThreeLowerBound.hashUpdateRows_range'_snoc (u x : List Bool) (s n : ℕ) (c : List Bool) : hashUpdateRows u x (List.range' s (n + 1)) c = hashUpdateRow u x (s + n) (List.range x.length) (hashUpdateRows u x (List.range' s n) c)

theorem Complexity.DepthThreeLowerBound.hashUpdateRow_range_succ (u x : List Bool) (i j : ℕ) (c : List Bool) : hashUpdateRow u x i (List.range (j + 1)) c = xorListAt (hashUpdateRow u x i (List.range j) c) i (u.getD (i + j) false && x.getD j false)

theorem Complexity.DepthThreeLowerBound.hashUpdateRows_range_succ (u x : List Bool) (i : ℕ) (c : List Bool) : hashUpdateRows u x (List.range (i + 1)) c = hashUpdateRow u x i (List.range x.length) (hashUpdateRows u x (List.range i) c)

theorem Complexity.DepthThreeLowerBound.hashReadIndex_lt {d r i j : ℕ} (hi : i < r) (hj : j < d) : i + j < d + r - 1

theorem Complexity.DepthThreeLowerBound.hashUpdateRows_getD_nodup (u x : List Bool) (is : List ℕ) (c : List Bool) (k : ℕ) (hbound : ∀ i ∈ is, i < c.length) (hn : is.Nodup) : (hashUpdateRows u x is c).getD k false = (c.getD k false ^^ if k ∈ is then hashRowBit u x k else false)

def Complexity.DepthThreeLowerBound.hashByUpdates (r : ℕ) (u x : List Bool) : List Bool

Compute the binary hash by successive bit-list updates.

Equations

• Complexity.DepthThreeLowerBound.hashByUpdates r u x = Complexity.DepthThreeLowerBound.hashUpdateRows u x (List.range r) (List.replicate r false)

@[simp]

theorem Complexity.DepthThreeLowerBound.hashByUpdates_length (r : ℕ) (u x : List Bool) : (hashByUpdates r u x).length = r

theorem Complexity.DepthThreeLowerBound.hashByUpdates_getD (r : ℕ) (u x : List Bool) (k : ℕ) : (hashByUpdates r u x).getD k false = if k < r then hashRowBit u x k else false

theorem Complexity.DepthThreeLowerBound.hashRowBit_ofFn {d r : ℕ} (u : BitWord (d + r - 1)) (x : BitWord d) (i : Fin r) : hashRowBit (List.ofFn u) (List.ofFn x) ↑i = wordHash u x i

theorem Complexity.DepthThreeLowerBound.hashByUpdates_ofFn_eq {d r : ℕ} (u : BitWord (d + r - 1)) (x : BitWord d) : hashByUpdates r (List.ofFn u) (List.ofFn x) = List.ofFn (wordHash u x)