falsifiesEightTick
plain-language theorem explainer
Defines when a pulsar-timing certificate falsifies the discrete eight-tick structure: the stacked measured residual lies strictly below the detection threshold (predicted ~10 ns signature minus three standard deviations). Verification and ledger-hum audits cite it as the pulsar arm of the composite falsifier. It is a pure definitional predicate, not a proved theorem.
Claim. Given a pulsar-timing falsifier certificate $f$ (measured residual $r$, uncertainty $\sigma$, and sufficient stack size), the eight-tick structure is falsified when $r < s - 3\sigma$, where $s$ is the predicted nanosecond-scale pulsar residual signature.
background
Recognition Science forces an eight-tick octave (forcing chain T7): the fundamental tick $\tau_0$ and period $\tau_8 = 8\tau_0$ set a discrete ledger cadence. In the LedgerHum verification module this cadence is confronted with high-precision pulsar timing via a metric-aliasing residual of order $\sim 10$ ns after stacking.
A PulsarTimingFalsifier packages the experimental side: stacked measured residual, observation count (at least $10^7$), and positive uncertainty, with guards that the stack is large enough for the $\sqrt{N}$ noise model. The companion detection threshold is the predicted signature minus three times that uncertainty, so a null or too-small residual is a one-sided rejection of the eight-tick hum.
The local setting is an explicit falsifier certificate: absence of the predicted residual, under proper stacking, is meant to kill the discrete 8-tick claim rather than leave it as an unfalsifiable story.
proof idea
Definitional, not a proof. The predicate is the strict inequality between the certificate's measured residual and the detection threshold (predicted pulsar residual signature minus $3\sigma$). No lemmas are applied; downstream code simply unfolds or cases on this Prop.
why it matters
This is the pulsar arm of the composite ledger-hum falsifier. ledgerHumFalsified ORs it with LIGO aliasing inconsistency and negative cross-correlation, so any single arm failure kills the package. Status reporting also surfaces the eight-tick and ~10 ns residual machinery this predicate guards.
Framework-wise it operationalizes T7 (eight-tick octave): the discrete period is not only derived in the forcing chain but given a concrete astronomical kill switch. It does not touch mass ladders, $\alpha$, or $D=3$; it only closes the observational loop on the tick structure itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.