omega_lambda_measurement
plain-language theorem explainer
Preregistered Planck-era dark-energy density parameter: central value 0.6847 with 1σ width 0.0073, labeled Omega_L_Planck. Cosmologists and RS verifiers cite it as the fixed observational anchor for Ω_Λ checks. The body is a pure structure literal of the preregistered Measurement record; no proof obligations.
Claim. The preregistered observational measurement of the dark-energy density parameter $\Omega_\Lambda$ is the triple $(\mathrm{name},\,c,\,\sigma)=(\text{Omega\_L\_Planck},\,0.6847,\,0.0073)$, i.e. central value $0.6847$ with one-sigma uncertainty $0.0073$.
background
This file is a pure data module under Verification.Preregistered.Hubble. Its module header states it holds representative Hubble-tension values and the Planck $\Omega_\Lambda$ figure, to be updated when new releases arrive.
The ambient Measurement type (from Preregistered.Core) is the triple of a string label, a real central value, and a real one-sigma width. It is the payload type used by the preregistered within-sigma predicates; it is not the richer RS-native measurement structure (value/window/protocol) nor the quantum nonlocality measurement (axis/outcome).
Sibling constants in the same namespace fix early- and late-universe $H_0$ anchors. Downstream tests compare an RS-side $\Omega_\Lambda$ prediction against this fixed observational record.
proof idea
Definition only: a structure literal that fills the three fields of the preregistered Measurement record (name string, central real, sigma real). No tactics, no lemmas, no computation.
why it matters
Supplies the observational side of the $\Omega_\Lambda$ consistency check. The immediate consumer is omega_lambda_passes_1sigma, which asserts that the RS prediction for $\Omega_\Lambda$ lies inside one sigma of this Planck anchor via the preregistered within_sigma predicate.
In the broader Verification layer this is how Recognition Science freezes external data before comparing it to forced constants and cosmology outputs (phi-ladder masses, BIT kernel families, etc.). Updating the numbers here is the intended path when Planck or successor releases revise $\Omega_\Lambda$; the test theorems then re-run against the new literal.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.