ledgerHumConfirmed
plain-language theorem explainer
Complete experimental confirmation of the ledger-hum signature is the conjunction of three channel checks on a falsifier bundle: strong stacked pulsar detection, LIGO noise consistent with metric aliasing, and array cross-correlation above 0.1. Observers and verification authors cite it as the pass/fail gate for the discrete eight-tick residual. The body is a pure definitional conjunction, not a derived theorem.
Claim. Given a ledger-hum falsifier bundle $f$ (pulsar timing data, LIGO noise-floor data, and a real cross-correlation coefficient), confirmation holds if and only if the pulsar channel meets the strong-detection criterion, the LIGO spectrum is consistent with metric aliasing, and the cross-correlation satisfies $f_{\mathrm{cc}} > 0.1$.
background
This module packages observational tests of the Recognition Science prediction that discrete spacetime (the eight-tick octave) imprints a nanosecond-scale residual, the "ledger hum," on precision timing and gravitational-wave noise. The eight-tick phases are $k\pi/4$ for $k=0,\ldots,7$; the related timescales $\tau_0$ and $\tau_8$ set the lag at which residuals should stack and arrays should correlate.
The falsifier bundle collects three independent channels: a pulsar-timing falsifier (stacked residual at the predicted $\tau_8$, targeting $\sim 10,\mathrm{ns}$ after noise subtraction), a LIGO noise-floor record (spectral departure, including an $f^{-4}$ shape above the effective Nyquist set by the tick), and a real cross-correlation between independent timing arrays at the $\tau_8$ lag. RS predicts that correlation positive.
The surrounding protocol text specifies operational cuts: more than five millisecond pulsars, $>10^8$ arrivals each, DM and timing-noise subtraction, LIGO analysis in the $10$–$1000,\mathrm{Hz}$ band, and common-mode controls on the cross-correlation.
proof idea
Definitional, not proved. The predicate is the bare conjunction of three propositions already attached to the falsifier fields: strong detection on the pulsar component, LIGO consistency with aliasing on the noise-floor component, and the numerical inequality that the stored cross-correlation exceeds $0.1$. No lemmas are applied; discharging it means supplying a concrete bundle whose three fields satisfy those props.
why it matters
In the verification layer this is the single boolean that says the discrete-spacetime hum has been seen in full, not just in one channel. It sits on top of the eight-tick structure (T7 in the forcing chain: period $2^3$) and the metric-aliasing story that links the tick to LIGO's noise floor and to pulsar residuals at $\tau_8$.
No downstream theorems currently consume it (used_by is empty), so its role is as the named acceptance criterion for the experimental protocol rather than as a lemma in a larger proof. It closes the loop from foundation (eight-tick phase, coupled axes, pre-logical cost) to a referee-checkable observation package: if all three conjuncts hold, the ledger-hum prediction is confirmed; if any fails under the stated cuts, the prediction is challenged.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.