planck_time_pos
The lemma establishes positivity of the Planck time defined from the codata constants for hbar, G, and c. Researchers deriving physical scales in Recognition Science cite it to confirm that the standard expression remains strictly positive. The proof is a direct one-line wrapper that unfolds the definition and applies the real-number positivity lemmas for square root, multiplication, division, and powering.
claim$0 < t_P$ where $t_P = t_P = sqrt( hbar_codata * G_codata / c_codata^5 )$ and the codata values are the reference constants for the reduced Planck constant, gravitational constant, and speed of light.
background
The module derives physical constants from Recognition Science primitives and lists CODATA reference values for c, ℏ, and G. The definition planck_time is the standard expression sqrt(hbar_codata * G_codata / c_codata^5). Upstream lemmas c_codata_pos, hbar_codata_pos, and G_codata_pos each reduce to norm_num after unfolding their respective codata definitions, establishing that all three inputs are positive reals.
proof idea
The proof unfolds planck_time and applies sqrt_pos.mpr to the positivity of the argument. That argument positivity follows from mul_pos applied to hbar_codata_pos and G_codata_pos, then div_pos with the result of pow_pos applied to c_codata_pos.
why it matters in Recognition Science
The lemma secures positivity of the derived Planck time inside the constants module, supporting the framework's construction of physical scales from the forcing chain (T0-T8) and the phi-ladder. It aligns with the Recognition Composition Law and the requirement that quantities such as the Berry creation threshold remain positive. No downstream theorems are listed, but the result underpins any later manipulation of Planck-scale expressions.
scope and limits
- Does not derive the Planck time formula from Recognition Science axioms.
- Does not supply a numerical value or experimental comparison.
- Does not treat units or dimensional consistency.
- Does not establish uniqueness or other algebraic properties.
formal statement (Lean)
158lemma planck_time_pos : 0 < planck_time := by
proof body
Term-mode proof.
159 unfold planck_time
160 exact sqrt_pos.mpr (div_pos (mul_pos hbar_codata_pos G_codata_pos) (pow_pos c_codata_pos 5))
161