ell0
plain-language theorem explainer
Defines the fundamental length unit ℓ₀ as 1 in RS-native units on the voxel scale. Researchers normalizing the Recognition Science framework to c = 1 and τ₀ = 1 tick cite this when scaling all spatial quantities. The definition is a direct noncomputable assignment with no reduction steps.
Claim. In RS-native units the fundamental length unit satisfies $ℓ_0 := 1$.
background
The Constants module adopts RS-native units in which the fundamental time quantum τ₀ equals 1 tick. The upstream derivation supplies the relation ell0 := c_codata * tau0, which collapses to 1 once c_codata = 1 and tau0 = 1 under the native-unit convention. This choice fixes the voxel as the base spatial measure for all subsequent length-dependent expressions.
proof idea
Direct definition that assigns the constant value 1. It is a one-line wrapper implementing the RS-native unit convention where the light-cone identity holds with c = 1.
why it matters
Anchors the length scale for BridgeData (external anchors G, ħ, c, tau0, ell0) and for UnitsKGateCert ratio computations. It is invoked by the light-cone lemma c_ell0_tau0 and by ell0_pos. In the framework this realizes the spatial unit inside the eight-tick octave with D = 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.