Frequency
plain-language theorem explainer
Frequency supplies the real-number type for rates measured in inverse ticks inside the RS-native ledger system. Chemists and vacuum-energy modelers cite it when scaling rates or power outputs that depend on the frequency quantum. The declaration is a one-line type abbreviation carrying no computational content or proof obligations.
Claim. Frequency is the type of real numbers $ℝ$ used to represent frequencies in units of inverse ticks.
background
The RS-native measurement system takes tick (τ₀) as the atomic time quantum and voxel (ℓ₀) as the spatial step with c = 1. Derived quanta are coh = φ^{-5} for energy and act = ħ for action. All quantities sit on the φ-ladder φ^n that supplies natural scalings for masses, energies, times and lengths.
proof idea
This is a type abbreviation with an empty proof body.
why it matters
Downstream definitions such as freqQuantum (1/tick), freq_raw and to_hertz rely on it for scaling and SI conversion. It appears in enzyme_enhances_rate for rate calculations and in SelfSustaining for vacuum power scaling. The type anchors frequency-dependent steps on the φ-ladder and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.