tau0_pos
plain-language theorem explainer
The lemma establishes that the fundamental time unit τ₀ is strictly positive in RS-native units. Derivations of the reduced Planck constant and canonical unit systems cite this result to anchor positivity throughout the derived constants. The proof reduces the claim directly to the definition of τ₀ as one tick via a single simplification step.
Claim. $0 < τ_0$, where $τ_0$ denotes the duration of one recognition tick in RS-native units.
background
In the Constants module the fundamental RS time quantum is introduced as τ₀ = 1 tick, serving as the atomic unit of time once the forcing chain has fixed c = 1. The definition unfolds τ₀ to the tick constant whose positivity is inherited from the ordered field of real numbers. Upstream results supply the reciprocal automorphism on the J-cost and the minimal physical assumptions on bridge anchors that reuse this positivity for length and action scales.
proof idea
The tactic proof applies simp to the definitions of τ₀ and tick, reducing 0 < τ₀ to the trivial inequality 0 < 1 in the reals.
why it matters
This lemma supplies the time-base positivity required by the canonical unit system and by the identity ħ = φ^{-5} obtained via multiplication with the coherence-energy term. It feeds the construction of RSUnitSystem and the positivity lemmas for ell0 and hbar, closing the T7 eight-tick octave step in the forcing chain. Downstream it is invoked in the ILG growth ODE and in nucleosynthesis tier calculations that rely on positive RS-native units.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.