tau0_pos
plain-language theorem explainer
The lemma establishes that the fundamental tick duration τ₀ is strictly positive in RS-native units. Researchers deriving constants such as ħ or assembling canonical unit systems cite this result to guarantee positivity throughout the construction. The proof is a one-line term-mode wrapper that reduces the claim to the positivity of 1 after simplification on the definition of τ₀.
Claim. $0 < τ_0$, where $τ_0$ is the fundamental tick duration in RS-native units.
background
In the Recognition Science framework, τ₀ is the base time unit defined as the duration of one tick. The Compat.Constants module re-exports it via def tau0 : ℝ := IndisputableMonolith.Constants.tick, while the parent Constants module supplies the noncomputable definition @[simp] noncomputable def tau0 : ℝ := tick. The module doc describes the file as containing project-wide constants and minimal structural lemmas.
proof idea
The proof is a one-line term-mode wrapper. It applies simpa [tau0] to unfold the definition and reduces the inequality directly to the known fact 0 < (1 : ℝ).
why it matters
This positivity lemma is invoked by twenty downstream declarations, including hbar_pos (which obtains 0 < ħ via mul_pos cLagLock_pos tau0_pos and states ħ = φ^{-5}) and canonicalUnits (which packages τ₀, ℓ₀ and φ into an RSUnitSystem). It supplies the required positivity hypothesis for the C-004 derivation of Planck's constant and for the ILG growth ODE and CPMInstance constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.