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

info_cost_zero_iff_unit

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)

  62theorem info_cost_zero_iff_unit (e : RecognitionEvent) :
  63    infoCost e = 0 ↔ e.ratio = 1 := by

proof body

Tactic-mode proof.

  64  unfold infoCost
  65  constructor
  66  · intro h
  67    rw [Jcost_eq_sq e.ratio_pos.ne'] at h
  68    have hden_pos : 0 < 2 * e.ratio := by linarith [e.ratio_pos]
  69    have hden_ne : (2 * e.ratio) ≠ 0 := ne_of_gt hden_pos
  70    have hsq : (e.ratio - 1) ^ 2 = 0 := by
  71      rwa [div_eq_zero_iff, or_iff_left hden_ne] at h
  72    nlinarith [sq_nonneg (e.ratio - 1)]
  73  · intro h; rw [h]; exact Jcost_unit0
  74
  75/-- **THEOREM IC-001.3**: Any ratio x ≠ 1 carries strictly positive information cost.
  76    J(x) > 0 for all x > 0, x ≠ 1. -/

used by (3)

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.