tau0_tP_ratio
plain-language theorem explainer
The definition supplies the ratio of the fundamental RS tick duration τ₀ to Planck time t_P as a real number. Researchers deriving Planck-scale quantities from Recognition Science principles cite this when linking discrete time units to quantum gravity. The implementation is a direct quotient that supports later numerical analysis relating the ratio to a power of the golden ratio φ.
Claim. Let τ₀ denote the fundamental tick duration and t_P the Planck time. The ratio is defined by τ₀ / t_P.
background
In the Recognition Science framework the Planck scale emerges where quantum mechanics meets gravity, with t_P = √(ℏG/c⁵) expressed in RS-native units via the fundamental tick τ₀. The module targets derivation of Planck length, mass and time from RS principles, noting l_P = c × τ₀ × φ^(-n) for suitable n. Upstream, τ₀ is supplied as the duration of one tick, appearing in Constants as tick and in Derivation as sqrt(hbar_codata * G_codata / (Real.pi * c_codata ^ 3)) / c_codata.
proof idea
The definition is a one-line wrapper that divides the imported tau0 by the planckTime definition from the same module.
why it matters
This definition supports the connection between the fundamental tick and Planck time in the QG-009 and QG-010 targets. It enables the analysis that the ratio approximates φ^34, tying into the eight-tick octave (T7) and phi-forcing chain (T5-T8). No direct downstream uses are listed, but it fills the gap in relating discrete RS time to quantum gravity scales.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.