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

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

  25theorem self_recognition_zero_cost (e : LedgerForcing.RecognitionEvent) :
  26    e.ratio = 1 → recognition_cost e = 0 := by

proof body

Term-mode proof.

  27  intro h
  28  simp only [recognition_cost, h, LedgerForcing.J]
  29  norm_num
  30
  31/-- Non-trivial recognition has positive cost.
  32    Uses the fact that J(x) = (x + 1/x)/2 - 1 ≥ 0, with = 0 iff x = 1. -/

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.