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

stable_iff_boundary

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)

  21theorem stable_iff_boundary (s : PreState) :
  22    IsStable s ↔ s.val = 0 ∨ s.val = 1 := by

proof body

Term-mode proof.

  23  unfold IsStable preCost
  24  constructor
  25  · intro h
  26    have hfact : s.val * (1 - s.val) = 0 := h
  27    rcases mul_eq_zero.mp hfact with h0 | h1
  28    · exact Or.inl h0
  29    · right
  30      linarith
  31  · intro h
  32    rcases h with h0 | h1
  33    · simp [h0]
  34    · simp [h1]
  35
  36/-- Stable states as arithmetic 0/1 encodings. -/

depends on (7)

Lean names referenced from this declaration's body.