The coefficient-four bound for the computed hard family

The actual uniform source-reduction family has fixed extraction error below one half and sublinear entropy. Its dyadic threshold has binary logarithm equal to that entropy. Balanced padding therefore gives the circuit bound 1 + 1/A for every graph-ordering coefficient A > 0, and shifting the eventual statement measures it at every sufficiently large full input length. The proved ordering bound with A = 1/3 gives the coefficient four, and the Gaussian edge-score bound with A = (3/π) arccos ((1 + 2√2)/4) gives 1 + π/(3 arccos((1 + 2√2)/4)); its rational weakening A = 9/32 gives 41/9. Conditionally on subcritical band clusters (Gaussian.BandSubcritical), the band-jump bound with A = 2 exp (-c²/2) p gives 1 + 1/A, and its rational weakening A = 5/18 at c = 4/25 gives 23/5.

theorem Algebraic.Cutwidth.Extractor.Internal.sourceReductionHardFamily_eventually_lt_size_of_orderingBound {A : ℝ} (hA : 0 < A) (order : ∀ (η : ℝ), 0 < η → ∃ (C : ℝ), Multigraph.OrderingBound A η C) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (circuit : Circuit Binary.signature n 1), (circuit.Computes Binary.interpretation fun (x : Fin n → Bool) (x_1 : Fin 1) => sourceReductionHardFamily n x) → (1 + 1 / A - ε) * ↑n < ↑circuit.size

theorem Algebraic.Cutwidth.Extractor.Internal.sourceReductionHardFamily_eventually_lt_size {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (circuit : Circuit Binary.signature n 1), (circuit.Computes Binary.interpretation fun (x : Fin n → Bool) (x_1 : Fin 1) => sourceReductionHardFamily n x) → (4 - ε) * ↑n < ↑circuit.size

theorem Algebraic.Cutwidth.Extractor.Internal.sourceReductionHardFamily_eventually_lt_size_gaussian {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (circuit : Circuit Binary.signature n 1), (circuit.Computes Binary.interpretation fun (x : Fin n → Bool) (x_1 : Fin 1) => sourceReductionHardFamily n x) → (1 + Real.pi / (3 * Real.arccos ((1 + 2 * √2) / 4)) - ε) * ↑n < ↑circuit.size

theorem Algebraic.Cutwidth.Extractor.Internal.sourceReductionHardFamily_eventually_lt_size_fortyOne_div_nine {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (circuit : Circuit Binary.signature n 1), (circuit.Computes Binary.interpretation fun (x : Fin n → Bool) (x_1 : Fin 1) => sourceReductionHardFamily n x) → (41 / 9 - ε) * ↑n < ↑circuit.size

theorem Algebraic.Cutwidth.Extractor.Internal.sourceReductionHardFamily_eventually_lt_size_of_bandSubcritical {c : ℝ} (hc : 0 < c) (hband : ∀ (q : ℝ) (R : ℕ), 0 ≤ q → 2 * q ^ 2 < 1 → Gaussian.BandSubcritical q R c) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (circuit : Circuit Binary.signature n 1), (circuit.Computes Binary.interpretation fun (x : Fin n → Bool) (x_1 : Fin 1) => sourceReductionHardFamily n x) → (1 + 1 / (2 * (Real.exp (-c ^ 2 / 2) * Gaussian.frontierCoefficient)) - ε) * ↑n < ↑circuit.size

theorem Algebraic.Cutwidth.Extractor.Internal.sourceReductionHardFamily_eventually_lt_size_twentyThree_div_five_of_band (hband : ∀ (q : ℝ) (R : ℕ), 0 ≤ q → 2 * q ^ 2 < 1 → Gaussian.BandSubcritical q R (4 / 25)) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (circuit : Circuit Binary.signature n 1), (circuit.Computes Binary.interpretation fun (x : Fin n → Bool) (x_1 : Fin 1) => sourceReductionHardFamily n x) → (23 / 5 - ε) * ↑n < ↑circuit.size