rsSpectralSlope
plain-language theorem explainer
Recognition Science predicts a spectral slope of -4 (power law f^{-4}) for the ledger-hum metric-aliasing signature above Nyquist. Anyone comparing a LIGO noise-floor fit to the RS aliasing hypothesis cites this constant. The declaration is a bare real assignment, not a derived identity.
Claim. The RS-predicted spectral slope for the ledger-hum metric-aliasing signature is $-4$, i.e. a power-law falloff $f^{-4}$ above the Nyquist frequency.
background
Module Verification.LedgerHum packages falsifiable signatures of a discrete recognition ledger against continuous spacetime detectors. One channel is metric aliasing: high-frequency ledger ticks fold into the LIGO band and leave a characteristic noise-floor shape.
The spectral slope is the exponent in a power-law model of that folded floor. Sibling definitions fix timing scales (tau_0, tau_8), the aliasing residual, and a nanosecond-scale pulsar residual; this constant is the RS target for the LIGO spectral fit alone.
No upstream lemma computes the exponent here. The value is the framework prediction that downstream consistency predicates compare against measured floors.
proof idea
Pure definition: the real constant is set to $-4$, with an inline comment that the intended power law is $f^{-4}$. No tactics, no lemmas, no reduction.
why it matters
Feeds ligoConsistentWithAliasing, which holds when a reported LIGO noise-floor spectral slope lies within absolute distance 1 of this constant. That predicate sits in the combined Ledger Hum falsifier bundle: if real LIGO spectral fits stay far from $-4$, the aliasing channel of the ledger-hum claim is rejected.
In the broader RS picture the steep falloff is the continuous-band imprint of the discrete eight-tick octave (T7) after aliasing. The declaration itself does not re-derive that chain; it freezes the numerical target the verification layer needs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.