PulsarTimingFalsifier
plain-language theorem explainer
A certificate packaging a stacked pulsar-timing residual, observation count, and uncertainty, with guards N ≥ 10^7 and σ > 0. Experimentalists and RS auditors cite it when testing for a ~10 ns residual tied to discrete eight-tick structure. Structure definition only: it fixes fields consumed by the eight-tick falsification predicates, with no proof body.
Claim. A pulsar-timing falsifier is a triple $(r, N, \sigma)$ consisting of a measured stacked residual $r \in \mathbb{R}$, an observation count $N \in \mathbb{N}$ satisfying $N \geq 10^{7}$, and a measurement uncertainty $\sigma \in \mathbb{R}$ with $\sigma > 0$.
background
Recognition Science forces an eight-tick octave (T7): a fundamental tick $\tau_0$ and period $\tau_8 = 8\tau_0$. Discrete sampling of spacetime is predicted to leave a metric-aliasing residual at nanosecond scale in stacked pulsar arrival times. The LedgerHum module treats that residual as a falsifiable "ledger hum."
Upstream measurement seams supply the reporting vocabulary (real value, optional sigma/interval uncertainty, protocol metadata). Sibling defs in this module fix $\tau_0 \sim 7.3\times 10^{-15}$ s, a predicted pulsar residual signature of order 10 ns, and a $\sqrt{N}$ stacking model.
This structure is the input record for those checks: what residual was measured, how many pulses were stacked, and at what uncertainty, with hard bounds that block underpowered claims.
proof idea
No proof. The declaration is a structure with three data fields (measured residual, observation count, uncertainty) and two propositional fields enforcing $N \geq 10^7$ and $\sigma > 0$. Downstream definitions read those fields directly; nothing is proved here.
why it matters
Supplies the pulsar channel of the ledger-hum falsification bundle. Downstream, detectionThreshold forms predicted signature minus $3\sigma$; falsifiesEightTick holds when the measured residual falls below that threshold; strongDetection holds when it exceeds signature plus $3\sigma$. LedgerHumFalsifier packages this record with LIGO spectral and cross-array correlation channels. The framework landmark under test is T7 (eight-tick octave): absence of a phase-coherent ~10 ns residual after adequate stacking and noise guards would falsify discrete 8-tick structure. ledgerHumStatus surfaces the certificate on the verification dashboard.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.