omegaLambda_sensitivity_pos
plain-language theorem explainer
The Planck 2018 Ω_Λ dataset attachment has strictly positive numerical sensitivity (0.0056). Auditors of the RS quantum-gravity falsifier register cite this to show the cosmological-constant row is observationally non-vacuous. The proof unfolds the attachment record and closes 0 < 0.0056 by norm_num.
Claim. The cosmological-constant dataset attachment (Planck 2018 TT,TE,EE+lowE+lensing, sensitivity $0.0056$ in $\Omega_\Lambda$ units) satisfies the positive-sensitivity requirement $0 < \mathrm{sensitivity}$.
background
This module attaches named observational channels and numerical sensitivity records to every row of the quantum-gravity master-plan §7 falsifier register. An attachment is a record with sector, dataset name, units, a reported sensitivity scale, an RS target scale or band, and a flag for whether current data already reach that target. The purpose is falsifiability accounting, not empirical confirmation of RS.
Positive sensitivity is the predicate $0 < D.\mathrm{sensitivity}$ on such a record. The Ω_Λ row uses the Planck 2018 base-ΛCDM figure $\Omega_\Lambda = 0.6889 \pm 0.0056$, with sensitivity set to the reported $1\sigma$ error $0.0056$ and RS band $(0.683, 0.686)$ used only for a two-sigma consistency check.
proof idea
One-line term-mode proof. Unfold the positive-sensitivity predicate and the Ω_Λ attachment definition, exposing the concrete inequality $0 < 0.0056$. Discharge it by norm_num. No lemmas beyond the two local definitions are required.
why it matters
Feeds the bundled certificate falsifierDatasetRegisterCert and the one-statement theorem that every falsifier-register row has positive sensitivity and positive RS target scale. Also used by omegaLambda_dataset_attachment_active in the Planck-likelihood module, which packages positive sensitivity, positive target scale, and the currently-sensitive flag for this row.
In the Recognition framework this is bookkeeping for the cosmological-constant prediction against Planck 2018, not a derivation of $\Omega_\Lambda$ from the forcing chain. It makes the register row machine-checkably non-vacuous so downstream verification can treat the Ω_Λ channel as an active falsifier rather than an empty placeholder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.