toRealizedHierarchy

formal source

  87/-- The earlier closed-scale model packages into the later
  88`RealizedHierarchy` interface, with the two critical fields now proved
  89rather than assumed. -/
  90noncomputable def toRealizedHierarchy
  91    (F : ClosedObservableFramework) (H : RealizedClosedScaleModel F) :
  92    RealizedHierarchy F where
  93  baseState := H.baseState
  94  levels_eq := by
  95    intro k
  96    rfl
  97  levels_pos := by
  98    intro k
  99    exact F.r_pos _
 100  growth := by
 101    rw [realized_closed_scale_ratio_step F H 0]
 102    exact H.growth
 103  ratio_self_similar := ratio_self_similar_of_realized_closed_scale F H
 104  additive_posting := by
 105    simpa using additive_posting_of_realized_closed_scale F H
 106
 107end HierarchyRealizationFromScale
 108end Foundation
 109end IndisputableMonolith