structure
definition
def or abbrev
TopologicalObstructionHyp
show as:
view Lean formalization →
formal statement (Lean)
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). -/