planck_time
plain-language theorem explainer
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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.