pulsarResidualSignature
plain-language theorem explainer
The stacked residual signature for pulsar timing arrays is fixed at 10 nanoseconds: the RS prediction for an 8-tick discreteness imprint after stacking ~10^8 pulse arrivals with path-length scatter. Timing-array and ledger-hum verification work cites this constant as the predicted residual scale. It is a bare numeric definition, not a derived theorem.
Claim. The Recognition Science stacked residual signature for pulsar timing is the real constant $10^{-8}\,\mathrm{s}$ (ten nanoseconds).
background
Module Verification.LedgerHum packages falsifiable timing predictions from the eight-tick ledger. The fundamental tick $\tau_0$ and the eight-tick period $\tau_8 = 8\tau_0$ set the discrete clock; the forcing chain (T7) identifies the octave period $2^3$ as the natural cycle.
Pulsar timing arrays record radio-pulse arrival times. If spacetime carries an 8-tick structure, stacking many arrivals should leave a residual. The doc-comment calculation starts from $\tau_8 \approx 5.84\times 10^{-14},\mathrm{s}$, multiplies by a stacking factor $\sqrt{N}$ with $N\sim 10^8$, and includes an $O(10)$ path-length factor, yielding a $\sim 10,\mathrm{ns}$ prediction.
Sibling definitions supply $\tau_0$, $\tau_8$, metric-aliasing structure, and the stacked-residual $\sqrt{N}$ model that this constant anchors.
proof idea
Pure definition: the real is set equal to $10\times 10^{-9}$ (Lean 10e-9). No lemmas, no tactics. Downstream theorems such as signature_is_nanosecond_scale unfold this constant and discharge the nanosecond-band inequalities by norm_num.
why it matters
This constant is the numerical target for the ledger-hum pulsar test of eight-tick discreteness (T7). Downstream, detectionThreshold is predicted residual minus $3\sigma$, and strongDetection is measured residual above predicted plus $3\sigma$; both compare data against this value. signature_is_nanosecond_scale certifies it lies in $(10^{-10},10^{-7}),\mathrm{s}$. ledgerHumStatus reports it in the module health string as the $\sim 10,\mathrm{ns}$ prediction.
It therefore sits at the interface between the abstract 8-tick octave and a concrete PTA falsifier: residuals well below the threshold would challenge the discrete-tick picture; a clear excess would support it. The value is an order-of-magnitude RS estimate, not a high-precision derived constant like $\alpha^{-1}$ in the RS band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.