falsifierDatasetRegisterCert_inhabited
plain-language theorem explainer
The master falsifier-register certificate type is inhabited: every quantum-gravity §7 register row carries a named dataset, a positive sensitivity scale, and a positive RS target scale. Verification and Track-6 sensitivity proofs cite this to discharge the Nonempty obligation on that certificate. The argument is a one-line term packing the concrete certificate instance already built in-module.
Claim. The type of master certificates for the quantum-gravity falsifier register is nonempty: there exists a record asserting that every §7 register row has a named observational dataset, a strictly positive numerical sensitivity scale, and a strictly positive Recognition Science 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. Status is structural: zero sorry and no new RS-internal axioms. A row is attached when it has a named observational channel, a numerical sensitivity scale, an RS target scale or band, and an honest flag on whether current data already reach that target.
The master certificate structure packages, for each attachment (BMV, Hawking temperature, leading-log entropy, Page curve, echoes, and the remaining register rows), two positivity facts: the dataset sensitivity scale is positive, and the RS target scale is positive. The module purpose is falsifiability accounting, not empirical confirmation; records do not claim any dataset has confirmed RS.
Anchor examples in the module header include Planck 2018 $\Omega_\Lambda$, constant-$w$ dark-energy fits, Cassini Shapiro delay, EHT M87* shadow geometry, GRAVITY S2 precession, PTA Hellings-Downs backgrounds, and GWTC-3 GR tests.
proof idea
One-line term proof. Nonemptiness of the master certificate type is witnessed by the already-constructed value that fills every structure field with the corresponding in-module positivity lemmas (positive sensitivity and positive target scale for each named attachment). No further tactic reasoning is required.
why it matters
This inhabitation is the structural closure step for §7 falsifier-register dataset accounting. Downstream, the one-statement theorem flattens the certificate into an explicit conjunction of positive sensitivities and positive RS target scales across all register rows. Track-6 falsifier sensitivity then consumes the same certificate family as part of the Fork F endpoint bundle (discriminator sector counts, rival-row coverage, and per-rival distinguishability).
In the broader Recognition verification stack, the result makes explicit which experiment tests which QG prediction and at what reported precision, without claiming confirmation. It sits in the verification domain rather than the T0-T8 forcing chain, but it is how RS keeps the quantum-gravity falsifier list observationally grounded and machine-checkable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.