PvsNPDissolution

formal source

  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 -/
  84
  85structure PvsNPResolutionStatus where
  86  conditional_proof_available : Bool
  87  dissolution_proved : Bool
  88  open_gap : String
  89  sorry_count_in_chain : ℕ
  90
  91def currentStatus : PvsNPResolutionStatus where
  92  conditional_proof_available := false
  93  dissolution_proved := true
  94  open_gap := "UniformTopologicalObstructionHyp: prove that for some fixed k, " ++