tau_0
plain-language theorem explainer
The atomic recognition tick is fixed at τ₀ = 7.30×10⁻¹⁵ s, the discrete time step of the ledger. Anyone building eight-tick periods, Hamiltonian generators, ILG kernels, or pulsar residual protocols cites this constant. It is a bare numeric definition in RS-native units, not a fitted parameter.
Claim. The fundamental recognition tick is the positive real $\tau_0 := 7.30 \times 10^{-15}$ seconds. Spacetime updates of the recognition ledger proceed in discrete steps of this duration; the eight-tick period is $\tau_8 = 8\tau_0$.
background
In Recognition Science the ledger does not evolve continuously. The forcing chain isolates an eight-tick octave (period $2^3$): each complete recognition cycle is eight atomic steps. The atomic step is $\tau_0$, called the fundamental tick.
This module (Verification.LedgerHum) packages that tick for observational checks (metric aliasing, pulsar residual signatures, stacked residuals). Downstream thermodynamics takes the IR cutoff as $f_0 = 1/(8\tau_0)$. The numeric value is stated as derived in the RS chain, not fitted to data.
Sibling constants include $\tau_8 = 8\tau_0$ and positivity lemmas used by protocol-validity proofs.
proof idea
Definition only: a noncomputable real assigned the literal $7.30\times 10^{-15}$. No lemmas, no tactics. Downstream proofs that need positivity or the eight-tick multiple unfold this constant and discharge inequalities by norm_num.
why it matters
Every discrete-time construction in the monolith needs a concrete tick. Hamiltonian emergence uses it to tie the finite-dimensional generator and the first-order step to a physical duration; the ILG kernel folds $\tau_0$ into the perturbation scale; recognition thermodynamics defines the fundamental frequency $f_0 = 1/(8\tau_0)$ from it.
Inside this module it anchors ledgerHumStatus, minimalProtocol_valid, and the stacked residual / pulsar-timing falsifier stack (nanosecond-scale residual predictions). It is the SI face of the eight-tick octave landmark: without a fixed $\tau_0$, protocol validity and residual observability statements have no units.
The value is presented as derived from the forcing chain rather than free, so changing it would move the entire nanosecond residual band and the thermodynamic IR cutoff together.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.