planck_time
The definition supplies the Planck time t_P via the square root of (hbar times G over c to the fifth) using the listed CODATA reference numbers. Researchers linking the Recognition Science time unit tau0 to the Planck scale cite this when closing the relation tau0 = t_P / sqrt(pi). The body is a direct abbreviation of the classical Planck-time formula with no internal lemmas.
claim$ t_P := sqrt( hbar_codata * G_codata / c_codata^5 ) $ where the inputs are the CODATA anchors c = 299792458, hbar = 1.054571817e-34, G = 6.67430e-11.
background
The Constants.Derivation module anchors derivations to CODATA reference values for c, hbar and G before relating them to Recognition Science primitives. The three upstream definitions supply exactly those numerical constants: c_codata = 299792458, hbar_codata = 1.054571817e-34 and G_codata = 6.67430e-11. These serve as fixed inputs to the standard Planck-time expression that later connects to the RS-native time tau0.
proof idea
The declaration is a direct definition that assembles the Planck time from the three codata constants via the square-root expression; no lemmas are invoked inside the body.
why it matters in Recognition Science
This definition supplies the input to the positivity lemma planck_time_pos and to the theorem tau0_planck_relation, which states tau0 = planck_time / sqrt(Real.pi). It therefore bridges the CODATA Planck scale to the Recognition Science fundamental time tau0 that appears in the forcing chain and the eight-tick octave.
scope and limits
- Does not derive the numerical values of hbar, G or c from Recognition Science primitives.
- Does not establish positivity of the result.
- Does not relate the expression to the phi-ladder or J-cost.
- Does not claim exact equality with any RS-native quantity beyond the downstream tau0 relation.
formal statement (Lean)
151def planck_time : ℝ := sqrt (hbar_codata * G_codata / c_codata ^ 5)