railEnergy
The railEnergy definition supplies the dimensionful energy on rail n as the product of the base cohesion energy and the dimensionless factor phi to the power 2n. Modelers of the periodic table in Recognition Science cite it to assign energies to phi-tier shells in a zero-parameter scaffold. The definition is a direct scalar multiplication that reuses the railFactor already defined in the same module.
claim$E_n = E_{coh} · ϕ^{2n}$ for integer rail index $n$, where $E_{coh}$ is the cohesion energy scale and ϕ is the golden-ratio fixed point.
background
The PeriodicTable module implements an octave-to-eight-tick mapping for chemistry using phi-tier rails together with fixed block offsets and an eight-window neutrality predicate. RailFactor supplies the dimensionless multiplier ϕ^{2n} on each rail; the same expression appears in the Nuclear.Octave and Spectra.SpectralLadder modules. E_coh is taken from the Constants bundle that also supplies the other RS-native scales (c = 1, ħ = ϕ^{-5}, G = ϕ^5/π). Module documentation states that noble-gas closures occur exactly where the cumulative valence cost satisfies eight-window neutrality, the chemical counterpart of the fundamental eight-tick ledger balance.
proof idea
One-line wrapper that multiplies the cohesion energy constant by the railFactor definition already present in the module.
why it matters in Recognition Science
The definition supplies the dimensionful energies required by the Noble Gas Closure Theorem (P0-A0) stated in the module documentation. It inherits the phi-ladder and eight-tick octave structure from the foundation (T7) and is used to generate the forced set {2, 10, 18, 36, 54, 86} without per-element tuning. Because used_by is currently empty, the declaration remains an open interface for downstream chemical predictions.
scope and limits
- Does not incorporate block offsets or sub-rail corrections.
- Does not perform per-element fitting or dataset calibration.
- Does not compute ionization potentials or other spectroscopic observables.
- Does not enforce the eight-window neutrality predicate itself.
formal statement (Lean)
71def railEnergy (n : ℤ) : ℝ :=
proof body
Definition body.
72 IndisputableMonolith.Constants.E_coh * railFactor n
73
74/- Sliding 8‑window sum used for neutrality tests. -/