tau_8_pos
plain-language theorem explainer
The eight-tick sampling period τ₈ is strictly positive. Anyone building the RS metric-aliasing record (Nyquist frequency, noise floor) cites this as the positivity witness for the sampling period field. The proof unfolds τ₈ = 8·τ₀ and multiplies the elementary facts 8 > 0 and τ₀ > 0.
Claim. The eight-tick period $\tau_8 := 8\,\tau_0$ satisfies $\tau_8 > 0$, where $\tau_0 > 0$ is the fundamental ledger tick.
background
In the LedgerHum verification module, spacetime is treated as updating on a discrete ledger clock. The base period is the fundamental tick $\tau_0 > 0$. Recognition Science forces an eight-tick octave (forcing-chain T7: period $2^3$), so the natural sampling window for metric updates is $\tau_8 = 8,\tau_0$.
Metric aliasing is the claim that continuous signals sampled every $\tau_8$ fold above the Nyquist frequency $1/(2\tau_8)$ and leave a staircase noise floor at the tick scale. The structure MetricAliasing therefore demands a proof that the sampling period is positive before it can form $1/(2\tau_8)$ and attach a nonnegative noise amplitude (taken as $\varphi^{-1}$).
Sibling facts already record $\tau_0 > 0$ (tau_0_pos). This lemma lifts that fact through the factor of eight.
proof idea
Term-mode after a single unfold. Expand $\tau_8$ to $8\cdot\tau_0$, then apply real multiplication-positivity (mul_pos) to the pair $(8 > 0)$ (closed by norm_num) and $\tau_0 > 0$ (the sibling tau_0_pos). No further lemmas.
why it matters
Feeds the sole downstream consumer rsMetricAliasing, which packages the RS eight-tick aliasing prediction: sampling period $\tau_8$, Nyquist frequency $1/(2\tau_8)$, noise amplitude $\varphi^{-1}$, with period_pos := tau_8_pos. Without this positivity witness the structure will not typecheck.
In the broader framework this is the verification-side footprint of forcing-chain T7 (eight-tick octave) and the discrete-update picture behind the ledger hum. The module text ties the same floor to LIGO and pulsar-timing arrays approaching the $\tau_0$ noise scale; later siblings (pulsarResidualSignature, PulsarTimingFalsifier) turn that into an observational test. The lemma itself is tiny, but it is the gate that lets the aliasing record be assembled.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.