falsifierDatasetRegisterCert
plain-language theorem explainer
A master certificate packing every quantum-gravity §7 falsifier-register row with a named dataset, a strictly positive observational sensitivity, and a strictly positive RS target scale. Verification auditors and anyone checking falsifiability accounting cite it. The body is a pure structure instance that wires in the per-row positivity lemmas.
Claim. There exists a certificate asserting that each §7 falsifier-register attachment (BMV, Hawking temperature, leading-log entropy, Page curve, post-merger echoes, $\Omega_\Lambda$, dark-energy $w$, QNM, PTA, and strong-field/precision-GR) has both a positive numerical sensitivity scale and a positive RS target scale.
background
The module attaches concrete named datasets and numerical sensitivity records to every row of the quantum-gravity master plan §7 falsifier register. Attachment means a named observational channel, a numerical sensitivity scale, an RS target scale or band, and an honest flag on whether current data already reach the RS target. The purpose is falsifiability accounting, not empirical confirmation.
DatasetAttachment records sector, dataset string, sensitivity, and target. HasPositiveSensitivity and HasPositiveTargetScale are the Prop wrappers that the sensitivity and target numbers are strictly positive. Anchor examples in the module include Planck 2018 $\Omega_\Lambda$, Cassini PPN-$\gamma$, EHT M87* shadow, NANOGrav 15-year Hellings-Downs, and GWTC-3 echo/graviton-mass bounds.
Upstream, each row has a pair of one-line norm_num theorems (e.g. BMV, echo, dark-energy $w$) proving positivity after unfolding the attachment.
proof idea
Pure structure construction: inhabit FalsifierDatasetRegisterCert by assigning, fieldwise, the already-proved positivity theorems bmv_sensitivity_pos, bmv_target_pos, hawking_sensitivity_pos, hawking_target_pos, and the analogous pairs for leading-log entropy, Page curve, echoes, $\Omega_\Lambda$, dark-energy $w$, QNM, PTA, and strong-field. No new arithmetic; each field is a direct reference to a sibling norm_num lemma.
why it matters
Closes the dataset-attachment layer of the §7 falsifier register: every row is certified to carry a positive sensitivity and a positive RS target. Downstream, falsifierDatasetRegisterCert_inhabited is the one-line Nonempty wrapper, giving the single-statement form that all falsifier-register rows have positive dataset sensitivities and positive RS target scales. In the broader Recognition verification stack this is structural bookkeeping for quantum-gravity predictions (Hawking temperature, Page curve, echoes, QNMs, PTA stochastic background, strong-field PPN/$\gamma$), not a derivation of those predictions from the forcing chain. It makes the falsifiability ledger machine-checkable with zero sorry and zero new RS axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.