Rectangle parameters for the fixed polynomial-time family

These facts concern the existing sourceReductionHardFamily, at its full input length. The threshold doubles the extractor threshold to account for its balanced padding. They are independent of the circuit basis, so mixed aggregate circuits use exactly the same family and polynomial-time evaluator as the ordinary binary lower bound.

def Algebraic.Cutwidth.Aggregate.familyThreshold (n : ℕ) : ℕ

The rectangle threshold for the fixed, balanced hard family at the full input length.

Equations

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

theorem Algebraic.Cutwidth.Aggregate.familyThreshold_one_lt (n : ℕ) : 1 < familyThreshold n

theorem Algebraic.Cutwidth.Aggregate.familyThreshold_log_isLittleO : (fun (n : ℕ) => Real.logb 2 ↑(familyThreshold n)) =o[Filter.atTop] fun (n : ℕ) => ↑n

The rectangle threshold has sublinear binary logarithm.

theorem Algebraic.Cutwidth.Aggregate.family_eventually_hard : ∀ᶠ (n : ℕ) in Filter.atTop, RectangleFree (Extractor.sourceReductionHardFamily n) (familyThreshold n) ∧ 2 ^ (n - 2) ≤ (accepting (Extractor.sourceReductionHardFamily n)).card

The fixed family is eventually dense and rectangle-free at the stated threshold.