Unrestricted depth-three lower bound: hash affine

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

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

@[reducible, inline]

abbrev Complexity.DepthThreeLowerBound.BinaryHash.OutsideData {d : ℕ} (T : Finset (Fin d)) : Type

Assignments to coordinates outside a specified set.

Equations

• Complexity.DepthThreeLowerBound.BinaryHash.OutsideData T = ({ i : Fin d // i ∉ T } → Complexity.DepthThreeLowerBound.BinaryHash.F2)

def Complexity.DepthThreeLowerBound.BinaryHash.coordinateCube {d : ℕ} (T : Finset (Fin d)) (rho : OutsideData T) : Set (Data d)

Assignments restricted to a specified coordinate set.

Equations

• Complexity.DepthThreeLowerBound.BinaryHash.coordinateCube T rho = {x : Complexity.DepthThreeLowerBound.BinaryHash.Data d | ∀ (i : Fin d) (hi : i ∉ T), x i = rho ⟨i, hi⟩}

def Complexity.DepthThreeLowerBound.BinaryHash.SupportedOn {d : ℕ} (T : Finset (Fin d)) (w : Data d) : Prop

A vector is zero outside the specified coordinate set.

Equations

• Complexity.DepthThreeLowerBound.BinaryHash.SupportedOn T w = ∀ i ∉ T, w i = 0

def Complexity.DepthThreeLowerBound.BinaryHash.coordinateCubeExtend {d : ℕ} (T : Finset (Fin d)) (rho : OutsideData T) (z : ↥T → F2) : Data d

Extend an assignment on selected coordinates by zero outside them.

Equations

• Complexity.DepthThreeLowerBound.BinaryHash.coordinateCubeExtend T rho z i = if hi : i ∈ T then z ⟨i, hi⟩ else rho ⟨i, hi⟩

theorem Complexity.DepthThreeLowerBound.BinaryHash.coordinateCubeExtend_mem {d : ℕ} (T : Finset (Fin d)) (rho : OutsideData T) (z : ↥T → F2) : coordinateCubeExtend T rho z ∈ coordinateCube T rho

def Complexity.DepthThreeLowerBound.BinaryHash.coordinateCubeEquiv {d : ℕ} (T : Finset (Fin d)) (rho : OutsideData T) : ↑(coordinateCube T rho) ≃ (↥T → F2)

Identify selected-coordinate assignments with their extended vectors.

Equations

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

def Complexity.DepthThreeLowerBound.BinaryHash.supportedDataEquiv {d : ℕ} (T : Finset (Fin d)) : { w : Data d // SupportedOn T w } ≃ (↥T → F2)

Identify supported data vectors with assignments on their support.

Equations

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

@[simp]

theorem Complexity.DepthThreeLowerBound.BinaryHash.supportedOn_zero {d : ℕ} (T : Finset (Fin d)) : SupportedOn T 0

theorem Complexity.DepthThreeLowerBound.BinaryHash.supportedOn_sub_of_mem {d : ℕ} {T : Finset (Fin d)} {rho : OutsideData T} {x y : Data d} (hx : x ∈ coordinateCube T rho) (hy : y ∈ coordinateCube T rho) : SupportedOn T (x - y)

theorem Complexity.DepthThreeLowerBound.BinaryHash.add_mem_coordinateCube {d : ℕ} {T : Finset (Fin d)} {rho : OutsideData T} {x w : Data d} (hx : x ∈ coordinateCube T rho) (hw : SupportedOn T w) : x + w ∈ coordinateCube T rho

theorem Complexity.DepthThreeLowerBound.BinaryHash.not_injOn_coordinateCube_iff {d r : ℕ} (u : Seed d r) (T : Finset (Fin d)) (rho : OutsideData T) : ¬Set.InjOn (hashF2 u) (coordinateCube T rho) ↔ ∃ (w : Data d), SupportedOn T w ∧ w ≠ 0 ∧ hashF2 u w = 0

theorem Complexity.DepthThreeLowerBound.BinaryHash.not_injOn_coordinateCube_iff_of_outside {d r : ℕ} (u : Seed d r) (T : Finset (Fin d)) (rho sigma : OutsideData T) : ¬Set.InjOn (hashF2 u) (coordinateCube T rho) ↔ ¬Set.InjOn (hashF2 u) (coordinateCube T sigma)

noncomputable def Complexity.DepthThreeLowerBound.BinaryHash.supportedVectors {d : ℕ} (T : Finset (Fin d)) : Finset (Data d)

The finite set of vectors supported on the selected coordinates.

Equations

• Complexity.DepthThreeLowerBound.BinaryHash.supportedVectors T = Finset.filter (Complexity.DepthThreeLowerBound.BinaryHash.SupportedOn T) Finset.univ

@[simp]

theorem Complexity.DepthThreeLowerBound.BinaryHash.mem_supportedVectors {d : ℕ} (T : Finset (Fin d)) (w : Data d) : w ∈ supportedVectors T ↔ SupportedOn T w

theorem Complexity.DepthThreeLowerBound.BinaryHash.supportedVectors_card {d : ℕ} (T : Finset (Fin d)) : (supportedVectors T).card = 2 ^ T.card

noncomputable def Complexity.DepthThreeLowerBound.BinaryHash.nonzeroSupportedVectors {d : ℕ} (T : Finset (Fin d)) : Finset (Data d)

The nonzero vectors supported on the selected coordinates.

Equations

• Complexity.DepthThreeLowerBound.BinaryHash.nonzeroSupportedVectors T = (Complexity.DepthThreeLowerBound.BinaryHash.supportedVectors T).erase 0

@[simp]

theorem Complexity.DepthThreeLowerBound.BinaryHash.mem_nonzeroSupportedVectors {d : ℕ} (T : Finset (Fin d)) (w : Data d) : w ∈ nonzeroSupportedVectors T ↔ SupportedOn T w ∧ w ≠ 0

theorem Complexity.DepthThreeLowerBound.BinaryHash.nonzeroSupportedVectors_card {d : ℕ} (T : Finset (Fin d)) : (nonzeroSupportedVectors T).card = 2 ^ T.card - 1

def Complexity.DepthThreeLowerBound.BinaryHash.kernelSeeds {d r : ℕ} (w : Data d) : Finset (Seed d r)

Seeds whose hash sends the specified vector to zero.

Equations

• Complexity.DepthThreeLowerBound.BinaryHash.kernelSeeds w = {u : Complexity.DepthThreeLowerBound.BinaryHash.Seed d r | Complexity.DepthThreeLowerBound.BinaryHash.hashF2 u w = 0}

@[simp]

theorem Complexity.DepthThreeLowerBound.BinaryHash.mem_kernelSeeds {d r : ℕ} (w : Data d) (u : Seed d r) : u ∈ kernelSeeds w ↔ hashF2 u w = 0

theorem Complexity.DepthThreeLowerBound.BinaryHash.kernelSeeds_card {d r : ℕ} (w : Data d) (hw : w ≠ 0) : (kernelSeeds w).card = 2 ^ (d - 1)

noncomputable def Complexity.DepthThreeLowerBound.BinaryHash.badSeeds {d r : ℕ} (T : Finset (Fin d)) (rho : OutsideData T) : Finset (Seed d r)

Seeds admitting a nonzero supported vector in the hash kernel.

Equations

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

@[simp]

theorem Complexity.DepthThreeLowerBound.BinaryHash.mem_badSeeds {d r : ℕ} (T : Finset (Fin d)) (rho : OutsideData T) (u : Seed d r) : u ∈ badSeeds T rho ↔ ¬Set.InjOn (hashF2 u) (coordinateCube T rho)

theorem Complexity.DepthThreeLowerBound.BinaryHash.badSeeds_eq_biUnion {d r : ℕ} (T : Finset (Fin d)) (rho : OutsideData T) : badSeeds T rho = (nonzeroSupportedVectors T).biUnion fun (w : Data d) => kernelSeeds w

theorem Complexity.DepthThreeLowerBound.BinaryHash.badSeeds_eq_of_outside {d r : ℕ} (T : Finset (Fin d)) (rho sigma : OutsideData T) : badSeeds T rho = badSeeds T sigma

theorem Complexity.DepthThreeLowerBound.BinaryHash.badSeeds_card_le {d r : ℕ} (T : Finset (Fin d)) (rho : OutsideData T) : (badSeeds T rho).card ≤ (2 ^ T.card - 1) * 2 ^ (d - 1)

theorem Complexity.DepthThreeLowerBound.BinaryHash.injOn_coordinateCube_empty {d r : ℕ} (u : Seed d r) (rho : OutsideData ∅) : Set.InjOn (hashF2 u) (coordinateCube ∅ rho)

@[simp]

theorem Complexity.DepthThreeLowerBound.BinaryHash.badSeeds_empty {d r : ℕ} (rho : OutsideData ∅) : badSeeds ∅ rho = ∅

theorem Complexity.DepthThreeLowerBound.BinaryHash.badSeeds_card_eq_zero_of_card_eq_zero {d r : ℕ} (T : Finset (Fin d)) (rho : OutsideData T) (hT : T.card = 0) : (badSeeds T rho).card = 0

@[simp]

theorem Complexity.DepthThreeLowerBound.BinaryHash.badSeeds_zero_data {r : ℕ} (T : Finset (Fin 0)) (rho : OutsideData T) : badSeeds T rho = ∅

theorem Complexity.DepthThreeLowerBound.BinaryHash.injOn_coordinateCube_zero_output_iff {d : ℕ} (u : Seed d 0) (T : Finset (Fin d)) (rho : OutsideData T) : Set.InjOn (hashF2 u) (coordinateCube T rho) ↔ T = ∅

theorem Complexity.DepthThreeLowerBound.BinaryHash.badSeeds_zero_output {d : ℕ} (T : Finset (Fin d)) (rho : OutsideData T) : badSeeds T rho = if T = ∅ then ∅ else Finset.univ