ligoConsistentWithAliasing
plain-language theorem explainer
A LIGO noise-floor datum is consistent with Recognition Science metric aliasing when its measured spectral slope above Nyquist lies within absolute distance 1 of the RS predicted slope. Experimentalists and auditors of the ledger-hum falsifier cite this predicate as the LIGO arm of the three-way test. It is a pure definitional inequality, not a derived theorem.
Claim. Given a LIGO noise-floor record (reference PSD, reference frequency, and measured spectral slope above Nyquist), the record is consistent with metric aliasing when $\lvert s_{\mathrm{meas}} - s_{\mathrm{RS}}\rvert < 1$, where $s_{\mathrm{RS}}$ is the Recognition Science predicted spectral slope (steep falloff above the Nyquist frequency set by the eight-tick cadence).
background
The LedgerHum module packages experimental falsifiers for the discrete-spacetime ("ledger hum") prediction: an eight-tick fundamental period $\tau_8$ that should imprint on precision timing and on gravitational-wave noise. One arm is LIGO. The structure LIGONoiseFloor records a reference power spectral density, a reference frequency, and the measured spectral slope above Nyquist.
Recognition Science attributes part of the approached LIGO noise floor to metric aliasing of the discrete ledger into the continuous strain channel. The predicted aliasing spectrum is flat below Nyquist and falls steeply above it; the constant rsSpectralSlope is that predicted high-frequency exponent. The present definition simply asks whether a measured slope sits within unit distance of that prediction.
The surrounding bundle also includes a pulsar-timing residual test (stacked residual at nanosecond scale) and a cross-correlation cut at lag $\tau_8$, forming a three-component confirmation/falsification interface.
proof idea
Definitional, not proved. The body is the single inequality comparing the absolute difference of the measured spectral slope and the RS constant rsSpectralSlope against the fixed tolerance 1. No lemmas are invoked; the predicate is the Prop that downstream confirmation and falsification defs unfold.
why it matters
This is the LIGO spectral arm of the ledger-hum falsifier bundle for discrete spacetime. Downstream, ledgerHumConfirmed requires it conjunctively with a strong pulsar detection and cross-correlation above 0.1; ledgerHumFalsified fires if the negation holds (or if either of the other arms fails). The module doc frames the full bundle as: (1) pulsar timing ~10 ns stacked residual, (2) LIGO spectral $f^{-4}$ above Nyquist, (3) timing-array correlation at $\tau_8$.
In the broader RS chain the eight-tick octave is landmark T7 (period $2^3$), forced after J-uniqueness and $\varphi$. A confirmed steep high-frequency LIGO slope matching the RS constant would be direct laboratory support for that discrete cadence; a clear mismatch falsifies the aliasing contribution claim. The definition itself does not compute the slope constant; it only packages the acceptance window used by the verification layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.