detectionThreshold
plain-language theorem explainer
Defines the 3σ lower detection threshold for the predicted ~10 ns stacked pulsar residual: signature minus three times the measurement uncertainty. Anyone checking the eight-tick falsifier certificate cites this bound. The body is a one-line arithmetic definition, not a proof.
Claim. Given a pulsar-timing falsifier certificate $f$ (measured stacked residual, observation count $\ge 10^7$, and uncertainty $\sigma_f > 0$), the detection threshold is $10\,\mathrm{ns} - 3\sigma_f$.
background
LedgerHum packages empirical checks of the discrete eight-tick time structure forced by the Recognition forcing chain (T7: period $2^3$). The fundamental RS time quantum is one tick $\tau_0 = 1$ in native units; one octave is eight ticks.
If spacetime carries that discrete cadence, pulsar timing arrays should leave a stacked residual signature of order $10,\mathrm{ns}$ after many pulse arrivals. The constant pulsarResidualSignature fixes that predicted scale at $10^{-8},\mathrm{s}$.
A PulsarTimingFalsifier is the certificate bundle: measured residual after stacking, observation count (required $\ge 10^7$), and positive uncertainty. The threshold defined here is the classical 3σ floor under that predicted signature.
proof idea
Pure definition: subtract three times the certificate uncertainty from the fixed nanosecond-scale residual signature. No lemmas, no tactics; noncomputable only because the ambient real arithmetic is.
why it matters
Supplies the cutoff used by falsifiesEightTick: measured residual strictly below this threshold is declared to falsify the discrete eight-tick structure. That is the operational half of the module's falsifier certificate (absence of a ~10 ns stacked residual under stacking guards and sufficient counts).
In the broader framework this is an empirical gate on T7 (eight-tick octave). It does not derive the residual from the Recognition Composition Law or the mass ladder; it only codifies the statistical decision boundary so the verification layer can state a crisp yes/no against PTA data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.