p_neq_np_assembled

formal source

  50/-- **CONDITIONAL THEOREM (P ≠ NP).**
  51    Given the uniform topological obstruction, for every polynomial bound
  52    there exists n₀ beyond which no polynomial circuit decides satisfiability. -/
  53theorem p_neq_np_assembled (pkg : PneqNPConditional) :
  54    ∀ (poly_k poly_c : ℕ), ∃ (n₀ : ℕ),
  55      ∀ n : ℕ, n₀ ≤ n →
  56        ∀ (f : CNFFormula n), f.isUNSAT →
  57          ∀ (c : BooleanCircuit n), CircuitDecides c f →
  58            ¬ (c.gate_count ≤ poly_c * n ^ poly_k) :=
  59  p_neq_np_conditional pkg.phase3_hypothesis
  60
  61/-! ## Path B: Dissolution (Unconditional RS Position) -/
  62
  63/-- The RS dissolution argument. -/
  64structure PvsNPDissolution where
  65  rhat_polytime : ∀ n : ℕ, ∀ f : CNFFormula n, f.isSAT →
  66    ∃ (steps : ℕ) (a : Assignment n), steps ≤ n ∧ satJCost f a = 0
  67  unsat_obstruction : ∀ n : ℕ, ∀ f : CNFFormula n, f.isUNSAT →
  68    ∀ a : Assignment n, satJCost f a ≥ 1
  69  local_blindness : ∀ n : ℕ, ∀ M : Finset (Fin n), M.card < n →
  70    ∀ decoder : ({i // i ∈ M} → Bool) → Bool,
  71      ∃ (b : Bool) (R : Fin n → Bool),
  72        decoder (BalancedParityHidden.restrict
  73          (BalancedParityHidden.enc b R) M) ≠ b
  74
  75theorem dissolution_holds : PvsNPDissolution where
  76  rhat_polytime := fun n f h =>
  77    let ⟨steps, a, hle, ha⟩ := sat_recognition_time_bound f h
  78    ⟨steps, a, hle, ha⟩
  79  unsat_obstruction := fun _n f h => unsat_cost_lower_bound f h
  80  local_blindness := fun _n M _hM decoder =>
  81    BalancedParityHidden.adversarial_failure M decoder
  82
  83/-! ## Status -/