pith. sign in
module module moderate

IndisputableMonolith.Spectra.SpectralLadder

show as:
view Lean formalization →

The SpectralLadder module supplies base frequency definitions and rail-based spectral functions for Recognition Science spectra calculations. It accepts a caller-supplied f0 (example E_coh/h) and provides a default fit-free value 1/(2 pi tau0) drawn from RS gates. Working physicists modeling coherent spectra cite these objects. The module is a collection of supporting definitions with no proofs.

claimLet $f_0$ be the supplied base frequency (e.g., $E_{coh}/h$), with default choice $f_0 = 1/(2π τ_0)$ where $τ_0$ is the RS time quantum. The module defines railFactor, frequencyOnRail, sum8 and eightGateCoherent on the spectral ladder.

background

The module sits in the Spectra domain and imports the fundamental RS time quantum $τ_0 = 1$ tick from Constants. It builds frequency objects around the eight-tick octave structure and the phi-ladder. The supplied module doc states that a default fit-free choice from RS gates is $1/(2π·τ_0)$.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the frequency ladder objects used by downstream spectral calculations in the Recognition framework. It directly supports the eight-tick octave (T7) and coherent-gate constructions that appear in the forcing chain.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (5)