Mpc_SI_pos
plain-language theorem explainer
The theorem establishes positivity of the SI megaparsec anchor used for cosmological distance conversions. Researchers bridging Recognition Science native units to observational data in meters would cite it to confirm the calibration constant supports positive lengths. The proof is a one-line wrapper that unfolds the explicit numerical definition and applies numerical normalization.
Claim. Let $Mpc_{SI}$ denote one megaparsec expressed in meters via the IAU 2012 definition, where $1$ pc $= 648000/π$ AU and $1$ AU $= 149597870700$ m. Then $0 < Mpc_{SI}$ holds with $Mpc_{SI} = 3.0857 × 10^{22}$.
background
The module supplies the SI calibration seam for cosmological observables. Recognition Science works in native units with $c = ℓ_0 = τ_0 = 1$, so external anchors such as the Planck length in meters and the megaparsec in meters are required to express predictions in human units. Mpc_SI is introduced as the concrete numerical constant $3.0857e22$ representing one megaparsec.
proof idea
The proof is a one-line wrapper that unfolds the definition of Mpc_SI to its explicit numerical value and invokes norm_num to confirm the inequality.
why it matters
The result secures the positivity of the megaparsec anchor inside the SI calibration seam. It supports the module's conversion functions by guaranteeing the bridge ratio from native units remains positive and well-defined. The declaration aligns with the module's epistemic status that SI numerical values are external calibration facts rather than Recognition Science predictions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.