planck_time_pos
plain-language theorem explainer
The lemma establishes that the Planck time constructed as the square root of ħ G over c^5 remains strictly positive when the inputs are the CODATA reference values. Researchers deriving fundamental scales or checking consistency in Recognition Science constant derivations would cite it to anchor positivity of the Planck scale. The proof is a direct term-mode application of sqrt_pos after unfolding the definition and chaining mul_pos, div_pos, and pow_pos on the three upstream positivity lemmas.
Claim. $0 < sqrt( ħ_codata ⋅ G_codata / c_codata^5 )$
background
The Constants.Derivation module derives physical constants from Recognition Science primitives, taking CODATA reference values c = 299792458 m/s, ħ = 1.054571817×10^{-34} J·s, and G = 6.67430×10^{-11} m³/(kg·s²) as starting points. The definition planck_time := sqrt (hbar_codata * G_codata / c_codata ^ 5) assembles the Planck time directly from these three quantities. Upstream lemmas c_codata_pos, hbar_codata_pos, and G_codata_pos each reduce to norm_num after unfolding their respective codata constants, supplying the positivity facts required here.
proof idea
Unfold planck_time to expose the square-root expression, then apply sqrt_pos.mpr. The argument of the square root is shown positive by div_pos whose numerator is mul_pos of hbar_codata_pos and G_codata_pos and whose denominator is pow_pos c_codata_pos 5.
why it matters
The result supplies a basic positivity guarantee for the Planck time inside the constant-derivation pipeline of Recognition Science. It sits downstream of the three codata positivity lemmas and the planck_time definition; although no direct used_by edges are recorded, the lemma closes the positivity interface needed before any further manipulation of the Planck scale in the framework's constant derivations or phi-ladder constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.