pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Spectra.SpectralLadder

show as:
view Lean formalization →

The SpectralLadder module supplies base frequency definitions and rail-based mappings for Recognition Science spectra. A caller provides f0, defaulting to 1/(2π τ₀) from RS gates and the time quantum. It defines railFactor, frequencyOnRail, sum8, and eightGateCoherent to build discrete ladders. Foundational physicists cite it when constructing spectra from the eight-tick octave. The module contains only definitions.

claimThe module defines base frequency $f_0$ (e.g., $E_{coh}/h$) with default $1/(2π τ_0)$, plus railFactor, frequencyOnRail, sum8, and eightGateCoherent for the spectral ladder.

background

Recognition Science builds spectra on the phi-ladder and eight-tick octave (T7) from the forcing chain. The imported Constants module fixes the RS time quantum τ₀ = 1 tick. This module introduces the spectral ladder starting from an externally supplied base frequency f0, with a fit-free default 1/(2π τ₀) drawn from RS gates as stated in the module doc-comment.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the frequency ladder scaffolding that supports spectra constructions in the Recognition framework. It aligns with the eight-tick octave (T7) and prepares discrete sums consistent with the Recognition Composition Law. No specific parent theorems are listed in the used-by edges.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (5)