structure
definition
AlgebraicRestrictionHyp
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Complexity.CircuitLowerBound on GitHub at line 62.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
-
of -
BooleanCircuit -
CircuitDecides -
LandscapeDepth -
CNFFormula -
has -
of -
defect -
cost -
cost -
of -
of -
for -
of -
and -
that
used by
formal source
59
60 This is the analog of the Karchmer-Wigderson depth lower bound,
61 specialized to the J-cost structure. -/
62structure AlgebraicRestrictionHyp where
63 /-- For any n-variable Boolean function with high landscape depth,
64 any circuit computing it has depth · size ≥ landscape depth · n -/
65 depth_size_tradeoff : ∀ (n : ℕ) (f : CNFFormula n),
66 f.isUNSAT →
67 ∀ (c : BooleanCircuit n),
68 CircuitDecides c f →
69 (c.gate_count : ℝ) ≥ LandscapeDepth f * n
70
71/-- **HYPOTHESIS (Topological Obstruction).**
72
73 The J-cost landscape for UNSAT formulas has a non-trivial topological
74 invariant: the defect moat (J-cost ≥ 1 everywhere) creates a "barrier"
75 that any circuit computing the satisfiability function must encode.
76
77 Encoding this barrier requires the circuit to represent the boundary
78 between the ≥1 region and the (hypothetical) zero-cost region. Since
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).**