pith. sign in
module module high

IndisputableMonolith.Cosmology.SIConversion

show as:
view Lean formalization →

The Cosmology.SIConversion module supplies SI-unit translations for RS cosmological scales, beginning with the Planck length fixed to the CODATA 2018 value. Cosmologists comparing native RS calculations against laboratory data cite these definitions for numerical checks. The module contains only constant definitions and positivity statements with no proofs.

claimThe module defines SI conversions including the Planck length $ℓ_P = √(ℏG/c³) = 1.616255 × 10^{-35}$ m with uncertainty ±0.000018 × 10^{-35} m, together with corresponding SI expressions for time, distance, and speed scales derived from the RS constants.

background

Recognition Science works in native units with c = 1 and the fundamental time quantum τ₀ = 1 tick supplied by the upstream Constants module. This module translates those scales into SI for direct comparison with observational cosmology. The supplied doc-comment anchors the Planck length to the standard formula and the 2018 CODATA numerical value.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

Provides SI equivalents that enable numerical validation of RS predictions against measured constants such as the Planck length. No downstream theorems are recorded in the dependency graph, so the module serves as a bridge layer for external comparison rather than an internal proof step.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (22)