scale
plain-language theorem explainer
The definition assigns to each natural number k the real number phi raised to the power k. Cosmologists mapping LSS regimes and applied researchers defining resonant devices cite it to locate lengths on the phi-ladder. It is introduced as a direct power expression with no reduction steps or lemmas.
Claim. For each natural number $k$, the scale length is defined by $s(k) := phi^k$.
background
The module sets five canonical LSS regimes (CMB acoustic scale, baryon acoustic oscillation, galaxy clusters, filamentary structure, cosmic voids) with configDim D = 5. Each regime occupies one rung on the phi-ladder in comoving length. The phi-ladder is the sequence of lengths generated by successive powers of the golden ratio, the self-similar fixed point forced in the Recognition Science chain.
proof idea
The declaration is a direct definition that sets the scale at rung k to phi raised to k. No lemmas or tactics are invoked.
why it matters
This supplies the explicit phi-ladder lengths used by ResonantScale (a length r is resonant when it equals phi to an integer power) and by phi_energy_rung_pos. It also feeds scale_fibonacci and pentatonicSize in the musical-scale derivations, and PhiInt elements of Z[phi]. The definition therefore anchors the LSS regime mapping stated in the module documentation and connects to the phi fixed-point step of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.