railFactor
plain-language theorem explainer
The railFactor definition supplies the dimensionless multiplier φ^{2n} for shell energies on rail n in the Recognition Science periodic table model. Chemists modeling φ-scaled shell energies without empirical fitting would reference this. It is realized as a one-line definition applying the real power function to the golden ratio constant raised to twice the rail index.
Claim. $railFactor(n) = φ^{2n}$ for integer rail index $n$, where $φ$ is the golden ratio constant.
background
The Periodic Table module implements a fit-free scaffold that maps the eight-tick octave to chemical shells via φ-tier rails. BlockOffsets supplies fixed integer offsets for s/p/d/f blocks (default values 0/1/2/3) with no per-element tuning. The module provides a zero-parameter API for valence cost calculations and noble gas closure detection under the 8-window neutrality condition described in the module documentation.
proof idea
The definition is a one-line wrapper that applies Real.rpow to the phi constant from Constants with exponent (2 : ℝ) * (n : ℝ).
why it matters
This definition populates the rail scaling used by railEnergy to produce dimensionful energies E_n = E_coh · φ^{2n} and by frequencyOnRail in the Spectra module. It supports the Noble Gas Closure Theorem (P0-A0) by enabling cumulative valence cost calculations that identify closures at 8-window neutrality points. The construction ties directly to the eight-tick octave (T7) and phi fixed point (T6) in the unified forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.