darkEnergyWAttachment
plain-language theorem explainer
Registers the dark-energy equation-of-state channel as a falsifier-register dataset row: DESI BAO + Planck CMB + supernovae w0-wa analyses, sensitivity 0.03 in units of w, against an RS structural target ~6.38e-10 at z=1. Cosmologists and RS auditors cite it when checking whether current w(z) precision can reach the phi-suppressed prediction. The body is a pure structure literal with currentlySensitive set false.
Claim. The dark-energy equation-of-state falsifier row is the dataset attachment with sector "Dark-energy equation of state $w(z)$", dataset "DESI BAO + Planck CMB + supernovae $w_0$-$w_a$ analyses", units $w$, observational sensitivity $0.03$, RS target scale $6.376\times 10^{-10}$, and flag that current data are not yet sensitive to that target.
background
The module attaches named observational channels and numerical scales to every row of the quantum-gravity master-plan §7 falsifier register. Attachment means four things only: a named dataset, a sensitivity number, an RS target scale or band, and an honest currently-sensitive flag. Purpose is falsifiability accounting, not confirmation.
DatasetAttachment is the record type: sector, dataset, units, sensitivity, rsTargetScale, and currentlySensitive. Sensitivity and target are dimensionless unless units says otherwise. For many future rows the flag is false: the channel is named but cannot yet resolve the φ-suppressed target.
The dark-energy row uses the constant-w Planck+BAO+SNe example $w_0 = -1.03 \pm 0.03$ as the sensitivity anchor, with DESI DR1/DR2 as the modern dynamic-$w$ channel. The RS structural scale is $\varphi^{-44} z \approx 6.38\times 10^{-10}$ at $z=1$, taken from the phi-ladder (scale k := phi^k in the large-scale-structure bridge).
proof idea
Definition by structure literal. Each field of DatasetAttachment is assigned a concrete string or real: sector and dataset name the channel, units is w, sensitivity is the reported $0.03$ constant-$w$ error, rsTargetScale is the numerical $\varphi^{-44}z$ value $6.376\times 10^{-10}$, and currentlySensitive is false. No lemmas, no tactics.
why it matters
This row is the single source of the RS $w(z)$ target used throughout the Planck-likelihood verification layer. Downstream, rsW1DeviationTarget is defined as this attachment's rsTargetScale; positivity and the comparison rsW1DeviationTarget < planckW0Sigma are proved by unfolding it. The status theorem packages positive sensitivity, positive target, and currentlySensitive = false. The one-statement likelihood theorem and DarkEnergyWPlanckLikelihoodCert both require that flag and the residual-versus-sigma bound.
In the broader RS picture the target is a high negative rung on the phi-ladder, far below present cosmological equation-of-state precision. The attachment therefore documents an open experimental gap rather than a closed test: DESI and future Stage-IV surveys are the named path, but the register honestly records that they do not yet reach $\varphi^{-44}z$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.