planck_time_SI_pos
plain-language theorem explainer
The theorem establishes that the Planck time in SI seconds is strictly positive. Cosmologists bridging Recognition Science native units to observational data would cite this when certifying calibration anchors for length and time scales. The proof is a one-line wrapper that unfolds the constant definition and applies numerical normalization to confirm the inequality.
Claim. $0 < t_P$ where $t_P = 5.391247 × 10^{-44}$ denotes the Planck time in seconds (CODATA 2018 value).
background
The SIConversion module supplies the bridge between Recognition Science native units (c = ℓ₀ = τ₀ = 1) and SI units for cosmological observables. The Planck time is defined as t_P = ℓ_P / c with numerical value 5.391247 × 10^{-44} s taken directly from CODATA 2018; this is an external calibration anchor, not an RS prediction. The module documentation states that the theoretical content resides in the ratios (R_obs / ℓ_P, t_age / t_P) rather than the absolute SI values themselves.
proof idea
The proof is a one-line wrapper that unfolds the definition of planck_time_SI and invokes norm_num to verify positivity of the constant 5.391247e-44.
why it matters
This supplies the positivity witness planck_time_positive inside the SI calibration certificate theorem. It completes the seam allowing RS predictions in native units to be compared with observations in meters and seconds. The module documentation emphasizes that SI values are external facts while ratios carry the RS content, supporting the Planck scale bridge (ℓ_P = 1/√π in native units).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.