RSATSeparation

formal source

 244
 245    This is NOT a proof of P ≠ NP for Turing machines. It establishes that
 246    the R̂ model of computation separates the classes in a different way. -/
 247structure RSATSeparation where
 248  /-- SAT is solvable in O(n) recognition steps for satisfiable instances -/
 249  sat_polytime : ∀ n : ℕ, ∀ f : CNFFormula n, f.isSAT →
 250    ∃ steps : ℕ, steps ≤ n ∧ ∃ a : Assignment n, satJCost f a = 0
 251  /-- No local certifier works for all formulas (adversarial failure) -/
 252  local_certifier_fails : ∀ n : ℕ, ∀ M : Finset (Fin n),
 253    M.card < n →
 254    ∃ b : Bool, ∃ R : Fin n → Bool,
 255      ∃ g : ({i // i ∈ M} → Bool) → Bool,
 256        g (BalancedParityHidden.restrict (BalancedParityHidden.enc b R) M) ≠ b
 257  /-- UNSAT instances have a persistent topological obstruction -/
 258  unsat_obstruction : ∀ n : ℕ, ∀ f : CNFFormula n, f.isUNSAT →
 259    ∀ a : Assignment n, satJCost f a ≥ 1
 260
 261theorem rsatSeparation : RSATSeparation where
 262  sat_polytime := fun n f h =>
 263    let ⟨steps, a, hle, ha⟩ := sat_recognition_time_bound f h
 264    ⟨steps, hle, a, ha⟩
 265  local_certifier_fails := fun n M hcard =>
 266    let ⟨b, R, g_eq⟩ := BalancedParityHidden.adversarial_failure M (fun _ => true)
 267    ⟨b, R, fun _ => true, g_eq⟩
 268  unsat_obstruction := fun n f h => unsat_cost_lower_bound f h
 269
 270end RSatEncoding
 271end Complexity
 272end IndisputableMonolith