pith. machine review for the scientific record. sign in
def definition def or abbrev high

planck_to_seconds

show as:
view Lean formalization →

Converts a time expressed as a multiple of the Planck time into seconds via direct scaling by the fixed SI Planck time. Cosmologists matching Recognition Science predictions for cosmic age or expansion rates to observational data would apply this conversion. The definition is a one-line scalar multiplication by the CODATA-sourced constant.

claimIf $t$ denotes a time expressed as a multiple of the Planck time, the corresponding time in seconds is $t$ times $5.391247$ times $10^{-44}$.

background

Recognition Science derives physics in native units where $c = 1$, so cosmological observables require an external calibration seam to SI units. The module supplies the Planck time anchor $t_P = 5.391247$ times $10^{-44}$ s drawn from CODATA 2018, together with conversion formulas that preserve the theoretical ratios while attaching the human-defined meter and second.

proof idea

One-line wrapper that multiplies the input by the constant planck_time_SI.

why it matters in Recognition Science

This definition supplies the time half of the SI reporting seam, allowing native RS quantities such as the age of the universe in Planck times to be rendered in seconds for direct comparison with Hubble or supernova data. It completes the bridge described in the module documentation and supports the Hubble-parameter conversion formula given in the same file.

scope and limits

formal statement (Lean)

  84def planck_to_seconds (t_planck : ℝ) : ℝ := t_planck * planck_time_SI

proof body

Definition body.

  85
  86/-- Convert a Hubble parameter from 1/t_P to km/s/Mpc.
  87    H₀ [1/t_P] × (t_P [s] / Mpc [m]) × (1 km) = H₀ [km/s/Mpc]. -/

depends on (3)

Lean names referenced from this declaration's body.