`the_proof_sketch`

definition

show as: view math explainer →

module: IndisputableMonolith.Complexity.CircuitLowerBound
domain: Complexity
line: 232 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Complexity.CircuitLowerBound on GitHub at line 232.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

AlgebraicRestrictionProofSketch IndisputableMonolith.Complexity.CircuitLowerBound

formal source

 229  layer_propagation : True
 230  accumulation : True
 231
 232def the_proof_sketch : AlgebraicRestrictionProofSketch where
 233  non_separability := trivial
 234  layer_propagation := trivial
 235  accumulation := trivial
 236
 237/-! ## Certificate -/
 238
 239structure CircuitLowerBoundCert where
 240  /-- Algebraic restriction gives linear lower bound -/
 241  algebraic_linear : AlgebraicRestrictionHyp →
 242    ∀ (n : ℕ) (f : CNFFormula n), f.isUNSAT →
 243    ∀ (c : BooleanCircuit n), CircuitDecides c f →
 244    (c.gate_count : ℝ) ≥ n
 245  /-- Topological obstruction gives exponential lower bound -/
 246  topological_exp : TopologicalObstructionHyp →
 247    ∀ (n : ℕ) (f : CNFFormula n), f.isUNSAT →
 248    ∀ (c : BooleanCircuit n), CircuitDecides c f →
 249    ∃ (k : ℕ), 0 < k ∧ (c.gate_count : ℝ) ≥ 2 ^ (n / k)
 250
 251def circuitLowerBoundCert : CircuitLowerBoundCert where
 252  algebraic_linear := fun hyp n f hunsat c hdec =>
 253    circuit_lower_bound_algebraic hyp f hunsat c hdec
 254  topological_exp := fun hyp n f hunsat c hdec =>
 255    circuit_lower_bound_topological hyp f hunsat c hdec
 256
 257end -- noncomputable section
 258
 259end CircuitLowerBound
 260end Complexity
 261end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.