frequencyOnRail
plain-language theorem explainer
The definition supplies the frequency at integer rail n as the base frequency f0 scaled by the dimensionless rail factor phi to the power 2n. Modelers of spectral lines or coherence diagnostics in Recognition Science would invoke it to locate energies on the phi-ladder. The implementation is a direct one-line multiplication that delegates the scaling to the shared railFactor definition.
Claim. The frequency on rail $n$ is $f_n = f_0 · ϕ^{2n}$, where $f_0$ is the coherence energy divided by Planck's constant and $ϕ$ denotes the golden ratio.
background
The SpectralLadder module supplies basic helpers for cross-domain spectral rails obeying $f_n = f_0 · ϕ^{2n}$ with $f_0 = E_{coh}/h$, together with an eight-gate coherence test for neutrality diagnostics. The railFactor function, appearing identically in PeriodicTable, Nuclear.Octave and locally, returns the dimensionless multiplier $ϕ^{2n}$ via Real.rpow on the constant phi.
proof idea
This is a one-line wrapper that multiplies the supplied base frequency f0 by railFactor n.
why it matters
The definition populates the spectral ladder used in coherence calculations and the eight-gate test within the same module. It realizes the phi-powered rail scaling required by the Recognition forcing chain, specifically the self-similar fixed point (T6) and eight-tick octave (T7). No downstream uses appear yet, so integration with mass formulas or Berry thresholds remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.