realized_ratio_eq_base

formal source

  80/-! ## Derived: Uniform Scale Ladder -/
  81
  82/-- All adjacent ratios in a realized hierarchy equal the base ratio. -/
  83theorem realized_ratio_eq_base (F : ClosedObservableFramework)
  84    (H : RealizedHierarchy F) :
  85    ∀ k, H.levels (k + 1) / H.levels k = H.levels 1 / H.levels 0 := by
  86  intro k
  87  induction k with
  88  | zero => rfl
  89  | succ k ih =>
  90    have h := H.ratio_self_similar k
  91    rw [h, ih]
  92
  93/-- All adjacent ratios in a realized hierarchy are equal. -/
  94theorem realized_uniform_ratios (F : ClosedObservableFramework)
  95    (H : RealizedHierarchy F) :
  96    ∀ j k, H.levels (j + 1) / H.levels j = H.levels (k + 1) / H.levels k := by
  97  intro j k
  98  rw [realized_ratio_eq_base F H j, realized_ratio_eq_base F H k]
  99
 100/-- Construct a `UniformScaleLadder` from a realized hierarchy. -/
 101noncomputable def realized_to_ladder (F : ClosedObservableFramework)
 102    (H : RealizedHierarchy F) : UniformScaleLadder :=
 103  no_free_scale_forces_uniform
 104    H.levels
 105    H.levels_pos
 106    (realized_uniform_ratios F H)
 107    H.growth
 108
 109/-- The realized hierarchy's additive posting gives the Fibonacci relation
 110on the uniform scale ladder. -/
 111theorem realized_additive_closure (F : ClosedObservableFramework)
 112    (H : RealizedHierarchy F) :
 113    (realized_to_ladder F H).levels 2 =