freq_raw
This definition converts an input frequency value to raw RS scale by multiplying it by the fundamental frequency quantum. Physicists using the Recognition Science native unit system cite it when expressing frequencies in tick-based units without SI anchors. The implementation is a direct multiplication marked for simplification in algebraic reductions.
claimLet $f$ be a real-valued frequency. Then the raw RS frequency is $f$ scaled by the quantum $1/τ_0$, where $τ_0$ is the fundamental tick interval.
background
The RS-Native Measurement System treats tick ($τ_0$) as the atomic time quantum and voxel ($ℓ_0$) as the corresponding spatial step, with $c=1$ by construction. Derived quantities include the coherence quantum $E_{coh}=φ^{-5}$ and action quantum $ħ=E_{coh}·τ_0$. All scales sit on the φ-ladder, so integer powers of φ fix masses, energies, and frequencies without external constants.
proof idea
Direct definition that multiplies the input by freqQuantum (itself defined as $1/tick$). The @[simp] attribute enables automatic reduction in subsequent algebraic steps.
why it matters in Recognition Science
This definition anchors frequency expressions inside the RS-native system where all ratios derive from φ alone. It supports the module's goal of expressing physics directly in ledger primitives (tick/voxel/coh/act) and feeds any later derivations that require frequency scaling on the φ-ladder.
scope and limits
- Does not perform conversion to SI frequency units.
- Does not incorporate external calibration constants.
- Does not adjust for relativistic Doppler or other dynamical effects.
- Does not assign numerical values beyond the quantum scaling factor.
formal statement (Lean)
131@[simp] noncomputable def freq_raw (f : Frequency) : ℝ := f * freqQuantum
proof body
Definition body.
132
133/-- Momentum quantum: E_coh/c = E_coh (since c = 1). -/