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

feasible_implies_boolean

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)

  53theorem feasible_implies_boolean {n N : ℕ} {φ : CNF n}
  54    (M : BWD3Model (n := n) (N := N) φ) :

proof body

Term-mode proof.

  55    ∀ u, M.admissible u → M.L.mulVec u = M.b → BooleanPhaseState u :=
  56  M.schur_pinch
  57
  58/--
  59Optional algorithmic interface: a rank/null-space test can be plugged in as a
  60single Boolean oracle. This is intentionally abstract at scaffold stage.
  61-/

depends on (16)

Lean names referenced from this declaration's body.