UniformTopologicalObstructionHyp
UniformTopologicalObstructionHyp packages a fixed positive integer k with the quantified claim that every unsatisfiable CNF formula on n variables forces any deciding Boolean circuit to have gate count at least 2 to the power n over k. Complexity researchers assembling conditional P versus NP arguments cite this structure to supply the uniform exponential lower bound. The declaration is a direct structure definition that bundles the parameter and the forall statement without computational steps.
claimA structure consisting of a positive integer $k$ such that for every natural number $n$ and every unsatisfiable CNF formula $f$ on $n$ variables, every Boolean circuit $c$ deciding $f$ satisfies gate count of $c$ at least $2^{n/k}$.
background
The module formalizes circuit lower bounds from J-frustration using the Recognition Composition Law to endow the J-cost landscape with multiplicative structure that polynomial circuits cannot exploit. BooleanCircuit is defined as a feed-forward structure with gate_count and gates in topological order, while CircuitDecides asserts an existential evaluation function matching the formula's satisfiability map. CNFFormula is a list of clauses over n variables with a var_count field.
proof idea
This is a structure definition that directly packages the positive integer k together with the uniform bound statement over all n and all unsatisfiable formulas.
why it matters in Recognition Science
The structure supplies the UniformTopologicalObstructionHyp required by PneqNPConditional in PvsNPAssembly and is the hypothesis parameter to the theorem p_neq_np_conditional. That theorem shows the bound implies no polynomial-size circuit decides unsatisfiability for large n. It fills the open gap listed in currentStatus for the circuit lower bound program and enables the conditional separation once the exponential domination step is applied.
scope and limits
- Does not prove existence of any such k.
- Does not fix a concrete numerical value for k.
- Does not apply to satisfiable formulas.
- Does not encode depth-width tradeoffs or spectral gap details.
formal statement (Lean)
123structure UniformTopologicalObstructionHyp where
124 /-- Universal exponent denominator -/
125 k : ℕ
126 k_pos : 0 < k
127 /-- For ALL UNSAT formulas on n variables, any deciding circuit has size ≥ 2^{n/k} -/
128 uniform_bound : ∀ (n : ℕ) (f : CNFFormula n),
129 f.isUNSAT →
130 ∀ (c : BooleanCircuit n),
131 CircuitDecides c f →
132 (c.gate_count : ℝ) ≥ 2 ^ (n / k)
133
134/-- **Exponential eventually dominates any polynomial.**
135 For any C, d, there exists m₀ such that C * m^d < 2^m for all m ≥ m₀.
136 Proof uses Mathlib's `tendsto_pow_const_div_const_pow_of_one_lt`. -/