MeasurementProtocol
plain-language theorem explainer
Bundles the four experimental knobs for a ledger-hum search: pulsar count, minimum pulse arrivals, LIGO frequency window, and cross-correlation lag window around the eight-tick period. Verification authors and observers cite it when fixing a concrete search recipe. Pure structure definition; no proof obligations.
Claim. A ledger-hum measurement protocol is a 4-tuple $(N_{\mathrm{pulsars}}, N_{\mathrm{pulses}}^{\min}, B_{\mathrm{LIGO}}, L_{\mathrm{corr}})$ with $N_{\mathrm{pulsars}}\in\mathbb{N}$ the number of millisecond pulsars, $N_{\mathrm{pulses}}^{\min}\in\mathbb{N}$ the minimum arrivals per pulsar, $B_{\mathrm{LIGO}}=(f_{\mathrm{lo}},f_{\mathrm{hi}})$ a LIGO band in Hz, and $L_{\mathrm{corr}}=(t_{\mathrm{lo}},t_{\mathrm{hi}})$ a cross-correlation lag range in seconds.
background
The Verification.LedgerHum module packages falsifiable timing and spectral signatures of the Recognition eight-tick octave. The fundamental tick $\tau_0$ and the eight-tick period $\tau_8=8\tau_0$ set the predicted residual scale and the lag at which independent pulsar arrays should correlate.
The doc-comment spells the intended campaign in three channels: (1) stack millisecond-pulsar timing residuals phase-aligned to $\tau_8$, with many arrivals and known noise subtracted; (2) inspect the LIGO noise floor in a stated band for a slope break off the quantum-noise model; (3) cross-correlate independent arrays at the $\tau_8$ lag with common-mode controls.
This structure only holds the numeric parameters of that campaign. It is unrelated to the Foundation.MeasurementMechanism structure of the same name (pre/interact/read coupling of ledger configurations).
proof idea
No proof. The declaration is a four-field structure: natural-number counts for pulsars and minimum pulses, plus two real pairs for the LIGO band and the correlation lag window. Downstream defs supply a concrete instance and a validity predicate on those fields.
why it matters
Gives a single typed carrier for the experimental recipe that would detect or refute the ledger hum tied to the T7 eight-tick octave. Downstream, minimalProtocol fills the fields with the doc-comment thresholds ($\ge 5$ pulsars, $\ge 10^8$ pulses, 10–1000 Hz, lag window containing $\tau_8$), protocolValid checks those inequalities, and ledgerHumStatus reports the package as ready.
Together with sibling residual and stacking models (nanosecond-scale pulsar signature, $\sqrt{N}$ stacked residual), it turns the abstract eight-tick claim into an observer-facing protocol rather than a pure existence statement. It does not itself close a forcing-chain step; it is the verification interface those predictions feed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.