FalsifierDatasetRegisterCert
plain-language theorem explainer
Master certificate that every §7 quantum-gravity falsifier-register row carries a named dataset with strictly positive numerical sensitivity and a strictly positive RS target scale. Verification and Track-6 auditors cite it when closing the dataset-attachment ledger. It is a pure structure of positivity propositions; a separate inhabitant fills the fields from the concrete attachment records.
Claim. A certificate asserting that each of the ten §7 falsifier-register 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 gravity) has strictly positive recorded sensitivity and strictly positive RS target scale.
background
This 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.
A DatasetAttachment records sector, dataset name, units, sensitivity, and rsTargetScale. The predicates used here are elementary: positive sensitivity means $0 < D.\mathrm{sensitivity}$; positive target scale means $0 < D.\mathrm{rsTargetScale}$. Upstream rows include BMV/MAQRO phase-rate (target band $\sim[4.77,5.04]\times10^{-7}$ rad/s), Hawking temperature (10% fractional threshold on future analog/PBH channels), echo amplitude (RS target $1/\varphi\approx0.618$ vs GWTC-3 null searches), and dark-energy $w$ (Planck+BAO+SNe sensitivity $\sim0.03$ vs RS scale $\varphi^{-44}z\sim6\times10^{-10}$ at $z=1$).
proof idea
No proof body: this is a structure definition. Each field is a proposition that a named attachment satisfies positive sensitivity or positive RS target scale. Inhabitance is deferred to the concrete certificate value and the nonempty theorem, which discharge the fields by positivity lemmas on the floating-point constants stored in each attachment record.
why it matters
Closes the structural half of the §7 falsifier-register ledger: every row is not merely named but certified to carry positive sensitivity and positive RS target. Downstream, the inhabited instance and the one-statement conjunction package the same facts for export; Track 6's falsifier-sensitivity certificate consumes this bundle as the dataset-attachment handoff among discriminator sectors, rival-row coverage, and guarded GWTC-3 ringdown processing. Within Recognition Science this is verification infrastructure rather than a forcing-chain step (T0–T8): it makes the quantum-gravity predictions auditable against named experiments (Planck $\Omega_\Lambda$, DESI $w$, NANOGrav/EPTA PTA, LIGO echoes/QNM, EHT/GRAVITY strong field, MAQRO-class BMV) without claiming confirmation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.