scale_step_ratio
plain-language theorem explainer
For any geometric scale sequence S with base ratio r > 0 and r ≠ 1, the ratio of consecutive scales equals r constantly. Researchers deriving constant ratios for realized hierarchies from scale primitives would cite this when closing the ratio_self_similar property. The proof is a short algebraic reduction that unfolds the power definition of scale, applies the successor exponent rule, and cancels after proving non-vanishing.
Claim. Let $S$ be a geometric scale sequence with ratio $r > 0$ and $r ≠ 1$. Then for every natural number $k$, the scale function satisfies $S.scale(k+1) / S.scale(k) = r$.
background
The module isolates derivations of realized-hierarchy fields once a ClosedObservableFramework realizes an earlier GeometricScaleSequence that is closed under ledgerCompose. GeometricScaleSequence is the structure carrying a ratio $r > 0$, $r ≠ 1$, together with the scale map that sends each natural number to the corresponding term in the geometric progression. Upstream, the cosmology scale definition supplies the concrete case scale(k) = phi^k, while the asteroid spectroscopy class records the same phi^k spectral progression as an observable signature.
proof idea
The term proof unfolds the scale definition inside GeometricScaleSequence, rewrites with the successor power rule, introduces the two non-zero hypotheses via ne_of_gt and pow_ne_zero, then finishes with simpa on mul_div_cancel_left₀.
why it matters
The result supplies the constant adjacent ratio used by realized_closed_scale_ratio_step to turn the realized orbit into a theorem rather than an assumption. It thereby advances the module goal of making ratio_self_similar and additive_posting provable once a closed scale model exists. In the Recognition Science setting this supports the geometric scaling step on the phi-ladder and the self-similar fixed point forced at T6. The remaining open question, stated in the module doc, is existence of such a realized closed scale model from ClosedObservableFramework alone.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.