ly_SI
plain-language theorem explainer
The definition supplies the SI length of one light-year as 9.461 × 10^15 meters. Cosmologists mapping RS-native predictions to observational data in conventional units reference this anchor. It enters as a direct numerical assignment with no derivation steps or lemmas.
Claim. One light-year equals $9.461 × 10^{15}$ meters.
background
Recognition Science operates in native units where c = ℓ₀ = τ₀ = 1 and the Planck length equals 1/√π. This module supplies the SI calibration seam so cosmological observables can be expressed in human units for comparison with data. The module documentation states that these SI numerical values are CODATA-sourced experimental inputs, not RS predictions, and that theoretical content resides in ratios such as observed radius over Planck length.
proof idea
As a definition the entry directly binds ly_SI to the literal value 9.461e15 with no lemmas or tactics applied.
why it matters
This constant is invoked by the downstream meters_to_Gly definition to convert meter-scale distances into billion light-years. It completes the SI reporting seam described in the module documentation, allowing RS-derived cosmological scales to be compared with Planck 2018 ΛCDM fits. The value itself carries no theoretical weight inside the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.