Documentation

Complexitylib.Circuits.DepthThree.LowerBound.Internal.HardSliceExistence

Unrestricted depth-three lower bound: hard slice existence #

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

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

source
theorem Complexity.DepthThreeLowerBound.actual_hash_coefficient_window_failure_le {d r h b : ℕ} (p : Fin r → Bool) [Fact (Irreducible (BinaryAlgebra.inputPolynomialBits p))] (hr : 0 < r) (hb : 1 ≤ b) (hh : 0 < h) (q : ℝ) (σ : Restriction (Fin d)) (hσ : restrictionWindow q σ) (hbound : 2 ^ Fintype.card (Live σ) / 2 ^ r + sparseMomentBound (Fintype.card (Live σ)) b (hardSliceSparseConstant b hb * Fintype.card (Live σ)) h (2 ^ (-↑(Fintype.card (Live σ)) / 4)) ≤ 2 * 2 ^ (-(q * ↑d) / 16)) :
(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 ^ (-(q * ↑d) / 16)) ≤ 2 * 2 ^ (-(q * ↑d) / 16)
source
theorem Complexity.DepthThreeLowerBound.exists_good_hash_coefficients {d r h b : ℕ} (p : Fin r → Bool) [Fact (Irreducible (BinaryAlgebra.inputPolynomialBits p))] (hr : 0 < r) (hb : 1 ≤ b) (hh : 0 < h) (q : ℝ) (hq : 0 ≤ q) (hq1 : q ≤ 1) (hbound : ∀ (m : ℕ), q * ↑d / 2 ≤ ↑m → ↑m ≤ 2 * (q * ↑d) → 2 ^ m / 2 ^ r + sparseMomentBound m b (hardSliceSparseConstant b hb * m) h (2 ^ (-↑m / 4)) ≤ 2 * 2 ^ (-(q * ↑d) / 16)) :
∃ (u : Fin (d + r - 1) → Bool) (β : Fin (2 * h) → BinaryAlgebra.BitQuotient p), (restrictionAvg q fun (σ : Restriction (Fin d)) => if ¬goodRestriction q (2 ^ (-(q * ↑d) / 16)) b (hashAcceptance p (2 * h) u β) σ then 1 else 0) ≤ 4 * 2 ^ (-(q * ↑d) / 16)
source
noncomputable def Complexity.DepthThreeLowerBound.coefficientInputBits {r t : ℕ} (p : Fin r → Bool) (β : Fin t → BinaryAlgebra.BitQuotient p) :
Fin t → Fin r → Bool

Assemble coefficient bit blocks for a chosen hard slice.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem Complexity.DepthThreeLowerBound.encode_coefficientInputBits {r t : ℕ} (p : Fin r → Bool) (β : Fin t → BinaryAlgebra.BitQuotient p) (j : Fin t) :
    (BinaryAlgebra.encode (fun (i : Fin r) => BinaryAlgebra.bitValue (p i)) fun (i : Fin r) => BinaryAlgebra.bitValue (coefficientInputBits p β j i)) = β j
    source
    theorem Complexity.DepthThreeLowerBound.hashAcceptance_coefficientInputBits {d r t : ℕ} (p : Fin r → Bool) [Fact (Irreducible (BinaryAlgebra.inputPolynomialBits p))] (u : Fin (d + r - 1) → Bool) (β : Fin t → BinaryAlgebra.BitQuotient p) :
    (hashAcceptance p t u fun (j : Fin t) => BinaryAlgebra.encode (fun (i : Fin r) => BinaryAlgebra.bitValue (p i)) fun (i : Fin r) => BinaryAlgebra.bitValue (coefficientInputBits p β j i)) = hashAcceptance p t u β