TopologicalObstructionHyp

formal source

  79    the boundary has exponential description complexity (it touches Ω(2^n)
  80    vertices of the Boolean hypercube), any circuit representing it must
  81    have super-polynomial size. -/
  82structure TopologicalObstructionHyp where
  83  /-- For UNSAT formulas, any deciding circuit has size ≥ 2^{n/k} for some k -/
  84  exponential_lower_bound : ∀ (n : ℕ) (f : CNFFormula n),
  85    f.isUNSAT →
  86    ∀ (c : BooleanCircuit n),
  87      CircuitDecides c f →
  88      ∃ (k : ℕ), 0 < k ∧ (c.gate_count : ℝ) ≥ 2 ^ (n / k)
  89
  90/-! ## The Circuit Lower Bound Theorem -/
  91
  92/-- **CONDITIONAL THEOREM (Circuit Lower Bound from Algebraic Restriction).**
  93
  94    Given the AlgebraicRestrictionHyp, any circuit deciding an UNSAT formula
  95    on n variables has size ≥ n (since landscape depth ≥ 1 for UNSAT). -/
  96theorem circuit_lower_bound_algebraic
  97    (hyp : AlgebraicRestrictionHyp) {n : ℕ} (f : CNFFormula n)
  98    (hunsat : f.isUNSAT) (c : BooleanCircuit n) (hdec : CircuitDecides c f) :
  99    (c.gate_count : ℝ) ≥ n := by
 100  have hd := hyp.depth_size_tradeoff n f hunsat c hdec
 101  have hld := landscapeDepth_unsat f hunsat
 102  have hn : (0 : ℝ) ≤ (n : ℝ) := Nat.cast_nonneg _
 103  calc (c.gate_count : ℝ) ≥ LandscapeDepth f * n := hd
 104    _ ≥ 1 * n := by
 105        apply mul_le_mul_of_nonneg_right hld hn
 106    _ = n := one_mul _
 107
 108/-- **CONDITIONAL THEOREM (Circuit Lower Bound from Topological Obstruction).**
 109
 110    Given the TopologicalObstructionHyp, any circuit deciding an UNSAT formula
 111    has exponential size. -/
 112theorem circuit_lower_bound_topological