Length
plain-language theorem explainer
Length supplies the real-number carrier for all spatial quantities in the RS-native system anchored to voxels and the phi-ladder. Workers deriving kinematic ratios or dimensional consistency in ledger cycles reference it when moving between discrete postings and continuum limits. The declaration is a direct abbreviation that binds the type to the reals, permitting immediate application of standard real arithmetic.
Claim. In the Recognition-Science native units, spatial extent is carried by the real numbers: lengths belong to $L = {x | x : {R}}$, with base step given by the voxel and scaling governed by the phi-ladder.
background
The module sets up an RS-native measurement system whose base standards are the tick (one discrete ledger interval) and the voxel (distance light travels in one tick). Length is the type assigned to quantities whose dimensional signature is [L¹ T⁰ M⁰]. The Dimension structure records independent exponents for length, time and mass, while dim_one supplies the zero-exponent case used for dimensionless ratios.
proof idea
Direct abbreviation with no proof obligations; the identifier is simply bound to the real numbers so that downstream algebraic and dimensional constructions inherit ordinary real arithmetic.
why it matters
The abbreviation is invoked by the Dimension structure, by tau0_sq_eq (which equates tau0 squared to hbar G over pi c to the fifth), and by display routines that convert between tau0 and kinematic wavelengths. It therefore supplies the spatial carrier required for the phi-ladder mass formula and for the eight-tick octave that fixes D = 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.