protocolValid
plain-language theorem explainer
A pulsar-timing measurement protocol is valid when it has at least three pulsars, at least 10^7 pulses each, a nonempty positive LIGO frequency band, and a correlation lag window that strictly contains the eight-tick period τ₈. Verifiers and experimentalists cite it to gate protocol instances before residual stacking or status reports. The body is a pure conjunction of numeric and interval inequalities; no proof is required.
Claim. A measurement protocol $p$ is valid when $n_{\mathrm{pulsars}}(p)\ge 3$, $\mathrm{min\_pulses}(p)\ge 10^7$, its LIGO band $(f_{\mathrm{lo}},f_{\mathrm{hi}})$ satisfies $0<f_{\mathrm{lo}}<f_{\mathrm{hi}}$, and its correlation lag range $(t_{\mathrm{lo}},t_{\mathrm{hi}})$ satisfies $t_{\mathrm{lo}}<\tau_8<t_{\mathrm{hi}}$, where $\tau_8=8\tau_0$ is the eight-tick period.
background
LedgerHum packages a falsifiable timing signature of the Recognition eight-tick cycle. The fundamental tick $\tau_0$ sets $\tau_8:=8\tau_0\approx 5.84\times 10^{-14},\mathrm{s}$, the period of one complete recognition update (T7 octave). Residual stacking is phase-aligned to that predicted lag.
The local MeasurementProtocol structure records four experimental knobs: pulsar count, minimum pulses per pulsar, a LIGO frequency band, and a cross-correlation lag window. (A same-named structure in MeasurementMechanism is the abstract pre/interact/read coupling story; here the type is the concrete pulsar-timing checklist.)
Protocol validity is the Prop that those knobs meet minimum numeric and interval constraints so that $\tau_8$ lies inside the lag search window and the band is a genuine open interval of positive frequencies.
proof idea
Definitional, not a proved theorem. The predicate is the four-way conjunction written in the body: pulsar count $\ge 3$, pulse floor $\ge 10^7$, LIGO band ordered with positive lower edge, and lag range strictly containing $\tau_8$. Downstream theorems discharge it by unfolding the def and the concrete protocol fields, then norm_num on each conjunct.
why it matters
Gates every concrete protocol before status reporting. The immediate consumer is minimalProtocol_valid, which shows the module's minimal protocol instance satisfies the predicate; ledgerHumStatus then folds that check into the human-readable verification string (tau definitions, metric aliasing, nanosecond residual signature, stacked $\sqrt{N}$ model).
In the framework this is the experimental face of T7: the eight-tick octave must sit inside the lag window or the residual stack cannot be phase-aligned to the predicted $\tau_8$. It does not itself compute the ~10 ns pulsar residual or the stacked-SNR model; those live in sibling defs. It only certifies that a protocol is numerically eligible to look.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.