railFactor
plain-language theorem explainer
Rail factor supplies the dimensionless multiplier phi to the power 2n for scaling energies or frequencies along integer rails in the phi-ladder. Nuclear spectra and periodic table calculations cite this definition to obtain uniform scaling without element-specific tuning. The implementation is a direct real exponentiation of the golden ratio constant.
Claim. The rail factor for an integer rail index $n$ equals $phi^{2n}$, where $phi$ is the golden ratio constant.
background
The Nuclear.Octave module defines railFactor to support level energy proxies within the eight-tick octave structure. It relies on the phi constant from the Constants bundle. Upstream definitions in SpectralLadder and PeriodicTable state the same form as the dimensionless shell rail multiplier (E_n/E_coh) at rail n: phi^{2n}.
proof idea
The definition directly invokes Real.rpow on the constant phi with exponent 2 times n. It is a one-line wrapper with no lemmas or tactics applied.
why it matters
This definition feeds railEnergy in PeriodicTable and frequencyOnRail in SpectralLadder. It realizes the phi-ladder scaling required by the Recognition Composition Law and the eight-tick octave (T7). It supplies the uniform multiplier used in nuclear and spectral applications.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.