AlgebraicRestrictionProofSketch

formal source

 224       the total propagation is 2^d. Reaching all n variables requires
 225       depth ≥ log₂(n), and each layer must have width ≥ n/2^d.
 226       Total size ≥ Σ_{d=0}^{log n} n/2^d = Θ(n). -/
 227structure AlgebraicRestrictionProofSketch where
 228  non_separability : True
 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