falsifier_dataset_register_one_statement
plain-language theorem explainer
Every quantum-gravity falsifier-register dataset row has strictly positive numerical sensitivity, and the master register certificate is inhabited. Verification auditors cite this as the single-statement closure that all §7 attachments carry positive sensitivity and (via the certificate) positive RS target scales. The proof is a pure term packing the ten individual positivity lemmas plus the inhabited certificate.
Claim. Each of the ten falsifier-register dataset attachments (BMV phase-rate, Hawking temperature, leading-log entropy, Page curve, black-hole echoes, $\Omega_\Lambda$, dark-energy $w$, quasinormal modes, pulsar timing arrays, and strong-field/precision-GR) satisfies $0 < \mathrm{sensitivity}$, and there exists a master certificate asserting positive sensitivity and positive RS target scale on every row.
background
This module attaches named observational channels and numerical sensitivity records to every row of the quantum-gravity master plan §7 falsifier register. Attachment means a named dataset, 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; records do not claim that any dataset has confirmed RS.
HasPositiveSensitivity is the predicate $0 < D.\mathrm{sensitivity}$ on a dataset attachment. The master certificate structure packages, for each §7 row, both that positivity and the companion positive RS target-scale requirement. Anchor channels include Planck 2018 $\Omega_\Lambda$, Planck+BAO+SNe $w_0$, Cassini Shapiro delay, EHT/GRAVITY strong-field tests, NANOGrav/EPTA PTA spectra, and GWTC-3 ringdown/echo searches.
Upstream lemmas discharge positivity for each concrete attachment by unfolding the attachment record and evaluating the numerical sensitivity (for example BMV band width, echo amplitude ratio $0.10$, dark-energy $w$ uncertainty $0.03$).
proof idea
Pure term-mode proof: the goal is an eleven-fold conjunction (ten sensitivity positivities plus nonemptiness of the master certificate). The term is the tuple of the ten individual positivity theorems (bmv_sensitivity_pos, hawking_sensitivity_pos, leadingLog_sensitivity_pos, pageCurve_sensitivity_pos, echo_sensitivity_pos, omegaLambda_sensitivity_pos, darkEnergyW_sensitivity_pos, qnm_sensitivity_pos, pta_sensitivity_pos, strongField_sensitivity_pos) together with falsifierDatasetRegisterCert_inhabited. Each positivity lemma is itself a short unfold + norm_num check on the corresponding attachment's sensitivity field.
why it matters
Closes the dataset-attachment layer of the quantum-gravity falsifier register as a single citable statement: every §7 row is wired to a named channel with positive sensitivity, and the master certificate (which also carries positive RS target scales) is inhabited. Module status is structural theorem, zero sorry, zero new RS-internal axioms, closure dated 2026-05-22.
No downstream consumers are recorded yet; the declaration is the top-level one-statement export of the module. It supports falsifiability accounting for RS predictions across tabletop BMV phase rates, black-hole thermodynamics and echoes, cosmological dark-energy parameters, QNMs, PTA stochastic backgrounds, and strong-field/precision-GR tests. It does not touch the forcing chain (T0–T8) or the Recognition Composition Law directly; it sits in the verification layer that makes those predictions experimentally accountable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.