ledgerHumFalsified
plain-language theorem explainer
The ledger-hum prediction is falsified when any one of three observational legs fails: pulsar stacked residual below threshold, LIGO spectral slope inconsistent with the RS aliasing law, or negative cross-correlation between timing arrays at the eight-tick lag. Experimentalists and RS auditors cite this as the single Prop that packages the full discrete-spacetime kill switch. It is a pure disjunctive definition, not a proved theorem.
Claim. Given a falsifier bundle $f$ with pulsar-timing data, LIGO noise-floor data, and a cross-correlation coefficient, the ledger-hum claim is falsified if and only if the measured pulsar residual lies below the detection threshold, or the LIGO spectral slope differs from the RS aliasing slope by at least $1$, or the array cross-correlation is strictly negative.
background
Recognition Science predicts a discrete spacetime tick structure with fundamental period $\tau_8$ (the eight-tick octave from the forcing chain T7). That discreteness imprints a nanosecond-scale "ledger hum" on precision timing and gravitational-wave spectra.
The module packages three independent observational channels into one structure: (1) pulsar timing arrays, where stacking $N\sim 10^8$ residuals should yield a $\sim 10,\mathrm{ns}$ signature if the eight-tick is real; (2) LIGO noise floors, where metric aliasing above Nyquist is predicted to produce a spectral slope near the RS value; (3) cross-correlation of independent timing arrays at lag $\tau_8$, which RS requires to be positive.
Upstream, falsifiesEightTick is the residual-below-threshold test on a pulsar bundle, and ligoConsistentWithAliasing requires the absolute deviation of the measured spectral slope from the RS slope to be less than one. The present definition simply ORs those failures with a negative cross-correlation.
proof idea
There is no proof body beyond the definitional equation. The proposition is the disjunction of three already-named atomic conditions on the three fields of the falsifier bundle. Expanding the definition is definitional reduction; no lemmas are applied.
why it matters
This is the top-level kill switch for the discrete-spacetime (ledger-hum) prediction inside the Verification layer. It sits directly on the eight-tick octave (forcing-chain T7) and on the RS metric-aliasing claim for LIGO. Downstream consumers are not yet wired in this snapshot (used_by is empty), but the companion doc-comment marks the dual "complete confirmation" path: all three components must pass for the hum to stand. A referee reading the RS verification stack cites this Prop whenever asking whether the nanosecond discrete-tick signature has been observationally ruled out.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.