Pith. sign in
module module moderate

IndisputableMonolith.Verification.DarkEnergyWPlanckLikelihood

show as:
view Lean formalization →

Verification layer attaching Planck+BAO+SNe constant-w constraints to the RS dark-energy equation-of-state track. It records the observational central value and uncertainty for w0, the RS baseline and z~1 deviation target, and proves the residual sits inside one sigma while the observational sigma exceeds the RS target scale. Cosmologists citing Track 4.C falsifiers use the exported certificate. The argument is mostly positive constants, residual arithmetic, and a dataset-attachment status record.

claimFix Planck+BAO+SNe constants $w_0^{\mathrm{obs}}$ and $\sigma_{w_0}>0$, an RS baseline $w_0^{\mathrm{RS}}$, and a positive RS $w_1$ deviation target at $z\sim 1$. The residual $|w_0^{\mathrm{RS}}-w_0^{\mathrm{obs}}|$ is at most one observational sigma, $\sigma_{w_0}$ exceeds the RS $z\sim 1$ target, and a named dataset-attachment status plus certificate package these comparisons for the falsifier likelihood register.

background

Track 4.C of the quantum-gravity master plan concerns the structural form of the dark-energy equation of state $w(z)$. The upstream cosmology module ships that structural theorem with zero sorry and no RS-internal axiom: it fixes how $w$ is allowed to depend on redshift inside Recognition Science, rather than fitting a free CPL pair $(w_0,w_a)$.

This verification module sits one layer above that structure. It imports the falsifier-register dataset attachments and pins concrete Planck+BAO+SNe numbers: a constant-$w$ central value, its one-sigma width, an RS baseline for $w_0$, and an RS target size for the $w_1$-scale deviation near $z\sim 1$. The residual is the absolute gap between the RS baseline and the Planck central value.

The local goal is not to re-derive $w(z)$, but to certify that the RS numbers land inside the published constant-$w$ band and that the observational uncertainty is large enough relative to the RS $z\sim 1$ target for the falsifier row to be scored.

proof idea

Definition block first: named reals for the Planck central value and sigma, the RS $w_0$ baseline, the RS $w_1$ deviation target, and the residual $|\mathrm{RS}-\mathrm{obs}|$.

Two positivity lemmas discharge $\sigma_{w_0}>0$ and the RS target $>0$ by norm_num-style evaluation of the concrete decimals.

The main comparison lemmas then show residual $\le$ one observational sigma and observational sigma greater than the RS $z\sim 1$ target, again by direct arithmetic on the fixed constants.

A dataset-attachment status record and a small certificate structure (DarkEnergyWPlanckLikelihoodCert / its value) bundle those facts for the parent likelihood register. No deep tactic proof: closed numerical inequalities plus packaging.

why it matters in Recognition Science

The parent consumer is the Falsifier Likelihood Register, which "aggregates Sessions 107--115: the dataset-specific likelihood/status layer over the quantum-gravity master plan §7 falsifier register." Without this module, the dark-energy $w$ row has structural form upstream but no Planck+BAO+SNe likelihood attachment.

Upstream, Cosmology.DarkEnergyWofZStructural closes Track 4.C as a structural theorem. This file converts that structure into a scored falsifier line: residual inside one sigma, sigma above the RS $z\sim 1$ target, and an explicit attachment status.

In the broader RS program this is empirical hygiene, not a new forcing step (T5--T8 stay untouched). It keeps the dark-energy claim auditably tied to a named external dataset so a referee can reject the row if Planck-central or sigma inputs move outside the certified inequalities.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (14)