binary_is_minimal

formal source

  74    ∀ n, L.levels n / L.levels (n + 1) = L.levels 0 / L.levels 1 :=
  75  L.no_external_scale 1 one_pos
  76
  77theorem binary_is_minimal (L : ZeroParameterLedger) (comp : LocalComposition L) :
  78    ∀ k, comp.compose k = comp.compose 0 := by
  79  intro k
  80  rw [comp.compose_from_levels, comp.compose_from_levels]
  81  exact uniform_ratio L k
  82
  83theorem locality_from_ledger (L : ZeroParameterLedger) :
  84    ∃ r : ℝ, r > 0 ∧ ∀ k, L.levels (k + 1) = r * L.levels k := by
  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
  97structure LocalityCert where
  98  uniform : ∀ (L : ZeroParameterLedger), ∀ n,
  99    L.levels n / L.levels (n + 1) = L.levels 0 / L.levels 1
 100  geometric : ∀ (L : ZeroParameterLedger),
 101    ∃ r : ℝ, r > 0 ∧ ∀ k, L.levels (k + 1) = r * L.levels k
 102
 103theorem locality_cert_exists : Nonempty LocalityCert :=
 104  ⟨{ uniform := fun L => uniform_ratio L
 105     geometric := fun L => locality_from_ledger L }⟩
 106
 107end IndisputableMonolith.Foundation.LocalityFromLedger