tick
plain-language theorem explainer
The definition sets the fundamental time quantum τ₀ equal to the base constant from Constants in the RS-native system. Researchers expressing times, periods, or frequencies in tick/voxel units cite it to keep all quantities dimensionless with respect to the ledger primitives. It is a direct one-line alias to the upstream constant fixed at 1.
Claim. Let $τ_0$ denote the fundamental time quantum. Then $τ_0 := 1$ where time is represented by the real numbers.
background
The module establishes an RS-native unit system whose base standards are the ledger primitives. Tick (τ₀) is the atomic time quantum, one discrete ledger posting interval; voxel (ℓ₀) is the corresponding length quantum. Time is the type alias ℝ. Upstream, Constants.tick supplies the value 1 together with the notation τ₀ and the remark that one octave equals 8 ticks.
proof idea
One-line definition that directly aliases the upstream constant Constants.tick.
why it matters
This supplies the base time unit for the entire native system and is referenced by forty downstream declarations, including the 8-window neutrality theorem in photobiomodulation and the carrier-period band for fast radio bursts. It implements the eight-tick octave (T7) by fixing the period unit and supports the φ-ladder scaling of all derived quantities. The module also records c = 1 and the optional SI calibration path.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.