realized_uniform_ratios

formal source

  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 =
 114      (realized_to_ladder F H).levels 1 + (realized_to_ladder F H).levels 0 :=
 115  H.additive_posting
 116
 117/-! ## Main Theorem: Realized Hierarchy Forces φ -/
 118
 119/-- **End-to-end theorem**: A realized hierarchy on a closed observable
 120framework forces the scale ratio to be φ.
 121
 122This replaces the old bridge that required external `sensitivity` and
 123`HasAdditiveComposition` hypotheses. Both are now derived from
 124the realization's `ratio_self_similar` and `additive_posting` fields,