ly_SI
The declaration supplies the SI value of one light-year as 9.461e15 meters. Cosmologists converting RS-native distances to observable units cite this anchor when reporting comoving radii or Hubble parameters. It is supplied as a direct numerical definition drawn from standard astronomical conversion factors.
claimOne light-year equals $9.461 × 10^{15}$ meters.
background
RS derives all physics in native units with c = ℓ₀ = τ₀ = 1. Comparison with observations requires a calibration seam that maps theoretical ratios to SI units via external experimental anchors such as the Planck length. The module documentation states that SI numerical values are CODATA-sourced and not RS predictions; the theoretical content resides in the ratios R_obs / ℓ_P and t_age / t_P. This definition supplies one such anchor for length conversions.
proof idea
Direct definition assigning the numerical value 9.461e15 without derivation or lemmas.
why it matters in Recognition Science
This definition anchors the conversion of RS predictions to SI units and feeds the meters_to_Gly function used for observed comoving radii in the same module. It completes the reporting seam described in the module documentation, allowing theoretical distances expressed in native units to be stated in meters or Gly. No open questions are touched.
scope and limits
- Does not derive the light-year length from Recognition Science principles.
- Does not provide error bounds or uncertainty estimates.
- Does not apply to any specific cosmological model.
- Does not replace the need for Planck-scale calibration.
Lean usage
def meters_to_Gly (r_m : ℝ) : ℝ := r_m / (ly_SI * 1e9)formal statement (Lean)
61def ly_SI : ℝ := 9.461e15
proof body
Definition body.
62
63/-- 1 Gyr (billion years) in seconds. -/