freq_raw
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.