minimalProtocol
plain-language theorem explainer
A concrete measurement protocol for the ledger-hum search: five millisecond pulsars, at least 10^8 pulses each, LIGO band 10–1000 Hz, and cross-correlation lags in (10^{-14}, 10^{-12}) s. Anyone citing the ledger-hum falsifier or the validity theorem for the minimal setup uses this record. It is a pure structure instance with fixed numeric fields, not a proved claim.
Claim. The minimal ledger-hum measurement protocol is the tuple $(n_{\mathrm{pulsars}}, n_{\mathrm{pulses}}, B_{\mathrm{LIGO}}, \Delta t_{\mathrm{corr}}) = (5,\,10^{8},\,(10,1000)\,\mathrm{Hz},\,(10^{-14},10^{-12})\,\mathrm{s})$.
background
LedgerHum packages an observational test of a predicted residual signature (phase-aligned to the eight-tick scale $\tau_8$) in millisecond-pulsar timing arrays, with a secondary LIGO-band cross-check. The local structure MeasurementProtocol fixes four experimental knobs: how many pulsars, the minimum pulse count per pulsar, the LIGO frequency window in Hz, and the lag window for residual cross-correlation in seconds.
The module doc for that structure requires multiple millisecond pulsars (more than five in the design note), stacking of residuals phase-aligned to predicted $\tau_8$, more than $10^8$ arrivals per pulsar, and subtraction of known noise (DM variations, timing noise). Sibling constants $\tau_0$ and $\tau_8$ set the time scales against which residuals are stacked.
Upstream, other modules use the word "protocol" for different objects (variational measurement stages, nested rational approximations, or named RS-native extractors). Here the meaning is strictly the pulsar/LIGO experimental parameter record above.
proof idea
Definitional construction only: instantiate the four fields of the measurement-protocol structure with the constants 5, $10^8$, the pair $(10,1000)$, and the pair $(10^{-14},10^{-12})$. No lemmas or tactics; the body is a structure value.
why it matters
Gives a single named baseline for the ledger-hum verification path. Downstream, minimalProtocol_valid proves this instance satisfies the local validity predicate (pulsar count and pulse floor meet the numeric cuts after unfolding $\tau_8$ and $\tau_0$). Sibling material (stacked residual, nanosecond-scale signature, PulsarTimingFalsifier) treats this as the default experimental envelope for claiming a detection or a null.
In the broader RS chain the eight-tick octave (T7) and the $\phi$-native time yardsticks motivate $\tau_8$; this definition does not re-derive those scales, it only freezes the observing parameters used to hunt the predicted residual. Without a fixed minimal protocol, validity and falsifier statements would float over arbitrary instrument choices.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.