strongDetection
plain-language theorem explainer
Defines the strong-detection predicate for a pulsar-timing falsifier certificate: the stacked residual must exceed the predicted ~10 ns RS signature by more than three standard deviations. Anyone checking the LedgerHum experimental protocol cites this gate. The body is a one-line inequality on the certificate fields.
Claim. Given a pulsar-timing falsifier certificate $f$ (stacked residual, observation count $\ge 10^7$, and positive uncertainty), strong detection holds when $$f.\mathrm{measured\_residual} > \mathrm{pulsarResidualSignature} + 3\, f.\mathrm{uncertainty}.$$
background
Module Verification.LedgerHum packages experimental checks of the discrete eight-tick ledger cadence forced by the Recognition chain (T7: period $2^3$; T8: $D=3$). The fundamental time quantum is one tick $\tau_0=1$ in RS-native units; one octave is eight ticks.
A PulsarTimingFalsifier certificate records a stacked residual after enough observations, together with its uncertainty. The sibling prediction pulsarResidualSignature is the nanosecond-scale offset expected from metric aliasing of the eight-tick structure. The structure doc states the falsifier: absence of a $\sim 10,\mathrm{ns}$ residual under proper stacking would defeat the discrete eight-tick claim.
Strong detection is the $3\sigma$ threshold on that residual, separating a clear positive from noise-consistent data.
proof idea
Pure definitional predicate: no tactics or lemmas. It expands to the strict inequality comparing the certificate's measured residual against the predicted signature plus three times the stated uncertainty. Downstream consumers unfold or rewrite with this definition.
why it matters
Feeds the complete confirmation predicate ledgerHumConfirmed, which requires strong detection on the pulsar arm, LIGO consistency with metric aliasing, and cross-correlation above $0.1$. That bundle is the experimental gate for the "ledger hum" signature of the eight-tick octave.
In the forcing chain, T7 fixes the eight-tick period and T8 forces $D=3$; the pulsar residual is a concrete, falsifiable imprint of that discrete cadence on timing data. The definition does not itself prove the physics; it names the statistical bar that would count as a positive hit in the protocol.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.