Unrestricted depth-three lower bound: interpolation signs

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

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

def Complexity.DepthThreeLowerBound.Interpolation.bitEval {F : Type uDepth1} {ι : Type uDepth2} [Field F] [Module BinaryAlgebra.F2 F] (ell : F →ₗ[BinaryAlgebra.F2] BinaryAlgebra.F2) (t : ℕ) (a : ι → F) : (Fin t → F) →+ ι → BinaryAlgebra.F2

Read a Boolean coordinate of polynomial evaluation.

Equations

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

@[simp]

theorem Complexity.DepthThreeLowerBound.Interpolation.bitEval_apply {F : Type uDepth1} {ι : Type uDepth2} [Field F] [Module BinaryAlgebra.F2 F] (ell : F →ₗ[BinaryAlgebra.F2] BinaryAlgebra.F2) (t : ℕ) (a : ι → F) (β : Fin t → F) (i : ι) : (bitEval ell t a) β i = ell (∑ j : Fin t, β j * a i ^ ↑j)

theorem Complexity.DepthThreeLowerBound.Interpolation.functional_surjective {F : Type uDepth1} [Field F] [Module BinaryAlgebra.F2 F] (ell : F →ₗ[BinaryAlgebra.F2] BinaryAlgebra.F2) (hOne : ell 1 = 1) : Function.Surjective ⇑ell

theorem Complexity.DepthThreeLowerBound.Interpolation.bitEval_surjective {F : Type uDepth1} {ι : Type uDepth2} [Field F] [Module BinaryAlgebra.F2 F] [Fintype ι] (ell : F →ₗ[BinaryAlgebra.F2] BinaryAlgebra.F2) (hOne : ell 1 = 1) {t : ℕ} (a : ι → F) (hsize : Fintype.card ι ≤ t) (ha : Function.Injective a) : Function.Surjective ⇑(bitEval ell t a)

def Complexity.DepthThreeLowerBound.Interpolation.coefficientBits {F : Type uDepth1} {ι : Type uDepth2} [Field F] [Module BinaryAlgebra.F2 F] (ell : F →ₗ[BinaryAlgebra.F2] BinaryAlgebra.F2) (t : ℕ) (a : ι → F) (β : Fin t → F) : ι → Bool

Express polynomial coefficients as Boolean bit blocks.

Equations

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

def Complexity.DepthThreeLowerBound.Interpolation.acceptEval {F : Type uDepth1} {ι : Type uDepth2} [Field F] [Module BinaryAlgebra.F2 F] (ell : F →ₗ[BinaryAlgebra.F2] BinaryAlgebra.F2) (t : ℕ) (a : ι → F) (β : Fin t → F) : ι → Bool

The acceptance bit extracted from polynomial evaluation.

Equations

• Complexity.DepthThreeLowerBound.Interpolation.acceptEval ell t a β i = !Complexity.DepthThreeLowerBound.Interpolation.coefficientBits ell t a β i

@[simp]

theorem Complexity.DepthThreeLowerBound.Interpolation.acceptEval_eq_true {F : Type uDepth1} {ι : Type uDepth2} [Field F] [Module BinaryAlgebra.F2 F] (ell : F →ₗ[BinaryAlgebra.F2] BinaryAlgebra.F2) (t : ℕ) (a : ι → F) (β : Fin t → F) (i : ι) : acceptEval ell t a β i = true ↔ ell (∑ j : Fin t, β j * a i ^ ↑j) = 0

def Complexity.DepthThreeLowerBound.Interpolation.complementEquiv (ι : Type uDepth3) : (ι → Bool) ≃ (ι → Bool)

The coefficient involution that complements the acceptance bit.

Equations

• Complexity.DepthThreeLowerBound.Interpolation.complementEquiv ι = { toFun := fun (b : ι → Bool) (i : ι) => !b i, invFun := fun (b : ι → Bool) (i : ι) => !b i, left_inv := ⋯, right_inv := ⋯ }

theorem Complexity.DepthThreeLowerBound.Interpolation.finiteAvg_bitEval {F : Type uDepth1} {ι : Type uDepth2} [Field F] [Module BinaryAlgebra.F2 F] [Fintype F] [Fintype ι] [DecidableEq ι] (ell : F →ₗ[BinaryAlgebra.F2] BinaryAlgebra.F2) (hOne : ell 1 = 1) {t : ℕ} (a : ι → F) (hsize : Fintype.card ι ≤ t) (ha : Function.Injective a) (Φ : (ι → BinaryAlgebra.F2) → ℝ) : (finiteAvg fun (β : Fin t → F) => Φ ((bitEval ell t a) β)) = finiteAvg Φ

theorem Complexity.DepthThreeLowerBound.Interpolation.finiteAvg_coefficientBits {F : Type uDepth1} {ι : Type uDepth2} [Field F] [Module BinaryAlgebra.F2 F] [Fintype F] [Fintype ι] [DecidableEq ι] (ell : F →ₗ[BinaryAlgebra.F2] BinaryAlgebra.F2) (hOne : ell 1 = 1) {t : ℕ} (a : ι → F) (hsize : Fintype.card ι ≤ t) (ha : Function.Injective a) (Φ : (ι → Bool) → ℝ) : (finiteAvg fun (β : Fin t → F) => Φ (coefficientBits ell t a β)) = finiteAvg Φ

theorem Complexity.DepthThreeLowerBound.Interpolation.finiteAvg_acceptEval {F : Type uDepth1} {ι : Type uDepth2} [Field F] [Module BinaryAlgebra.F2 F] [Fintype F] [Fintype ι] [DecidableEq ι] (ell : F →ₗ[BinaryAlgebra.F2] BinaryAlgebra.F2) (hOne : ell 1 = 1) {t : ℕ} (a : ι → F) (hsize : Fintype.card ι ≤ t) (ha : Function.Injective a) (Φ : (ι → Bool) → ℝ) : (finiteAvg fun (β : Fin t → F) => Φ (acceptEval ell t a β)) = finiteAvg Φ

theorem Complexity.DepthThreeLowerBound.Interpolation.card_bitEval_fiber_mul {F : Type uDepth1} {ι : Type uDepth2} [Field F] [Module BinaryAlgebra.F2 F] [Fintype F] [Fintype ι] (ell : F →ₗ[BinaryAlgebra.F2] BinaryAlgebra.F2) (hOne : ell 1 = 1) {t : ℕ} (a : ι → F) (hsize : Fintype.card ι ≤ t) (ha : Function.Injective a) (b : ι → BinaryAlgebra.F2) : 2 ^ Fintype.card ι * Fintype.card { β : Fin t → F // (bitEval ell t a) β = b } = Fintype.card F ^ t

theorem Complexity.DepthThreeLowerBound.Interpolation.card_bitEval_fiber {F : Type uDepth1} {ι : Type uDepth2} [Field F] [Module BinaryAlgebra.F2 F] [Fintype F] [Fintype ι] (ell : F →ₗ[BinaryAlgebra.F2] BinaryAlgebra.F2) (hOne : ell 1 = 1) {t : ℕ} (a : ι → F) (hsize : Fintype.card ι ≤ t) (ha : Function.Injective a) {r : ℕ} (hr : 1 ≤ r) (hcard : Fintype.card F = 2 ^ r) (b : ι → BinaryAlgebra.F2) : Fintype.card { β : Fin t → F // (bitEval ell t a) β = b } = 2 ^ (r * t - Fintype.card ι)

theorem Complexity.DepthThreeLowerBound.Interpolation.finiteAvg_acceptEval_finset {F : Type uDepth1} [Field F] [Module BinaryAlgebra.F2 F] [Fintype F] {Z : Type uDepth4} [DecidableEq Z] (ell : F →ₗ[BinaryAlgebra.F2] BinaryAlgebra.F2) (hOne : ell 1 = 1) {t : ℕ} (a : Z → F) (s : Finset Z) (hsize : s.card ≤ t) (ha : Set.InjOn a ↑s) (Φ : (↥s → Bool) → ℝ) : (finiteAvg fun (β : Fin t → F) => Φ fun (z : ↥s) => acceptEval ell t a β ↑z) = finiteAvg Φ