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

rsatSeparation

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)

 261theorem rsatSeparation : RSATSeparation where
 262  sat_polytime := fun n f h =>

proof body

Term-mode proof.

 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

depends on (5)

Lean names referenced from this declaration's body.