darkEnergyW_sensitivity_pos
plain-language theorem explainer
The dark-energy equation-of-state dataset attachment carries a strictly positive numerical sensitivity (0.03 in units of w). Cosmologists and RS auditors cite it when certifying that the w(z) falsifier row is observationally instrumented. The proof unfolds the positivity predicate and the attachment record, then discharges 0 < 0.03 by norm_num.
Claim. The dark-energy equation-of-state dataset attachment (DESI BAO + Planck CMB + supernovae $w_0$–$w_a$ analyses, sensitivity $0.03$ in units of $w$) satisfies $0 < \mathrm{sensitivity}$.
background
The 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, and a flag for whether current data already reach the RS target. The purpose is falsifiability accounting, not empirical confirmation.
HasPositiveSensitivity is the predicate $0 < D.\mathrm{sensitivity}$ on such a record. The dark-energy $w(z)$ attachment uses Planck+BAO+SNe constant-$w$ precision $w_0 = -1.03 \pm 0.03$ (and DESI dynamic-$w$ channels) as the sensitivity scale, against an RS structural target of order $\varphi^{-44}z \approx 6.38\times 10^{-10}$ at $z=1$, far below present equation-of-state precision.
proof idea
One-line tactic proof: unfold the positivity predicate and the concrete attachment definition, exposing the numeric goal $0 < 0.03$, then close it with norm_num. No lemmas beyond definitional unfolding are required.
why it matters
This lemma is the sensitivity half of the dark-energy $w(z)$ attachment status theorem, which packages positive sensitivity, positive RS target scale, and the explicit flag currentlySensitive = false. It is also a field of the aggregate falsifier-dataset-register certificate and appears in the one-statement conjunction that every register row has positive sensitivity and positive target scale.
In the broader RS verification layer this is bookkeeping for the cosmology sector of the falsifier register: it records that a real observational channel exists at the $3%$ level in $w$, while the RS target remains many orders of magnitude smaller. It does not touch the forcing chain (T0–T8), RCL, or the mass ladder; it only certifies that the $w(z)$ row is instrumented for future comparison.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.