pith. sign in
module module high

IndisputableMonolith.Spectra.SpectralLadder

show as:
view Lean formalization →

SpectralLadder module defines base frequency f0 together with rail factor, frequency-on-rail, sum8 and eight-gate-coherent constructions for the spectra domain. It accepts f0 from the caller or defaults to the fit-free value 1/(2π τ0) drawn from the RS time quantum. Researchers building spectral ladders or coherence models cite these definitions. The module contains only definitions and no theorems.

claimDefault base frequency $f_0 = 1/(2π τ_0)$. Rail factor, frequency on rail $f(r)$, eight-term sum, and coherent eight-gate frequency, all parameterized by supplied $f_0$ or the default above.

background

The module imports Constants, whose sole content is the definition of the fundamental RS time quantum τ₀ = 1 tick. It supplies spectral-ladder objects that start from a caller-provided base frequency f0 (example: E_coh/h) and offers the default fit-free choice 1/(2π τ0) drawn from RS gates. Sibling definitions railFactor, frequencyOnRail, sum8 and eightGateCoherent implement the ladder steps.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

Supplies the spectral-ladder infrastructure required by the Spectra domain. It converts the RS time quantum τ₀ into frequency rails that support eight-tick octave and coherence calculations downstream in Recognition Science.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (5)