UniformTopologicalObstructionHyp

formal source

 120/-- **STRENGTHENED HYPOTHESIS**: Uniform exponential lower bound.
 121    The constant k is fixed (not formula-dependent), giving a uniform
 122    exponential lower bound that enables the polynomial comparison. -/
 123structure UniformTopologicalObstructionHyp where
 124  /-- Universal exponent denominator -/
 125  k : ℕ
 126  k_pos : 0 < k
 127  /-- For ALL UNSAT formulas on n variables, any deciding circuit has size ≥ 2^{n/k} -/
 128  uniform_bound : ∀ (n : ℕ) (f : CNFFormula n),
 129    f.isUNSAT →
 130    ∀ (c : BooleanCircuit n),
 131      CircuitDecides c f →
 132      (c.gate_count : ℝ) ≥ 2 ^ (n / k)
 133
 134/-- **Exponential eventually dominates any polynomial.**
 135    For any C, d, there exists m₀ such that C * m^d < 2^m for all m ≥ m₀.
 136    Proof uses Mathlib's `tendsto_pow_const_div_const_pow_of_one_lt`. -/
 137private theorem exp_dominates_poly (C d : ℕ) :
 138    ∃ m₀ : ℕ, ∀ m : ℕ, m₀ ≤ m → C * m ^ d < 2 ^ m := by
 139  suffices h : ∃ m₀ : ℕ, ∀ m, m₀ ≤ m → (C : ℝ) * (m : ℝ) ^ d < (2 : ℝ) ^ m by
 140    obtain ⟨m₀, hm₀⟩ := h; exact ⟨m₀, fun m hm => by exact_mod_cast hm₀ m hm⟩
 141  have htend := tendsto_pow_const_div_const_pow_of_one_lt d
 142    (show (1 : ℝ) < 2 by norm_num)
 143  have hev : ∀ᶠ n : ℕ in Filter.atTop,
 144      (n : ℝ) ^ d / (2 : ℝ) ^ n < 1 / ((C : ℝ) + 1) :=
 145    htend.eventually (Iio_mem_nhds (by positivity : (0 : ℝ) < 1 / ((↑C : ℝ) + 1)))
 146  rw [Filter.eventually_atTop] at hev
 147  obtain ⟨m₀, hm₀⟩ := hev
 148  exact ⟨m₀, fun m hm => by
 149    have hlt := hm₀ m hm
 150    have h2 : (0 : ℝ) < (2 : ℝ) ^ m := by positivity
 151    have hC1 : (0 : ℝ) < (C : ℝ) + 1 := by positivity
 152    have hmd : (0 : ℝ) ≤ (m : ℝ) ^ d := by positivity
 153    rw [div_lt_iff₀ h2] at hlt