tau0_pos
plain-language theorem explainer
tau0_pos asserts that the fundamental tick duration tau0 is strictly positive in the Recognition Science constants derivation. Researchers deriving hbar positivity or constructing canonical RS units cite it to anchor time-scale signs. The proof is a term-mode chain that unfolds tau0 and applies div_pos together with sqrt_pos.mpr to the codata-derived expression.
Claim. $0 < tau0$, where $tau0$ is the fundamental tick duration defined via the quotient of the positive square root of $(hbar_{codata} G_{codata}) / (pi c_{codata}^3)$ by $c_{codata}$.
background
The module derives physical constants from Recognition Science primitives using CODATA reference values c = 299792458 m/s, ℏ = 1.054571817×10^{-34} J·s, and G = 6.67430×10^{-11} m³/(kg·s²). tau0 is introduced as the duration of one tick, with an explicit derived expression in Derivation that references the codata constants. Upstream results supply the definition tau0 := tick together with the positivity lemmas c_codata_pos, G_codata_pos, and hbar_codata_pos, each obtained by norm_num on their explicit positive values.
proof idea
The term proof unfolds tau0, then applies div_pos to split into numerator and denominator positivity. The numerator is handled by sqrt_pos.mpr applied to div_pos of mul_pos hbar_codata_pos G_codata_pos over mul_pos Real.pi_pos (pow_pos c_codata_pos 3). The denominator positivity is discharged directly by c_codata_pos.
why it matters
tau0_pos supplies the positivity fact required by hbar_pos (which states ℏ = phi^{-5} in RS-native units) and by the construction of canonicalUnits. It completes the C-004 Planck-constant derivation step and feeds the ILG growth ODE and CPMInstance. Within the framework it secures the positive time scale needed for the eight-tick octave and the forcing chain from T0 to T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.