crossCorrelationPredicted
plain-language theorem explainer
Recognition Science predicts moderate positive cross-correlation of pulsar timing residuals at the eight-tick lag τ₈, with coefficient strictly between 0.1 and 1. Timing-array analysts testing the RS metric-aliasing template against stacked residuals would cite this band. The declaration is a bare existential Prop encoding that interval; nothing is proved here.
Claim. There exists a real $r$ with $0.1 < r < 1$, the predicted moderate positive cross-correlation of residuals at the $\tau_8$ (eight-tick) timescale.
background
The module packages falsifiable pulsar-timing signatures of the Recognition ledger "hum": a coherent residual pattern locked to the discrete tick structure. Sibling constants fix the fundamental tick $\tau_0$ and the eight-tick octave lag $\tau_8 = 2^3\tau_0$, the period forced by the T7 step of the unified forcing chain.
Cross-correlation here is the overlap between an observed stacked residual series and the RS metric-aliasing template (the predicted phase pattern from ledger updates). The claim is only the sign and rough strength of that overlap at lag $\tau_8$, not a full matched-filter derivation.
Upstream, the only named dependency is a PRC-native positivity predicate on ratio orbits; it is not used in the body and does not constrain the numerical band.
proof idea
Definition only: the Prop is the existential statement $\exists r\in\mathbb{R},, 0.1<r<1$. No tactics, no lemmas, no reduction. The comment marks the intended scientific reading (moderate positive correlation).
why it matters
This is one atomic prediction inside the LedgerHum verification suite. Sibling declarations build the residual signature, the stacked observable, and the composite PulsarTimingFalsifier; any failed component is meant to falsify the theory. The lag is the eight-tick octave (T7), so a null or negative correlation at $\tau_8$ would strike the discrete-time backbone rather than a free nuisance parameter.
No downstream Lean consumers are wired yet (used_by is empty). The def therefore stands as an interface hypothesis for observational tests, not as a proved theorem inside the forcing chain (T0–T8) or the mass/α ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.