realized_closed_scale_ratio_step
plain-language theorem explainer
Any orbit in a ClosedObservableFramework that realizes a closed geometric scale sequence has constant adjacent ratios equal to the sequence ratio. Researchers deriving hierarchy fields from scale primitives cite it to obtain ratio self-similarity as a theorem. The proof substitutes the realization equation at consecutive steps, cancels the positive amplitude, and reduces to the scale step lemma.
Claim. Let $F$ be a closed observable framework and $H$ a realized closed scale model of $F$ with base state $b$, positive amplitude $a$, and geometric scale sequence $s$. For every natural number $k$, the ratio $F.r(F.T^{[k+1]} b)/F.r(F.T^{[k]} b)$ equals the fixed ratio of $s$.
background
A ClosedObservableFramework supplies a state space, transition map $T$, and positive observable $r$ with non-triviality. A RealizedClosedScaleModel augments this with a base state, positive amplitude, and a GeometricScaleSequence whose scale values are recovered exactly by the orbit under $T$ scaled by the amplitude; the sequence is required to be closed. The module isolates the strongest derivation currently available, turning the two target fields of RealizedHierarchy into theorems once such a model exists.
proof idea
Apply the realization equation at steps $k+1$ and $k$ to replace both observables by amplitude times the corresponding scale value. Cancel the common positive amplitude factor via mul_div_mul_left. The resulting adjacent scale ratio equals the fixed ratio by the scale_step_ratio lemma.
why it matters
The result supplies the constant-ratio step required by ratio_self_similar_of_realized_closed_scale and by the packaging into toRealizedHierarchy. It therefore converts the ratio_self_similar field from assumption to theorem, as stated in the module documentation. Within the Recognition framework it supports the self-similar fixed point and the eight-tick octave by confirming invariance of the realized orbit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.