ratio_only

formal source

  49
  50/-! ## Key Theorems -/
  51
  52theorem ratio_only (L : ZeroParameterLedger) :
  53    ∀ m n : ℕ, L.levels m / L.levels n =
  54      (L.levels 0 / L.levels 1) ^ ((m : ℤ) - n) := by
  55  intro m n
  56  induction m with
  57  | zero =>
  58    induction n with
  59    | zero => simp
  60    | succ n ih =>
  61      have h := L.no_external_scale 1 one_pos n
  62      rw [div_eq_div_iff (ne_of_gt (L.all_positive 0)) (ne_of_gt (L.all_positive (n + 1)))]
  63      have := L.no_external_scale 1 one_pos 0
  64      rw [Nat.zero_add] at this
  65      rw [div_eq_div_iff (ne_of_gt (L.all_positive 0)) (ne_of_gt (L.all_positive 1))] at this
  66      nlinarith [L.all_positive 0, L.all_positive 1, L.all_positive n, L.all_positive (n+1)]
  67  | succ m ih =>
  68    have h := L.no_external_scale 1 one_pos m
  69    rw [div_eq_div_iff (ne_of_gt (L.all_positive (m+1))) (ne_of_gt (L.all_positive n))]
  70    have hm := L.no_external_scale 1 one_pos 0
  71    nlinarith [L.all_positive m, L.all_positive (m+1), L.all_positive n, L.all_positive 0, L.all_positive 1]
  72
  73theorem uniform_ratio (L : ZeroParameterLedger) :
  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