tau0
plain-language theorem explainer
tau0 defines the fundamental time quantum τ₀ in RS-native units as equal to one tick. Bridge data structures and unit conversion certificates cite this definition when anchoring external constants to the RS framework. The declaration is a direct noncomputable alias to the tick constant, which is set to 1.
Claim. In RS-native units the fundamental time quantum satisfies $τ_0 = 1$, where the value 1 denotes the duration of one tick.
background
The Constants module sets the RS-native time quantum as τ₀ = 1 tick. The tick constant is defined as 1 in ℝ and serves as the base time unit, with c = 1 and ħ = φ^{-5} in the same system. The module doc states that τ₀ is the duration of one tick, the fundamental time quantum.
proof idea
This is a one-line definition that aliases tau0 directly to the tick constant.
why it matters
tau0 supplies the base time unit for the BridgeData structure that anchors G, ħ, c and for the computeRatios function that checks clock and length ratios in UnitsKGateCert. It corresponds to the fundamental time quantum in the Recognition Science framework and is used by the c_ell0_tau0 lemma to establish ℓ₀ = c · τ₀, consistent with the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.