Unrestricted depth-three lower bound: hard slice probability

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

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

noncomputable def Complexity.DepthThreeLowerBound.hardSliceSparseConstant (b : ℕ) (hb : 1 ≤ b) : ℕ

The sparse-family constant used in the hard-slice existence argument.

Equations

• Complexity.DepthThreeLowerBound.hardSliceSparseConstant b hb = Classical.choose ⋯

theorem Complexity.DepthThreeLowerBound.hardSliceSparseConstant_pos (b : ℕ) (hb : 1 ≤ b) : 0 < hardSliceSparseConstant b hb

theorem Complexity.DepthThreeLowerBound.hardSliceSparseConstant_spec (b : ℕ) (hb : 1 ≤ b) (V : Type) [Fintype V] [DecidableEq V] (G : Cube V → ℝ) (htests : ∀ (H : CNF V), H.Normalized → H.WidthAtMost b → List.length H ≤ hardSliceSparseConstant b hb * Fintype.card V → |finiteAvg fun (x : Cube V) => G x * indicator (H.eval x)| ≤ 2 ^ (-↑(Fintype.card V) / 4)) : corr b G ≤ 2 ^ (-↑(Fintype.card V) / 8)

theorem Complexity.DepthThreeLowerBound.sparseMomentBound_nonneg (m b L h : ℕ) (δ : ℝ) : 0 ≤ sparseMomentBound m b L h δ

theorem Complexity.DepthThreeLowerBound.coefficient_corr_failure_le {F V : Type} [Field F] [Module BinaryAlgebra.F2 F] [Fintype F] [Fintype V] (ell : F →ₗ[BinaryAlgebra.F2] BinaryAlgebra.F2) (hOne : ell 1 = 1) (a : Cube V → F) (ha : Function.Injective a) (b : ℕ) (hb : 1 ≤ b) (h : ℕ) (hh : 0 < h) : (finiteProb fun (β : Fin (2 * h) → F) => ¬(corr b fun (x : Cube V) => sign (Interpolation.acceptEval ell (2 * h) a β x)) ≤ 2 ^ (-↑(Fintype.card V) / 8)) ≤ sparseMomentBound (Fintype.card V) b (hardSliceSparseConstant b hb * Fintype.card V) h (2 ^ (-↑(Fintype.card V) / 4))

theorem Complexity.DepthThreeLowerBound.hash_coefficient_corr_failure_le {F V U : Type} [Field F] [Module BinaryAlgebra.F2 F] [Fintype F] [Fintype V] [Fintype U] [Nonempty U] (ell : F →ₗ[BinaryAlgebra.F2] BinaryAlgebra.F2) (hOne : ell 1 = 1) (a : U → Cube V → F) (b : ℕ) (hb : 1 ≤ b) (h : ℕ) (hh : 0 < h) : (finiteProb fun (ω : U × (Fin (2 * h) → F)) => ¬(corr b fun (x : Cube V) => sign (Interpolation.acceptEval ell (2 * h) (a ω.1) ω.2 x)) ≤ 2 ^ (-↑(Fintype.card V) / 8)) ≤ (finiteProb fun (u : U) => ¬Function.Injective (a u)) + sparseMomentBound (Fintype.card V) b (hardSliceSparseConstant b hb * Fintype.card V) h (2 ^ (-↑(Fintype.card V) / 4))

noncomputable def Complexity.DepthThreeLowerBound.encodedHash {d r : ℕ} (p : Fin r → Bool) (u : Fin (d + r - 1) → Bool) (x : Cube (Fin d)) : BinaryAlgebra.BitQuotient p

Hash the data and encode the result in the polynomial quotient.

Equations

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

theorem Complexity.DepthThreeLowerBound.encodedHash_fill_injective {d r : ℕ} (p : Fin r → Bool) (u : Fin (d + r - 1) → Bool) (σ : Restriction (Fin d)) (hu : Function.Injective fun (z : Cube (Live σ)) => BinaryHash.hashBool u (fill σ z)) : Function.Injective fun (z : Cube (Live σ)) => encodedHash p u (fill σ z)

noncomputable def Complexity.DepthThreeLowerBound.hashAcceptance {d r : ℕ} (p : Fin r → Bool) [Fact (Irreducible (BinaryAlgebra.inputPolynomialBits p))] (t : ℕ) (u : Fin (d + r - 1) → Bool) (β : Fin t → BinaryAlgebra.BitQuotient p) : Cube (Fin d) → Bool

Evaluate the acceptance bit determined by a hash output.

Equations

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

theorem Complexity.DepthThreeLowerBound.actual_hash_coefficient_failure_le {d r : ℕ} (p : Fin r → Bool) [Fact (Irreducible (BinaryAlgebra.inputPolynomialBits p))] (hr : 0 < r) (σ : Restriction (Fin d)) (b : ℕ) (hb : 1 ≤ b) (h : ℕ) (hh : 0 < h) : (finiteProb fun (ω : (Fin (d + r - 1) → Bool) × (Fin (2 * h) → BinaryAlgebra.BitQuotient p)) => ¬(corr b fun (z : Cube (Live σ)) => sign (hashAcceptance p (2 * h) ω.1 ω.2 (fill σ z))) ≤ 2 ^ (-↑(Fintype.card (Live σ)) / 8)) ≤ 2 ^ Fintype.card (Live σ) / 2 ^ r + sparseMomentBound (Fintype.card (Live σ)) b (hardSliceSparseConstant b hb * Fintype.card (Live σ)) h (2 ^ (-↑(Fintype.card (Live σ)) / 4))