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

constant_implies_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)

  79theorem constant_implies_zero_cost {x : V → ℝ} {v w : V}
  80    (h : x v = x w) (hw : 0 < x w) :
  81    Jcost (x v / x w) = 0 := by

proof body

Term-mode proof.

  82  rw [h, div_self (ne_of_gt hw)]
  83  exact Jcost_unit0
  84
  85/-- **RESULT 1 — Full characterization (iff).**
  86
  87On a connected graph with a positive field x : V → ℝ_{>0}:
  88
  89  (∀ edges, J(x_v/x_w) = 0)  ↔  x is constant.
  90
  91This is the machine-verified version of Result 1. -/

used by (1)

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

depends on (15)

Lean names referenced from this declaration's body.