Depth-three lower bounds for the explicit hard family -- proofs

Internal proofs for Complexitylib.Circuits.DepthThree.Explicit.

The explicit family Algebraic.Cutwidth.Extractor.sourceReductionHardFamily satisfies the frontier method's hypotheses: its accepted sets are eventually K-rectangle-free with log K = o(n) and accept half of the cube. A K-rectangle-free set contains no subcube of dimension 2 ⌈log₂ K⌉ = o(n). On inputs of positive length the family is balanced padding, f(x) = g(x_1, …, x_{n-1}) ⊕ x_0, so flipping the first input bit exchanges accepted and rejected inputs: the rejected sets have the same size and contain no larger subcubes.

theorem Complexity.DepthThree.sourceReductionHardFamily_flipOn_zero (m : ℕ) (x : BitString (m + 1)) : Algebraic.Cutwidth.Extractor.sourceReductionHardFamily (m + 1) (x.flipOn {0}) = !Algebraic.Cutwidth.Extractor.sourceReductionHardFamily (m + 1) x

Flipping the first input bit negates the padded family.

theorem Complexity.DepthThree.setOf_false_eq_image (m : ℕ) : {x : BitString (m + 1) | Algebraic.Cutwidth.Extractor.sourceReductionHardFamily (m + 1) x = false} = (fun (x : BitString (m + 1)) => x.flipOn {0}) '' {x : BitString (m + 1) | Algebraic.Cutwidth.Extractor.sourceReductionHardFamily (m + 1) x = true}

theorem Complexity.DepthThree.ncard_false_eq_ncard_true (m : ℕ) : {x : BitString (m + 1) | Algebraic.Cutwidth.Extractor.sourceReductionHardFamily (m + 1) x = false}.ncard = {x : BitString (m + 1) | Algebraic.Cutwidth.Extractor.sourceReductionHardFamily (m + 1) x = true}.ncard

The rejected inputs are as many as the accepted ones.

theorem Complexity.DepthThree.containsSubcube_true_of_false {m D : ℕ} (h : ContainsSubcube {x : BitString (m + 1) | Algebraic.Cutwidth.Extractor.sourceReductionHardFamily (m + 1) x = false} D) : ContainsSubcube {x : BitString (m + 1) | Algebraic.Cutwidth.Extractor.sourceReductionHardFamily (m + 1) x = true} D

A subcube of rejected inputs flips to a subcube of accepted inputs.

theorem Complexity.DepthThree.sourceReductionHardFamily_hypotheses : ∃ (D : ℕ → ℕ), ((fun (n : ℕ) => ↑(D n)) =o[Filter.atTop] fun (n : ℕ) => ↑n) ∧ (∀ᶠ (n : ℕ) in Filter.atTop, ¬ContainsSubcube {x : BitString n | Algebraic.Cutwidth.Extractor.sourceReductionHardFamily n x = true} (D n)) ∧ (fun (n : ℕ) => ↑n * Real.log 2 - Real.log ↑{x : Fin n → Bool | Algebraic.Cutwidth.Extractor.sourceReductionHardFamily n x = true}.ncard) =o[Filter.atTop] fun (n : ℕ) => ↑n

The explicit family's subcube-dimension bound and density, from the frontier hypotheses.

theorem Complexity.DepthThree.sourceReductionHardFamily_sigmaThree {k : ℕ} (hk : 1 ≤ k) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, 2 ^ ((1 / ↑k - ε) * ↑n) ≤ ↑(sigmaThreeSize k (Algebraic.Cutwidth.Extractor.sourceReductionHardFamily n))

Σ₃^k for the explicit family.

theorem Complexity.DepthThree.sourceReductionHardFamily_piThree {k : ℕ} (hk : 1 ≤ k) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, 2 ^ ((1 / ↑k - ε) * ↑n) ≤ ↑(piThreeSize k (Algebraic.Cutwidth.Extractor.sourceReductionHardFamily n))

Π₃^k for the explicit family.