U_tau0
plain-language theorem explainer
The lemma normalizes the fundamental time unit tau0 to unity inside the RS-native gauge U. Workers on dimensionless constants or the phi-ladder cite this when setting the tick as the base interval. Proof is immediate reflexivity after the gauge definition.
Claim. In the RS-native unit system $U$ with base time set to one tick, the duration $tau_0$ equals 1.
background
The module RSNativeUnits sets up a native measurement system treating the tick as the atomic time quantum and the voxel as the causal spatial step, with all ratios fixed by phi. The gauge U is the structure fixing tau0 to tick, ell0 to voxel, and c to 1 so that light speed is unity in these units. Upstream tau0 appears as a placeholder in Compat.Constants and as a codata-derived expression in Derivation, which the native gauge overrides for internal use.
proof idea
The proof is a one-line wrapper that applies reflexivity to the field access after unfolding the definition of U.
why it matters
This normalization anchors the time base for the RS-native system and the phi-ladder scalings used in mass and energy formulas. It supports the eight-tick octave and derivations of constants such as hbar = phi^{-5}. No direct downstream uses appear in the graph, but the result underpins the constants module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.