omegaLambdaAttachment
plain-language theorem explainer
Attaches the Planck 2018 base-ΛCDM measurement of the cosmological-constant density to the §7 falsifier register. Sensitivity is 0.0056 in Ω_Λ units; the RS target scale is the band width 0.686−0.683, and the row is flagged currently sensitive. Cosmologists and RS auditors cite it for the two-sigma consistency check of the RS band Ω_Λ ∈ (0.683, 0.686) against Planck's 0.6889 ± 0.0056. The body is a plain structure literal.
Claim. The cosmological-constant falsifier row is the dataset attachment with sector "Cosmological constant $\Omega_\Lambda$", dataset "Planck 2018 TT,TE,EE+lowE+lensing", units $\Omega_\Lambda$, numerical sensitivity $0.0056$, RS target scale $0.686-0.683$, and currently-sensitive flag equal to true.
background
This module wires named observational channels onto every row of the quantum-gravity master plan §7 falsifier register. Each row is a DatasetAttachment: sector label, dataset name, units string, a numerical sensitivity, an RS target scale (or band width), and a Boolean saying whether present data already reach that target. Sensitivities and targets are dimensionless unless units says otherwise. The point is falsifiability accounting, not confirmation.
The cosmological-constant row uses the Planck 2018 TT,TE,EE+lowE+lensing base-ΛCDM record $\Omega_\Lambda = 0.6889 \pm 0.0056$. Recognition Science predicts a narrow band $\Omega_\Lambda \in (0.683, 0.686)$. The attachment stores the reported one-sigma error as sensitivity and the band width $0.003$ as the RS target scale, with the currently-sensitive flag set true because Planck already resolves that scale at roughly two sigma.
proof idea
Definitional structure literal, not a proved theorem. The six fields of the dataset-attachment record are filled by string and numeral assignments: sector and dataset name the Planck 2018 channel, units are $\Omega_\Lambda$, sensitivity is the published $0.0056$, rsTargetScale is the arithmetic difference $0.686 - 0.683$, and currentlySensitive is the Boolean true. No lemmas are invoked; downstream positivity facts discharge by unfold plus norm_num on these constants.
why it matters
This row is one of the concrete anchors of the §7 falsifier register. It feeds the positivity lemmas for sensitivity and target scale, the one-statement register theorem that every row has positive sensitivity and positive RS target, and the master register certificate that packages those facts. It is also the attachment consumed by the Planck $\Omega_\Lambda$ likelihood certificate, which asserts the residual of the RS band against Planck lies inside two sigma and that the attachment is active (positive sensitivity, positive target, currently sensitive).
In the broader RS picture the cosmological constant is a late-universe observable tied to the phi-ladder and large-scale structure scales; the attachment does not derive $\Omega_\Lambda$, it only records which public dataset tests the predicted band and at what precision. That keeps the falsifier ledger honest: the prediction is named, the experiment is named, and the sensitivity comparison is machine-checkable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.