scale_pos
plain-language theorem explainer
The theorem shows that the scale function, defined as phi to the power k for natural k, yields a strictly positive real number. Cosmologists building Recognition Science models of large-scale structure cite it to confirm that all comoving lengths on the phi-ladder remain positive. The proof is a direct one-line application of the standard positivity lemma for powers with positive base.
Claim. For every natural number $k$, $0 < s(k)$ where $s(k) := r^k$ and $r > 0$ is the self-similar fixed point of the forcing chain.
background
The LargeScaleStructureFromRS module places five canonical regimes (CMB acoustic scale, baryon acoustic oscillation, galaxy clusters, filamentary structure, cosmic voids) one rung apart on the phi-ladder in comoving length, with configDim D = 5. The scale function is defined as the noncomputable map sending each natural number k to phi^k. This positivity statement depends on the upstream definition of scale together with the known positivity of phi.
proof idea
The proof is a one-line wrapper that applies the lemma pow_pos to the positivity of phi and the natural-number exponent k.
why it matters
The result is invoked inside largeScaleStructureCert to certify the five regimes with positive scales. It also supports the GeometricScaleSequence structure in PhiForcingDerived and the ILGState record in CPMInstance. It supplies the required positivity for the phi-ladder cosmology, consistent with the self-similar fixed point (T6) and the eight-tick octave (T7) of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.