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

recognition_is_cost_structure

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)

  59theorem recognition_is_cost_structure :
  60    ∀ (e : LedgerForcing.RecognitionEvent),
  61    (e.ratio = 1 ↔ recognition_cost e = 0) ∧
  62    (e.ratio ≠ 1 → recognition_cost e > 0) := by

proof body

Tactic-mode proof.

  63  intro e
  64  refine ⟨⟨self_recognition_zero_cost e, ?_⟩, nontrivial_recognition_positive_cost e⟩
  65  intro h
  66  simp only [recognition_cost, LedgerForcing.J] at h
  67  have hpos := e.ratio_pos
  68  have h0 : e.ratio ≠ 0 := hpos.ne'
  69  -- h says (e.ratio + e.ratio⁻¹)/2 - 1 = 0
  70  -- So e.ratio + e.ratio⁻¹ = 2
  71  have h1 : e.ratio + e.ratio⁻¹ = 2 := by linarith
  72  -- This means (e.ratio - 1)² = 0
  73  have heq : e.ratio + e.ratio⁻¹ = (e.ratio^2 + 1) / e.ratio := by field_simp
  74  have h2 : (e.ratio^2 + 1) / e.ratio = 2 := by rw [← heq]; exact h1
  75  have h3 : e.ratio^2 + 1 = 2 * e.ratio := by
  76    have := congrArg (· * e.ratio) h2
  77    simp only [div_mul_cancel₀ _ h0] at this
  78    linarith
  79  have h4 : (e.ratio - 1)^2 = 0 := by nlinarith [sq_nonneg (e.ratio - 1)]
  80  exact sub_eq_zero.mp (sq_eq_zero_iff.mp h4)
  81
  82/-! ## Part 1: Observable Extraction = Recognition -/
  83

used by (1)

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

depends on (9)

Lean names referenced from this declaration's body.