ledgerHumStatus
plain-language theorem explainer
Status string summarizing the LedgerHum verification bundle: eight-tick timescales, pulsar residual and LIGO spectral signatures, and the formal falsification predicates. Experimentalists and auditors cite it as a checklist of what the module claims is in place. The body is pure string concatenation of fixed checklist lines; no proof obligations.
Claim. A fixed status report string asserting that the LedgerHum module defines the fundamental tick $\tau_0 \approx 7.30\times 10^{-15}\,\mathrm{s}$, the eight-tick period $\tau_8 = 8\tau_0$, metric-aliasing and stacked-residual models (nanosecond-scale pulsar timing signature with $\sqrt{N}$ stacking), LIGO $f^{-4}$ noise-floor analysis, measurement-protocol validity, and the complete falsifier bundle, together with the three falsifiable predictions and the joint-absence falsification criterion.
background
LedgerHum sits in the Verification domain and packages Recognition Science's eight-tick octave (forcing-chain T7: period $2^3$) as an observational target. The fundamental RS time quantum is the tick $\tau_0$ (Constants.tick, RS-native value 1; SI scale quoted here as $7.30\times 10^{-15},\mathrm{s}$), and $\tau_8 = 8\tau_0$ is one octave.
Sibling definitions supply the concrete observables: MetricAliasing (sampling, Nyquist, noise), pulsarResidualSignature (predicted $\sim 10,\mathrm{ns}$ residual), stackedResidual ($\sqrt{N}$ scaling), PulsarTimingFalsifier and falsifiesEightTick (formal absence conditions), plus LIGONoiseFloor spectral-slope analysis. MeasurementProtocol (Foundation) frames the three-stage pre/interact/read experimental requirements; protocolValid is the corresponding predicate.
Upstream constants also touch residual targets and phi-ladder periods used elsewhere in RS astrophysics, but this status string only inventories the LedgerHum surface.
proof idea
Not a proof. The definition is a single String built by concatenating fixed checklist lines (tick definitions, structure names, falsifiable predictions, and the joint-absence falsification sentence). An #eval at the module end prints the report. No lemmas are applied.
why it matters
Gives auditors a one-glance inventory of the LedgerHum falsification surface without opening every sibling. The scientific content it points at is the eight-tick octave (T7) made observational: a $\sim 10,\mathrm{ns}$ stacked pulsar-timing residual, an $f^{-4}$ spectral slope above Nyquist in LIGO, and positive cross-correlation at lag $\tau_8$. The closing line states the intended joint falsifier: absence of all three signatures under a valid measurement protocol.
Nothing downstream currently depends on this string (used_by is empty); it is documentation-as-code for the verification bundle, not a step in the forcing chain or a mass/alpha derivation. It does not itself prove any of the checked items exist as theorems.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.