Transporting balanced padding through the asymptotic lower bound

Doubling a source threshold and shifting its index preserve a sublinear binary logarithm. At each positive length, the padded extractor gives a rectangle-free function accepting exactly half the inputs. The graph-free circuit theorems therefore apply to one fixed padded family, as do the theorems with a general graph-ordering coefficient.

theorem Algebraic.Cutwidth.Extractor.Internal.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

theorem Algebraic.Cutwidth.Extractor.Internal.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

theorem Algebraic.Cutwidth.Extractor.Internal.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

theorem Algebraic.Cutwidth.Extractor.Internal.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