tau0_ne_zero
plain-language theorem explainer
The lemma establishes that the fundamental tick duration tau0 derived from CODATA placeholders is nonzero. Derivations of Planck's constant and gravitational constant in Recognition Science cite it to keep all time scales well-defined and positive. The proof is a direct one-line application of the standard inequality conversion ne_of_gt to the upstream positivity result.
Claim. Let $tau_0$ be the fundamental tick duration defined by $tau_0 = sqrt(hbar_codata * G_codata / (pi * c_codata^3)) / c_codata$. Then $tau_0 neq 0$.
background
The Constants.Derivation module derives physical constants from Recognition Science primitives using CODATA reference values for c, hbar, and G. Here tau0 is introduced as the positive square-root expression built from those placeholders. Upstream results supply both the definition of tau0 as the tick duration and the lemma tau0_pos asserting its strict positivity via repeated application of sqrt_pos and div_pos to the positive codata constants.
proof idea
One-line wrapper that applies ne_of_gt directly to the upstream lemma tau0_pos.
why it matters
The result completes the basic positivity package for the derived time unit in the constants derivation, matching sibling lemmas for c, hbar, and G. It supports the overall forcing chain by guaranteeing a nonzero fundamental scale before any further constructions such as the phi-ladder or eight-tick octave are applied. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.