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

locality_from_ledger

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)

  83theorem locality_from_ledger (L : ZeroParameterLedger) :
  84    ∃ r : ℝ, r > 0 ∧ ∀ k, L.levels (k + 1) = r * L.levels k := by

proof body

Term-mode proof.

  85  use L.levels 1 / L.levels 0
  86  refine ⟨div_pos (L.all_positive 1) (L.all_positive 0), ?_⟩
  87  intro k
  88  have h := uniform_ratio L k
  89  rw [div_eq_div_iff (ne_of_gt (L.all_positive k)) (ne_of_gt (L.all_positive (k+1)))] at h
  90  rw [div_eq_div_iff (ne_of_gt (L.all_positive 0)) (ne_of_gt (L.all_positive 1))] at h
  91  have hk_pos := L.all_positive k
  92  field_simp
  93  linarith
  94
  95/-! ## Certificate -/
  96

used by (1)

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

depends on (4)

Lean names referenced from this declaration's body.