minimalProtocol_valid
plain-language theorem explainer
The minimal pulsar-timing protocol (5 pulsars, 10^8 pulses, LIGO band 10–1000 Hz, lag window 10^{-14}–10^{-12} s) satisfies the formal validity predicate. Anyone citing the LedgerHum verification stack uses this as the baseline admissible experiment. The proof is pure arithmetic: unfold the structures and discharge six numeric inequalities with norm_num.
Claim. The minimal measurement protocol with $n_{\mathrm{pulsars}}=5$, $\mathrm{min\_pulses}=10^8$, LIGO band $(10,1000)$, and correlation lag range $(10^{-14},10^{-12})$ satisfies the validity conditions: at least 3 pulsars, at least $10^7$ pulses, a positive nonempty LIGO frequency interval, and a lag window that strictly contains the eight-tick period $\tau_8=8\tau_0$.
background
LedgerHum packages falsifiable pulsar-timing signatures of the recognition ledger. The atomic time unit is $\tau_0\approx 7.30\times 10^{-15},\mathrm{s}$ (the fundamental tick forced by the eight-tick octave T7); the full recognition cycle is $\tau_8=8\tau_0\approx 5.84\times 10^{-14},\mathrm{s}$.
A MeasurementProtocol records how many pulsars, how many pulses, which LIGO frequency band, and which correlation-lag window an experiment uses. Validity (protocolValid) demands: $\ge 3$ pulsars, $\ge 10^7$ pulses, a positive nonempty LIGO interval, and a lag range that strictly brackets $\tau_8$ so the eight-tick residual is inside the searchable window.
The minimal protocol is the concrete default: 5 pulsars, $10^8$ pulses, band $(10,1000)$, lags $(10^{-14},10^{-12})$. This theorem simply certifies that default against the predicate.
proof idea
Term-mode proof by unfolding. Expand protocolValid, minimalProtocol, tau_8, and tau_0, then build the six-conjunct conjunction with successive constructors. Each conjunct is a concrete numeric comparison (5 ≥ 3, 10^8 ≥ 10^7, 10 > 0, 10 < 1000, 10^{-14} < 8·7.30e-15, 8·7.30e-15 < 10^{-12}); all are closed by norm_num. No lemmas beyond definitional unfolding are required.
why it matters
Gives a machine-checked, ready-to-cite baseline experiment for the LedgerHum verification layer. Downstream residual and falsifier constructions (stacked residual, pulsar residual signature, PulsarTimingFalsifier) presuppose a valid protocol; this theorem supplies the canonical one. It ties the measurement window directly to the eight-tick period $\tau_8$ forced by T7 in the UnifiedForcingChain, so any claimed nanosecond-scale ledger hum is searched inside a lag band that mathematically contains the RS fundamental cycle. With zero used_by edges yet, it is presently a leaf certificate rather than an intermediate lemma.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.