No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
18def railFactor (n : ℤ) : ℝ :=
proof body
Definition body.
19 Real.rpow IndisputableMonolith.Constants.phi ((2 : ℝ) * (n : ℝ))
20
21/‑ Level energy proxy on rail n with sub‑rail offset δ (integer). -/
used by (4)
From the project-wide theorem graph. These declarations reference this one in their body.
-
railEnergy
in IndisputableMonolith.Chemistry.PeriodicTable
decl_use
-
railFactor
in IndisputableMonolith.Chemistry.PeriodicTable
decl_use
-
frequencyOnRail
in IndisputableMonolith.Spectra.SpectralLadder
decl_use
-
railFactor
in IndisputableMonolith.Spectra.SpectralLadder
decl_use
depends on (5)
Lean names referenced from this declaration's body.
-
railFactor
in IndisputableMonolith.Chemistry.PeriodicTable
decl_use
-
Constants
in IndisputableMonolith.CPM.LawOfExistence
decl_use
-
sub
in IndisputableMonolith.Numerics.Interval.Basic
decl_use
-
sub
in IndisputableMonolith.RecogSpec.Core
decl_use
-
railFactor
in IndisputableMonolith.Spectra.SpectralLadder
decl_use