planck_time_inner_nonneg
plain-language theorem explainer
The lemma establishes nonnegativity of ħ G / c⁵ using the CODATA reference values. Researchers working on constants derivation in Recognition Science cite it to confirm the radicand of the Planck time is nonnegative and well-defined over the reals. The proof is a one-line term that chains mul_pos, pow_pos, and div_pos on the three positivity lemmas for the constants.
Claim. $0 ≤ ħ_{codata} · G_{codata} / c_{codata}^5$
background
The module derives physical constants from Recognition Science primitives by importing CODATA reference values: c = 299792458 m/s, ħ = 1.054571817×10^{-34} J·s, and G = 6.67430×10^{-11} m³/(kg·s²). The relevant definitions are c_codata, hbar_codata, and G_codata, each a direct real-number constant, together with their positivity lemmas c_codata_pos, hbar_codata_pos, and G_codata_pos obtained by unfolding and applying norm_num.
proof idea
The term proof applies le_of_lt to the result of div_pos (mul_pos hbar_codata_pos G_codata_pos) (pow_pos c_codata_pos 5). It therefore reduces the claim to the elementary fact that the product of two positive reals divided by a positive fifth power remains positive.
why it matters
The result is a prerequisite for the sibling definition tau0 that sets τ₀ = t_P / √π. It supplies the basic positivity check needed before taking the square root in the Planck-time expression inside the constants derivation. The lemma closes a small but necessary gap in the chain that grounds ħ, G, and c inside the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.