tau0
plain-language theorem explainer
τ₀ is the fundamental tick duration in RS-native units, introduced as a direct alias to the core tick constant. Bridge and certificate code cite this placeholder when anchoring time scales for ratio checks and data structures. The definition is a one-line assignment with no further reduction.
Claim. Define the fundamental tick duration by $τ_0 := 1$ in RS-native units, where the tick is the base time quantum.
background
The Compat.Constants module supplies project-wide constants and minimal structural lemmas. τ₀ acts as a placeholder for the duration of one fundamental tick, re-exported for compatibility layers. Upstream, the core Constants.tau0 is documented as the fundamental time unit τ₀ (duration of one tick) in RS-native units, while tick is defined by the equation tick = 1. The RSNativeUnits module repeats the same tick definition inside the Time type. This choice aligns with the eight-tick cycle as the fundamental evolution period.
proof idea
The declaration is a one-line definition that directly aliases IndisputableMonolith.Constants.tick.
why it matters
This definition supplies the time anchor required by BridgeData structures and by the ratio computations inside UnitsKGateCert. It is referenced by the light-cone lemma c_ell0_tau0 that states ℓ₀ = c · τ₀. In the Recognition framework it instantiates the T7 eight-tick octave as the base period for all evolution.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.