The explicit lower bound from modular contribution rank

The fixed hard family retains its Gaussian coefficient when the modular contribution matrix has sublinear information content. The modulus may vary with the input length and the circuit. The factorization is constructed from the matrix itself, so no separate compression certificate is assumed.

theorem Algebraic.Cutwidth.Aggregate.Compressed.sourceReductionHardFamily_eventually_lt_size_modular_stateBudget (D : ℕ → ℕ) (hD : (fun (n : ℕ) => ↑(D n)) =o[Filter.atTop] fun (n : ℕ) => ↑n) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (p : ℕ) [inst : Fact (Nat.Prime p)] (c : Circuit (Aggregate.signature (Aggregate.Compressed.Modular.State p)) n 1), (c.Computes Aggregate.interpretation fun (x : Fin n → Bool) (x_1 : Fin 1) => Extractor.sourceReductionHardFamily n x) → 2 * Nat.clog 2 (p ^ Aggregate.Compressed.Modular.contributionRank c.program) ≤ D n → (1 + Real.pi / (3 * Real.arccos ((1 + 2 * √2) / 4)) - ε) * ↑n < ↑c.size

The full Gaussian coefficient follows from the exact modular state budget, uniformly over prime moduli and circuits, with no additional factorization hypothesis.

theorem Algebraic.Cutwidth.Aggregate.Compressed.sourceReductionHardFamily_eventually_lt_size_modular_rankBudget (D : ℕ → ℕ) (hD : (fun (n : ℕ) => ↑(D n)) =o[Filter.atTop] fun (n : ℕ) => ↑n) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (p : ℕ) [inst : Fact (Nat.Prime p)] (c : Circuit (Aggregate.signature (Aggregate.Compressed.Modular.State p)) n 1), (c.Computes Aggregate.interpretation fun (x : Fin n → Bool) (x_1 : Fin 1) => Extractor.sourceReductionHardFamily n x) → 2 * Aggregate.Compressed.Modular.contributionRank c.program * Nat.clog 2 p ≤ D n → (1 + Real.pi / (3 * Real.arccos ((1 + 2 * √2) / 4)) - ε) * ↑n < ↑c.size

A sublinear rank-times-residue budget preserves the coefficient for varying prime moduli.

theorem Algebraic.Cutwidth.Aggregate.Compressed.sourceReductionHardFamily_eventually_lt_size_modular_fixedPrime (p : ℕ) [Fact (Nat.Prime p)] (R : ℕ → ℕ) (hR : (fun (n : ℕ) => ↑(R n)) =o[Filter.atTop] fun (n : ℕ) => ↑n) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (c : Circuit (Aggregate.signature (Aggregate.Compressed.Modular.State p)) n 1), (c.Computes Aggregate.interpretation fun (x : Fin n → Bool) (x_1 : Fin 1) => Extractor.sourceReductionHardFamily n x) → Aggregate.Compressed.Modular.contributionRank c.program ≤ R n → (1 + Real.pi / (3 * Real.arccos ((1 + 2 * √2) / 4)) - ε) * ↑n < ↑c.size

At any fixed prime modulus, a sublinear rank bound alone suffices.