obs_radius_m
plain-language theorem explainer
The definition supplies the observed comoving radius of the universe in meters as 4.40 × 10^26 from the Planck 2018 ΛCDM fit. Cosmologists comparing Recognition Science scale predictions to data would cite this anchor. The assignment is a direct numerical definition with no computation.
Claim. The observed comoving radius of the observable universe is given by $r = 4.40 × 10^{26}$ meters, taken from the Planck 2018 ΛCDM fit that corresponds to 46.5 Gly.
background
The module sets up the SI calibration seam that converts Recognition Science native units (c = ℓ₀ = τ₀ = 1) into meters and seconds for comparison with observations. The Planck length and time act as the external bridge, with their SI values treated as experimental inputs rather than RS predictions. Upstream structures supply the J-cost minimization from PhysicsComplexityStructure, the ledger factorization from DAlembert, and the spectral emergence of gauge content from SpectralEmergence that justify the ratios calibrated by this constant.
proof idea
This is a direct definition that assigns the numerical value 4.40e26. No lemmas or tactics are applied beyond the literal constant from the doc-comment.
why it matters
This definition anchors the conversion of Recognition Science cosmological predictions into SI units, enabling direct comparison with observations. It fills the reporting seam in the module where ratios such as R_obs / ℓ_P carry the theoretical content. It connects to the forcing chain landmarks T7 eight-tick octave and T8 D = 3 by providing the observable scale against which phi-ladder mass and length predictions are tested.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.