90noncomputable def toRealizedHierarchy 91 (F : ClosedObservableFramework) (H : RealizedClosedScaleModel F) : 92 RealizedHierarchy F where 93 baseState := H.baseState
proof body
Definition body.
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
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.