freqQuantum
freqQuantum defines the base frequency unit in the RS-native system as the reciprocal of the fundamental time quantum tick. Researchers expressing frequencies on the phi-ladder or converting to raw ledger scales would cite this constant. The definition is a direct noncomputable assignment of 1 divided by the imported tick value.
claimThe frequency quantum is defined by $f_Q = 1 / τ_0$, where $τ_0$ is the fundamental RS time quantum (tick) and frequency values are elements of $ℝ$.
background
The RS-Native Measurement System module establishes tick ($τ_0$) as the atomic time quantum with value 1 and voxel as the corresponding length quantum, enforcing $c=1$. Frequency is introduced as the type alias $ℝ$, while derived units include the coherence quantum $E_{coh}=φ^{-5}$ and action quantum $ħ=E_{coh}·τ_0$. The phi-ladder organizes all scalings via integer powers of $φ$. Upstream, the tick constant is supplied directly from IndisputableMonolith.Constants as the ledger posting interval, and the scale function from LargeScaleStructureFromRS supplies $φ^k$ for ladder steps.
proof idea
The declaration is a one-line definition that directly assigns the reciprocal of the tick constant imported from Constants.RSNativeUnits and Constants.
why it matters in Recognition Science
freqQuantum supplies the conversion factor that freq_raw applies to map arbitrary frequencies onto the raw RS scale. It anchors frequency expressions to the fundamental time quantum, supporting the eight-tick octave (T7) and the overall forcing chain from T0 to T8. The definition closes the base-unit layer before phi-ladder mass and energy formulas are applied.
scope and limits
- Does not assign a numerical SI value to the frequency quantum.
- Does not incorporate phi-ladder rung adjustments or gap(Z) corrections.
- Does not derive tick from the J-uniqueness or RCL functional equation.
- Does not address frequency spectra or Berry creation thresholds.
Lean usage
def demo (f : Frequency) : ℝ := f * freqQuantumformal statement (Lean)
128@[simp] noncomputable def freqQuantum : Frequency := 1 / tick
proof body
Definition body.
129
130/-- Convert frequency to raw RS scale. -/