tau_8
plain-language theorem explainer
The eight-tick recognition period is defined as eight times the fundamental tick: τ₈ = 8 τ₀ ≈ 5.84×10⁻¹⁴ s. Anyone working the LedgerHum verification stack (metric aliasing, pulsar residual stacking, protocol validity) cites this constant. The body is a one-line scalar definition from τ₀.
Claim. Define the eight-tick period by $\tau_8 := 8\,\tau_0$, where $\tau_0\approx 7.30\times 10^{-15}\,\mathrm{s}$ is the fundamental recognition tick. Numerically $\tau_8\approx 5.84\times 10^{-14}\,\mathrm{s}$.
background
LedgerHum packages the discrete-time constants used to falsify or support Recognition Science against pulsar-timing and LIGO-band data. The atomic time unit is the fundamental tick $\tau_0\approx 7.30\times 10^{-15},\mathrm{s}$, stated as derived (not fitted) from the eight-tick forcing step.
In the forcing chain, T7 fixes an eight-tick octave: spacetime updates close after period $2^3=8$ ticks. One full recognition cycle therefore lasts $\tau_8=8\tau_0$. Downstream objects treat $\tau_8$ as the sampling period of the RS metric-aliasing model and as the lag scale that a valid measurement protocol must bracket.
The module imports Constants and Patterns; positivity of the period is recorded separately so that Nyquist frequencies and residual amplitudes stay well-defined over $\mathbb{R}$.
proof idea
Pure definition: multiply the already-declared fundamental tick by eight. No lemmas, no tactics; the value is 8 * tau_0 on $\mathbb{R}$. Positivity and numerical comparisons are proved later (tau_8_pos, protocol and stacking theorems) by unfolding this abbreviation and using norm_num.
why it matters
This constant is the time-domain face of T7 (eight-tick octave) inside the verification layer. It is the sampling period of rsMetricAliasing (Nyquist frequency $1/(2\tau_8)$, noise amplitude $\varphi^{-1}$), the lag that protocolValid requires to lie strictly inside the correlation window, and the prefactor of the stacking model `stackedResidual N = \tau_8\sqrt{N}$.
Parent consumers include minimalProtocol_valid (unfolds $\tau_8$ and checks the lag inequalities by norm_num), stacked_residual_observable (shows $N\ge 10^8$ pushes the residual above $10^{-10},\mathrm{s}$), and the status string ledgerHumStatus. Without a single named eight-tick period, the pulsar residual signature and the metric-aliasing falsifier lose their RS-native clock.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.