Length
Spatial measurements receive the real numbers as their carrier type in the RS-native unit system. Researchers deriving constants from the phi-ladder or constructing ledger cycles cite this abbreviation when populating dimension records. The declaration is a direct abbreviation with no proof obligations or additional structure.
claimSpatial lengths take values in the real numbers $ℝ$.
background
The RSNativeUnits module sets up a measurement system whose base standards are the tick (one ledger posting interval) and the voxel (distance light travels in one tick). Length supplies the type for every quantity carrying a spatial character, consistent with the phi-ladder where lengths scale by integer powers of phi and with c fixed at unity.
proof idea
The declaration is a one-line abbreviation that equates the spatial type to the real numbers.
why it matters in Recognition Science
This abbreviation supplies the carrier type for lengths inside the Cycle structure of LedgerAlgebra and the Dimension record of Dimensions. It is referenced by tau0_sq_eq and by the kinematic display functions in KDisplayCore. The definition thereby anchors the spatial part of the forcing chain and the three-dimensional geometry that follows from the eight-tick octave.
scope and limits
- Does not assign a numerical value to the base length unit.
- Does not enforce positivity or other constraints on length values.
- Does not supply conversion factors to SI units.
- Does not encode relations to time or mass dimensions.
formal statement (Lean)
54abbrev Length := ℝ