UniformScaleLadder

formal source

  33
  34/-- A scale ladder extracted from multilevel composition: a sequence
  35of positive level sizes with a uniform scaling ratio. -/
  36structure UniformScaleLadder where
  37  levels : ℕ → ℝ
  38  levels_pos : ∀ k, 0 < levels k
  39  ratio : ℝ
  40  ratio_gt_one : 1 < ratio
  41  uniform_scaling : ∀ k, levels (k + 1) = ratio * levels k
  42
  43/-- **No-free-scale theorem**: In a zero-parameter ledger, if
  44adjacent level ratios could differ, each independent ratio would
  45constitute a free real parameter.  Therefore all adjacent ratios
  46must be equal, giving a uniform scale ladder. -/
  47noncomputable def no_free_scale_forces_uniform
  48    (levels : ℕ → ℝ)
  49    (levels_pos : ∀ k, 0 < levels k)
  50    (ratios_equal : ∀ j k, levels (j + 1) / levels j = levels (k + 1) / levels k)
  51    (ratio_gt_one : 1 < levels 1 / levels 0) :
  52    UniformScaleLadder :=
  53  { levels := levels
  54    levels_pos := levels_pos
  55    ratio := levels 1 / levels 0
  56    ratio_gt_one := ratio_gt_one
  57    uniform_scaling := by
  58      intro k
  59      have hratio := ratios_equal k 0
  60      have hk_pos := levels_pos k
  61      have h0_pos := levels_pos 0
  62      rw [div_eq_div_iff (ne_of_gt hk_pos) (ne_of_gt h0_pos)] at hratio
  63      rw [mul_comm (levels 1) (levels k)] at hratio
  64      have : levels (k + 1) = levels 1 / levels 0 * levels k := by
  65        field_simp
  66        linarith