LedgerHumFalsifier
plain-language theorem explainer
Bundles the three observational channels that can falsify Recognition Science's discrete eight-tick spacetime: pulsar timing residuals, LIGO spectral noise shape, and cross-array timing correlation at the eight-tick period. Experimentalists and auditors cite it as the single certificate type for the ledger-hum protocol. It is a plain structure packing two sibling falsifier records plus a real cross-correlation coefficient.
Claim. A ledger-hum falsifier certificate is a triple $(P, L, r)$ where $P$ is a pulsar-timing falsifier (stacked residual, observation count $\ge 10^7$, uncertainty), $L$ is a LIGO noise-floor record (PSD at a reference frequency and measured spectral slope above Nyquist), and $r \in \mathbb{R}$ is the cross-correlation coefficient between timing arrays. Recognition Science predicts $r > 0$ at the eight-tick scale $\tau_8$.
background
The LedgerHum module packages empirical tests of the discrete eight-tick octave forced at T7 of the unified forcing chain. The fundamental tick $\tau_0$ and the period $\tau_8 = 8\tau_0$ set the nanosecond-scale residual expected after stacking pulsar TOAs, and the Nyquist frequency of metric sampling that should shape the LIGO noise floor.
PulsarTimingFalsifier records a stacked residual, observation count (with a $\ge 10^7$ guard), and uncertainty; absence of a $\sim 10,\mathrm{ns}$ residual under those guards would falsify the eight-tick structure. LIGONoiseFloor records PSD, reference frequency, and spectral slope; RS attributes part of the floor to metric aliasing, predicting a steep falloff above Nyquist rather than a pure quantum floor.
The third coordinate is the cross-correlation between independent timing arrays at the $\tau_8$ lag. Positive correlation is the joint signature that the residual is a shared discrete-time effect rather than uncorrelated instrumental noise.
proof idea
No proof body: this is a structure definition. It packs three fields already defined in-module (PulsarTimingFalsifier, LIGONoiseFloor, and a real cross-correlation). Downstream predicates read the fields directly; there is no algebraic reduction or tactic script at this declaration.
why it matters
This bundle is the input type for the module's pass/fail predicates. ledgerHumFalsified holds if the pulsar channel falsifies the eight-tick residual, or the LIGO record is inconsistent with aliasing, or cross-correlation is negative. ledgerHumConfirmed requires strong pulsar detection, LIGO consistency with aliasing, and cross-correlation $> 0.1$. ledgerHumStatus reports the protocol checklist built around the same objects.
In the broader framework it is the empirical face of T7 (eight-tick octave) and of metric aliasing on the discrete ledger: a concrete, multi-channel route to kill or support the claim that spacetime updates on a $2^3$ period. It does not itself compute masses, $\alpha$, or forcing steps T0–T6/T8; it only certifies whether the discrete-time hum is seen in timing and GW data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.