ell0
plain-language theorem explainer
The declaration supplies the physical value of the RS fundamental length by multiplying the CODATA speed of light by the derived tick duration tau0. Bridge data structures and unit certification routines cite this when mapping RS voxels to laboratory lengths. It is a one-line definition that composes the imported c value with the square-root expression for tau0 obtained from the relation tau0 squared equals hbar G over pi c to the fifth.
Claim. Define the fundamental length scale by the product of the CODATA speed of light and the derived tick duration: let $c = 299792458$ m/s and let $tau_0 = sqrt(hbar G / (pi c^3)) / c$; then ell_0 = c * tau_0.
background
The module anchors physical constants to CODATA reference values for c, hbar and G while deriving the remaining scales from Recognition Science primitives. The tick duration tau0 is obtained from the square-root formula sqrt(hbar_codata * G_codata / (pi * c_codata^3)) / c_codata, which satisfies the key lemma tau0 squared equals hbar G over pi c to the fifth. The module imports Compat.Constants for the placeholder tick and Constants for the native tick definition.
proof idea
This is a one-line definition that multiplies the CODATA speed of light by the tau0 expression already defined in the same module via the square-root formula.
why it matters
This supplies the length anchor for the BridgeData structure that provides external G, hbar, c, tau0 and ell0 values without axioms. It is used in computeRatios to form clock and length ratios against RSUnits and underpins the lemma c_ell0_tau0 that recovers the light-cone relation in native units. The definition closes the loop from the temporal scale tau0 to the spatial voxel size, consistent with the forcing chain that yields D=3 and the eight-tick period.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.