meters_to_Gly
plain-language theorem explainer
The meters-to-gigalight-years conversion divides an input distance in meters by the product of one light-year in SI units and one billion. Cosmologists matching Recognition Science predictions to the observed 46.5 Gly universe radius would cite this seam. It is implemented as a direct division using the pre-defined light-year constant.
Claim. Let $r$ be a distance in meters. The equivalent distance in gigalight-years is $r / (L_y × 10^9)$, where $L_y$ is the length of one light-year in meters.
background
The SIConversion module establishes the calibration seam between RS-native units (where $c = ℓ_0 = τ_0 = 1$) and SI observables. It anchors on external Planck length and time values to express ratios such as observed radius over Planck length. SI numerical values remain CODATA-sourced inputs rather than RS predictions.
proof idea
The definition consists of a single arithmetic operation that divides the meter-valued input by the product of the light-year constant and one billion.
why it matters
This definition populates the SI conversion layer in the cosmology module, permitting numerical comparison between RS-native cosmological predictions and astronomical observations. It directly supports the reporting of quantities such as the comoving radius of the observable universe in gigalight-years. The module documentation identifies these conversions as the bridge through which external data enters the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.