pith. machine review for the scientific record. sign in
theorem proved term proof

dissolution_holds

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  75theorem dissolution_holds : PvsNPDissolution where
  76  rhat_polytime := fun n f h =>

proof body

Term-mode proof.

  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

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (6)

Lean names referenced from this declaration's body.