planckTime
plain-language theorem explainer
The definition supplies the Planck time t_P = √(ℏ G / c⁵) using RS-native constants. Researchers linking the coherence time τ₀ to quantum gravity scales cite it when computing the ratio τ₀ / t_P. It is realized as a direct one-line transcription of the conventional formula that substitutes the imported ħ and G.
Claim. The Planck time is defined by $t_P = √(ℏ G / c^5)$, where ħ is the reduced Planck constant in RS units and G is the gravitational constant obtained from the recognition length scale.
background
The Quantum.PlanckScale module targets derivation of Planck length, mass, and time from RS principles, with explicit links to τ₀ and φ. The Planck time marks the scale at which quantum mechanics and gravity intersect, listed numerically as ≈ 5.4 × 10^{-44} s, and is positioned as the natural unit for quantum gravity.
proof idea
This is a one-line definition that directly transcribes the standard Planck time formula. It imports ħ (defined as φ^{-5} in Constants) and G (defined as λ_rec² c³ / (π ħ) in Constants), then assembles the square root of their product divided by c^5.
why it matters
The definition feeds the downstream ratio τ₀ / t_P, whose doc-comment records the value ≈ 2.39 × 10^{16} and asks which power of φ it matches. It advances the module's QG-009 and QG-010 targets of expressing the Planck scale through φ. The result sits inside the forcing chain that fixes D = 3 and the eight-tick octave, though the explicit φ exponent for t_P remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.