p_neq_np_conditional
The conditional theorem shows that a uniform topological obstruction with fixed k forces every deciding circuit for unsatisfiable CNF formulas on n variables to have gate count at least 2^{n/k}, which overtakes any fixed polynomial for large n. Complexity theorists assembling conditional P versus NP results would cite this when the obstruction hypothesis is available. The proof extracts k from the hypothesis, invokes exp_dominates_poly to locate a crossover threshold, and reduces the polynomial comparison to the exponential lower bound through
claimAssume the uniform topological obstruction hypothesis holds with fixed positive integer $k$. Then for all natural numbers $p_k, p_c$ there exists $n_0$ such that for all $n >= n_0$, every unsatisfiable CNF formula $f$ on $n$ variables, and every Boolean circuit $c$ that decides $f$, the gate count of $c$ satisfies gate_count$(c) > p_c n^{p_k}$.
background
The CircuitLowerBound module derives super-polynomial circuit size from high J-frustration on SAT instances. UniformTopologicalObstructionHyp is the structure fixing a constant $k > 0$ and asserting that every circuit deciding an unsatisfiable formula on $n$ variables has gate_count at least $2^{n/k}$. BooleanCircuit is the feed-forward model with gate_count and a topological list of gates; CircuitDecides requires an evaluation function matching the formula's satisfiability predicate.
proof idea
The tactic proof introduces the polynomial parameters, sets $k$ from the hypothesis and records its positivity, then obtains a threshold $m_0$ from the exp_dominates_poly lemma applied to the scaled polynomial. It refines the existential to $k$ times max($m_0$,1) and, for $n$ large, sets $m = n/k$, verifies $m >= m_0$ and $m >= 1$ via Nat division lemmas, establishes the polynomial bound is dominated by a multiple of $m^{p_k}$, applies the domination lemma to reach a strict inequality against $2^m$, invokes the uniform_bound from the hypothesis, and closes with real-number linarith.
why it matters in Recognition Science
This supplies the conditional separation that is assembled into the parent theorem p_neq_np_assembled in PvsNPAssembly. It completes the SAT instantiation step of the module's three-part argument linking J-frustration (from the Recognition Composition Law) to exponential circuit lower bounds. The result sits at the research frontier noted in the module doc, where algebraic restriction and topological obstruction hypotheses remain open; discharging them would complete the P ≠ NP claim inside the Recognition framework.
scope and limits
- Does not discharge UniformTopologicalObstructionHyp or prove the exponential lower bound itself.
- Does not address the algebraic restriction hypothesis on J-cost non-separability.
- Does not apply to circuits allowing global coupling or non-feed-forward topologies.
- Does not quantify precise constants inside the exponential bound or handle average-case formulas.
formal statement (Lean)
166theorem p_neq_np_conditional (hyp : UniformTopologicalObstructionHyp) :
167 ∀ (poly_k poly_c : ℕ), ∃ (n₀ : ℕ),
168 ∀ n : ℕ, n₀ ≤ n →
169 ∀ (f : CNFFormula n), f.isUNSAT →
170 ∀ (c : BooleanCircuit n), CircuitDecides c f →
171 ¬ (c.gate_count ≤ poly_c * n ^ poly_k) := by
proof body
Tactic-mode proof.
172 intro poly_k poly_c
173 set k := hyp.k
174 have hk_pos := hyp.k_pos
175 obtain ⟨m₀, hm₀⟩ := exp_dominates_poly (poly_c * (2 * k) ^ poly_k) poly_k
176 refine ⟨k * max m₀ 1, fun n hn f hunsat c hdec hle => ?_⟩
177 set m := n / k
178 have hm_ge_m₀ : m₀ ≤ m := by
179 apply (Nat.le_div_iff_mul_le hk_pos).mpr
180 calc m₀ * k ≤ max m₀ 1 * k := Nat.mul_le_mul_right k (le_max_left m₀ 1)
181 _ = k * max m₀ 1 := Nat.mul_comm _ _
182 _ ≤ n := hn
183 have hm_ge_1 : 1 ≤ m := by
184 apply (Nat.le_div_iff_mul_le hk_pos).mpr
185 calc 1 * k = k := Nat.one_mul k
186 _ = k * 1 := (Nat.mul_one k).symm
187 _ ≤ k * max m₀ 1 := Nat.mul_le_mul_left k (le_max_right m₀ 1)
188 _ ≤ n := hn
189 have hn_le : n ≤ 2 * k * m := by
190 have h1 : n = k * m + n % k := (Nat.div_add_mod n k).symm
191 have h2 : n % k < k := Nat.mod_lt n hk_pos
192 have h3 : k ≤ k * m := Nat.le_mul_of_pos_right k (by linarith : 0 < m)
193 have h4 : 2 * k * m = k * m + k * m := by ring
194 linarith
195 have h_npk : poly_c * n ^ poly_k ≤ poly_c * (2 * k) ^ poly_k * m ^ poly_k := by
196 calc poly_c * n ^ poly_k
197 ≤ poly_c * (2 * k * m) ^ poly_k :=
198 Nat.mul_le_mul_left _ (Nat.pow_le_pow_left hn_le _)
199 _ = poly_c * ((2 * k) ^ poly_k * m ^ poly_k) := by rw [Nat.mul_pow]
200 _ = poly_c * (2 * k) ^ poly_k * m ^ poly_k := by ring
201 have hdom := lt_of_le_of_lt h_npk (hm₀ m hm_ge_m₀)
202 have hexp := hyp.uniform_bound n f hunsat c hdec
203 have hpoly : (c.gate_count : ℝ) ≤ ↑(poly_c * n ^ poly_k) := by exact_mod_cast hle
204 have hdom_real : (↑(poly_c * n ^ poly_k) : ℝ) < (2 : ℝ) ^ m := by exact_mod_cast hdom
205 linarith
206
207/-! ## What Remains Open -/
208
209/-- **OPEN: Discharge AlgebraicRestrictionHyp.**
210
211 The d'Alembert multiplicative structure must be shown to force Ω(n)
212 simultaneous bit access. The proposed approach:
213
214 1. Show that evaluating J(x·y) from J(x) and J(y) requires knowing
215 both x and y (not just one of them) — this is the "non-separability"
216 of the multiplicative combiner.
217
218 2. In circuit terms: any gate computing J-cost on a subset of variables
219 cannot propagate the multiplicative structure without reading all
220 variables in that subset.
221
222 3. Accumulate: each layer of the circuit can propagate multiplicative
223 structure through at most 2^depth variables. For depth d,
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). -/