Mpc_SI
Mpc_SI supplies the IAU 2012 length of one megaparsec in meters as the external constant 3.0857e22. Cosmologists converting RS-native Hubble rates or distances into km/s/Mpc units cite this anchor to match observations. The declaration is a direct numerical assignment with no computation or lemmas.
claimOne megaparsec equals $3.0857 × 10^{22}$ meters, where 1 pc = $648000/π$ AU and 1 AU = 149597870700 m exactly.
background
Recognition Science derives physics in native units with c = ℓ₀ = τ₀ = 1. The Cosmology.SIConversion module supplies external SI calibration constants so that RS predictions can be compared with observations in meters, seconds, and km/s/Mpc. Mpc_SI is one such anchor; its value is taken from the IAU 2012 definition rather than derived inside the theory.
proof idea
The definition directly assigns the numerical value 3.0857e22. No lemmas or tactics are applied; it is a constant declaration.
why it matters in Recognition Science
Mpc_SI anchors the SI reporting seam and feeds the conversion def hubble_to_kms_mpc, which scales a native Hubble parameter by the inverse Planck time and Mpc_SI to produce km/s/Mpc. It also supports the positivity theorem Mpc_SI_pos. The module treats all such SI numbers as external calibration points, not RS predictions, consistent with the framework's separation of native theory from human-unit reporting.
scope and limits
- Does not derive the megaparsec length from RS axioms or the phi-ladder.
- Does not claim the numerical value is a theoretical prediction.
- Applies strictly to the IAU 2012 definition of the parsec.
- Does not address redshift or other cosmological corrections.
formal statement (Lean)
58def Mpc_SI : ℝ := 3.0857e22
proof body
Definition body.
59
60/-- 1 light-year in meters. -/