ratio_self_similar_of_realized_closed_scale
plain-language theorem explainer
The theorem establishes that any realized closed scale model on a closed observable framework produces a constant ratio between successive observable values along the orbit. Researchers deriving hierarchy fields from geometric scale primitives cite this to replace an assumption with a derived property. The proof is a one-line wrapper that rewrites the target equality using the ratio step lemma at two consecutive indices.
Claim. Let $F$ be a closed observable framework and $H$ a realized closed scale model for $F$. Then for every integer $k$, the ratio of the observable on the orbit satisfies $F.r(F.T^{[k+2]}(H.baseState)) / F.r(F.T^{[k+1]}(H.baseState)) = F.r(F.T^{[k+1]}(H.baseState)) / F.r(F.T^{[k]}(H.baseState))$.
background
A ClosedObservableFramework consists of a countable state space $S$, transition map $T$, and positive observable $r$ obeying nontriviality and closure. A RealizedClosedScaleModel augments this with a base state, positive amplitude, and a closed geometric scale sequence such that the observable on the iterated orbit equals amplitude times the scale value at each step. The module isolates the strongest derivation currently available: once such a model exists, the two target fields of RealizedHierarchy become theorems rather than hypotheses.
proof idea
The proof is a one-line wrapper that applies realized_closed_scale_ratio_step at index $k+1$ and at index $k$, then rewrites the desired equality directly.
why it matters
This supplies the ratio_self_similar field inside toRealizedHierarchy, which packages the model into the full RealizedHierarchy interface. It thereby discharges one of the two properties listed as open in the module documentation, leaving only existence of a realized closed scale model unresolved. In the Recognition framework it realizes the self-similar fixed-point property at the level of observable ratios along the orbit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.