Unrestricted depth-three lower bound: hash probability

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

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

theorem Complexity.DepthThreeLowerBound.finiteProb_eq_card_div {Ω : Type uDepth1} [Fintype Ω] (P : Ω → Prop) : finiteProb P = ↑(Fintype.card { ω : Ω // P ω }) / ↑(Fintype.card Ω)

theorem Complexity.DepthThreeLowerBound.BinaryHash.hashBool_fiber_probability {d r : ℕ} (x : Fin d → Bool) (hx : x ≠ fun (x : Fin d) => false) (a : Fin r → Bool) : (finiteProb fun (u : Fin (d + r - 1) → Bool) => hashBool u x = a) = (2 ^ r)⁻¹

theorem Complexity.DepthThreeLowerBound.BinaryHash.hashBool_collision_probability {d r : ℕ} (x y : Fin d → Bool) (hxy : x ≠ y) : (finiteProb fun (u : Fin (d + r - 1) → Bool) => hashBool u x = hashBool u y) = (2 ^ r)⁻¹

theorem Complexity.DepthThreeLowerBound.BinaryHash.hashBool_badSeed_probability_le {d r : ℕ} (T : Finset (Fin d)) (rho : { i : Fin d // i ∉ T } → Bool) : (finiteProb fun (u : Fin (d + r - 1) → Bool) => ¬Set.InjOn (hashBool u) (boolCoordinateCube T rho)) ≤ (2 ^ T.card - 1) / 2 ^ r

theorem Complexity.DepthThreeLowerBound.BinaryHash.hashBool_badSeed_probability_le_pow {d r : ℕ} (T : Finset (Fin d)) (rho : { i : Fin d // i ∉ T } → Bool) : (finiteProb fun (u : Fin (d + r - 1) → Bool) => ¬Set.InjOn (hashBool u) (boolCoordinateCube T rho)) ≤ 2 ^ T.card / 2 ^ r

def Complexity.DepthThreeLowerBound.BinaryHash.restrictionFixed {d : ℕ} (σ : Restriction (Fin d)) : { i : Fin d // i ∉ liveSet σ } → Bool

The fixed-coordinate contribution of a restriction to a linear hash.

Equations

• Complexity.DepthThreeLowerBound.BinaryHash.restrictionFixed σ i = (σ ↑i).getD false

theorem Complexity.DepthThreeLowerBound.BinaryHash.fill_mem_boolCoordinateCube {d : ℕ} (σ : Restriction (Fin d)) (z : Cube (Live σ)) : fill σ z ∈ boolCoordinateCube (liveSet σ) (restrictionFixed σ)

theorem Complexity.DepthThreeLowerBound.BinaryHash.range_fill_eq_boolCoordinateCube {d : ℕ} (σ : Restriction (Fin d)) : Set.range (fill σ) = boolCoordinateCube (liveSet σ) (restrictionFixed σ)

theorem Complexity.DepthThreeLowerBound.BinaryHash.fill_injective {d : ℕ} (σ : Restriction (Fin d)) : Function.Injective (fill σ)

theorem Complexity.DepthThreeLowerBound.BinaryHash.hashBool_fill_injective_iff {d r : ℕ} (σ : Restriction (Fin d)) (u : Fin (d + r - 1) → Bool) : (Function.Injective fun (z : Cube (Live σ)) => hashBool u (fill σ z)) ↔ Set.InjOn (hashBool u) (boolCoordinateCube (liveSet σ) (restrictionFixed σ))

theorem Complexity.DepthThreeLowerBound.BinaryHash.card_liveSet {d : ℕ} (σ : Restriction (Fin d)) : (liveSet σ).card = Fintype.card (Live σ)

theorem Complexity.DepthThreeLowerBound.BinaryHash.hashBool_restriction_failure_le {d r : ℕ} (σ : Restriction (Fin d)) : (finiteProb fun (u : Fin (d + r - 1) → Bool) => ¬Function.Injective fun (z : Cube (Live σ)) => hashBool u (fill σ z)) ≤ (2 ^ Fintype.card (Live σ) - 1) / 2 ^ r

theorem Complexity.DepthThreeLowerBound.BinaryHash.hashBool_restriction_failure_le_pow {d r : ℕ} (σ : Restriction (Fin d)) : (finiteProb fun (u : Fin (d + r - 1) → Bool) => ¬Function.Injective fun (z : Cube (Live σ)) => hashBool u (fill σ z)) ≤ 2 ^ Fintype.card (Live σ) / 2 ^ r