Pith. sign in
module module high

IndisputableMonolith.Cosmology.SIConversion

show as:
view Lean formalization →

This module supplies SI-unit conversions for Recognition Science cosmological constants, including the Planck length fixed at the CODATA 2018 value. Cosmologists comparing RS-native predictions against laboratory and astronomical data would cite these definitions. The module consists entirely of definitions that import the RS time quantum from Constants and express the conversions directly.

claim$\ell_P = \sqrt{\hbar G / c^3} = 1.616255 \times 10^{-35}\,\mathrm{m}$ (CODATA 2018), together with the corresponding SI expressions for Planck time, $c$, Mpc, ly, and Gyr.

background

The module sits in the Cosmology domain and imports IndisputableMonolith.Constants, whose sole documented object is the fundamental RS time quantum $\tau_0 = 1$ tick. All quantities are therefore expressed relative to this tick in RS-native units before conversion to meters, seconds, and other SI measures. The supplied sibling definitions (planck_length_SI, planck_time_SI, c_SI, Mpc_SI, etc.) and their positivity lemmas constitute the entire content.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module anchors RS cosmology to experimental numbers by supplying the Planck length and related constants in SI units. It thereby supports any later numerical or observational comparison within the cosmology section, directly referencing the CODATA 2018 measurement quoted in the module documentation.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (22)