U_ell0
plain-language theorem explainer
The lemma normalizes the base length ell0 to unity inside the RS-native gauge U. Researchers deriving the phi-ladder masses or the constants hbar = phi^{-5} and G = phi^5/pi would cite this to fix the scale before applying the recognition composition law. The proof is a direct reflexivity step once the unit record is unfolded.
Claim. In the RS-native gauge with base time quantum one tick and base length one voxel, the fundamental length satisfies $ell_0 = 1$.
background
The module defines an RS-native unit system whose base standards are the ledger primitives tick (atomic time quantum) and voxel (spatial step light traverses in one tick). All physics is expressed in these units with c = 1 and all dimensionless ratios fixed by phi alone; the phi-ladder supplies the natural scalings phi^n for masses, energies, times and lengths. The structure U records tau0 := tick, ell0 := voxel and c := c together with the consistency condition c_ell0_tau0 proved by simplification.
proof idea
One-line wrapper that applies reflexivity after the definition of U unfolds ell0 to voxel and the upstream ell0 definition supplies the value 1.
why it matters
This normalization anchors the entire RS-native system so that subsequent derivations of constants and the mass formula yardstick * phi^(rung - 8 + gap(Z)) proceed without external scale factors. It supports the forcing chain steps that fix D = 3 and the alpha band inside (137.030, 137.039). The declaration closes the gauge choice required before the recognition composition law can be applied to physical quantities.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.