Coefficient-four hardness from balanced padding

One fixed extractor family with any fixed error strictly below one half and sublinear source entropy yields one fixed padded family that requires more than (4 - ε) times its padded input length in gates, for every positive ε and all sufficiently large inputs. The same result holds for nondeterministic circuits with unrestricted witness lengths. The extractor family remains an assumption; all graph bounds and padding steps are proved. With the graph-ordering hypothesis for a general coefficient A > 0 in place of the proved bound, the same padded family needs more than (1 + 1/A - ε) times its padded input length in gates.

theorem Algebraic.Cutwidth.eventually_lt_size_balancePad_of_flatSumsetExtractor (f : (n : ℕ) → Cslib.BooleanFunction n) (K : ℕ → ℕ) {ν : ℝ} (hν : ν < 1 / 2) (positive : ∀ᶠ (n : ℕ) in Filter.atTop, 0 < K n) (hK : (fun (n : ℕ) => Real.logb 2 ↑(K n)) =o[Filter.atTop] fun (n : ℕ) => ↑n) (extract : ∀ᶠ (n : ℕ) in Filter.atTop, FlatSumsetExtractor (f n) (K n) ν) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (circuit : Circuit Binary.signature (n + 1) 1), (circuit.Computes Binary.interpretation fun (x : Fin (n + 1) → Bool) (x_1 : Fin 1) => balancePad (f n) x) → (4 - ε) * (↑n + 1) < ↑circuit.size

Balanced padding turns extraction with any fixed error below one half and log₂ K = o(n) into a lower bound measured at the full padded length. The family and its threshold are fixed before choosing the circuit slack.

theorem Algebraic.Cutwidth.nondet_eventually_lt_size_balancePad_of_flatSumsetExtractor (f : (n : ℕ) → Cslib.BooleanFunction n) (K : ℕ → ℕ) {ν : ℝ} (hν : ν < 1 / 2) (positive : ∀ᶠ (n : ℕ) in Filter.atTop, 0 < K n) (hK : (fun (n : ℕ) => Real.logb 2 ↑(K n)) =o[Filter.atTop] fun (n : ℕ) => ↑n) (extract : ∀ᶠ (n : ℕ) in Filter.atTop, FlatSumsetExtractor (f n) (K n) ν) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (m : ℕ) (circuit : Circuit Binary.signature (n + 1 + m) 1), NondetComputes circuit (balancePad (f n)) → (4 - ε) * (↑n + 1) < ↑circuit.size

The same padded family is hard for nondeterministic circuits with any number of witness inputs; the lower bound counts its n + 1 ordinary inputs.

theorem Algebraic.Cutwidth.eventually_lt_size_balancePad_of_flatSumsetExtractor_of_orderingBound {A : ℝ} (hA : 0 < A) (order : ∀ (η : ℝ), 0 < η → ∃ (C : ℝ), Multigraph.OrderingBound A η C) (f : (n : ℕ) → Cslib.BooleanFunction n) (K : ℕ → ℕ) {ν : ℝ} (hν : ν < 1 / 2) (positive : ∀ᶠ (n : ℕ) in Filter.atTop, 0 < K n) (hK : (fun (n : ℕ) => Real.logb 2 ↑(K n)) =o[Filter.atTop] fun (n : ℕ) => ↑n) (extract : ∀ᶠ (n : ℕ) in Filter.atTop, FlatSumsetExtractor (f n) (K n) ν) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (circuit : Circuit Binary.signature (n + 1) 1), (circuit.Computes Binary.interpretation fun (x : Fin (n + 1) → Bool) (x_1 : Fin 1) => balancePad (f n) x) → (1 + 1 / A - ε) * (↑n + 1) < ↑circuit.size

Balanced padding with a general graph-ordering coefficient: if the ordering hypothesis holds with coefficient A > 0 for every positive slack, the same padded family needs more than (1 + 1/A - ε) (n + 1) gates.

theorem Algebraic.Cutwidth.nondet_eventually_lt_size_balancePad_of_flatSumsetExtractor_of_orderingBound {A : ℝ} (hA : 0 < A) (order : ∀ (η : ℝ), 0 < η → ∃ (C : ℝ), Multigraph.OrderingBound A η C) (f : (n : ℕ) → Cslib.BooleanFunction n) (K : ℕ → ℕ) {ν : ℝ} (hν : ν < 1 / 2) (positive : ∀ᶠ (n : ℕ) in Filter.atTop, 0 < K n) (hK : (fun (n : ℕ) => Real.logb 2 ↑(K n)) =o[Filter.atTop] fun (n : ℕ) => ↑n) (extract : ∀ᶠ (n : ℕ) in Filter.atTop, FlatSumsetExtractor (f n) (K n) ν) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (m : ℕ) (circuit : Circuit Binary.signature (n + 1 + m) 1), NondetComputes circuit (balancePad (f n)) → (1 + 1 / A - ε) * (↑n + 1) < ↑circuit.size

The nondeterministic padded bound with a general graph-ordering coefficient A > 0, for any number of witness inputs.