U
plain-language theorem explainer
Defines the canonical RS-native units gauge U by setting the time base to one tick, the length base to one voxel, and the speed of light to unity while satisfying the light-cone identity. Recognition Science practitioners cite this gauge when expressing all physical quantities in the tick-voxel system without external references. The definition constructs the RSUnits record directly from the primitive tick and voxel constants and verifies the required relation by simplification.
Claim. Define the RS-units structure $U$ by $U.tau0 := 1$ (one tick), $U.ell0 := 1$ (one voxel), $U.c := 1$, together with the identity $U.c · U.tau0 = U.ell0$.
background
The module establishes an RS-native measurement system whose base standards are the ledger primitives themselves. Tick is the atomic time quantum with value 1, voxel is the causal spatial step with value 1, and c is fixed at 1 so that light traverses one voxel in one tick. The RSUnits structure packages these into a record that also carries the light-cone constraint c · tau0 = ell0 as an explicit field.
proof idea
Direct record construction. The definition supplies the three numeric fields from the sibling constants tick, voxel and c, then discharges the c_ell0_tau0 field by a single simp tactic that rewrites using the definitions of those constants.
why it matters
U supplies the fixed gauge that every subsequent RS-native calculation assumes. It is invoked by Chain structures for atomic ticks and ledgers, by aesthetic certificates such as BerlyneInvertedUCert and aestheticCost_zero_at_optimum, and by unit-ratio diagnostics in UnitsKGate. The construction realizes the c = 1 property required by the eight-tick octave and the phi-ladder scaling described in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.