tau_0_pos
plain-language theorem explainer
The fundamental recognition tick τ₀ is strictly positive as a real number. Anyone building ledger timing, eight-tick periods, or pulsar residual signatures cites this positivity lemma. The proof unfolds the numeric definition and discharges the inequality by norm_num.
Claim. The fundamental tick satisfies $\tau_0 > 0$, where $\tau_0 \approx 7.30 \times 10^{-15}\,\mathrm{s}$ is the atomic time step of the recognition ledger.
background
In the LedgerHum verification module, spacetime is updated in discrete recognition steps. The atomic step is the fundamental tick $\tau_0$, fixed numerically at about $7.30 \times 10^{-15}$ seconds (derived from the forcing chain, not fitted). From the eight-tick octave (T7), a full recognition cycle lasts eight such ticks, so the period is $\tau_8 = 8\tau_0$.
Positivity of the base tick is the elementary real-arithmetic fact needed before any product, residual stack, or nanosecond-scale signature can be shown positive or observable. The module sits in the Verification domain and imports Constants and Patterns alongside Mathlib.
proof idea
One-line tactic proof: unfold the definition of $\tau_0$ to the concrete positive float literal, then norm_num closes $\tau_0 > 0$ in $\mathbb{R}$. No external lemmas beyond the definition are required.
why it matters
Feeds directly into tau_8_pos, which multiplies by eight and reuses this fact to prove the full eight-tick period is positive. That period is the ledger's fundamental update cycle (T7 eight-tick octave in the forcing chain). Downstream metric-aliasing and pulsar-timing falsifiers in the same module rely on a positive time base so residual signatures sit on a well-defined nanosecond scale. Without $\tau_0 > 0$, the stacked residual and PulsarTimingFalsifier chain cannot even state strict inequalities.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.