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

rs_exists_iff_zero_cost

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)

 115theorem rs_exists_iff_zero_cost (x : ℝ) (hx : x > 0) :
 116    Cost.Jcost x = 0 ↔ x = 1 := by

proof body

Tactic-mode proof.

 117  constructor
 118  · intro h
 119    rw [Cost.Jcost_eq_sq hx.ne'] at h
 120    have hden : (2 * x) > 0 := by linarith
 121    have hne : (2 * x) ≠ 0 := ne_of_gt hden
 122    have hsq : (x - 1)^2 = 0 := by
 123      rwa [div_eq_zero_iff, or_iff_left hne] at h
 124    nlinarith [sq_nonneg (x - 1)]
 125  · intro h; rw [h]; exact Cost.Jcost_unit0
 126
 127/-! ## IV. Church-Turing Chain -/
 128

used by (1)

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

depends on (8)

Lean names referenced from this declaration's body.