realized_additive_closure

formal source

 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,
 125which are RS-native physical principles. -/
 126theorem realized_hierarchy_forces_phi (F : ClosedObservableFramework)
 127    (H : RealizedHierarchy F) :
 128    (realized_to_ladder F H).ratio = PhiForcing.φ :=
 129  hierarchy_emergence_forces_phi
 130    (realized_to_ladder F H)
 131    (realized_additive_closure F H)
 132
 133/-! ## Non-Uniform Ratios Create Continuous Moduli
 134
 135The following theorem proves that `ratio_self_similar` is the ONLY option
 136consistent with `no_continuous_moduli`. If the ratio function were not
 137constant, the carrier would need to encode a continuously varying
 138parameter, contradicting the closed observable framework. -/
 139
 140/-- If hierarchy levels have non-uniform ratios and the observable
 141separates hierarchy states, then continuous moduli exist in the carrier.