darkEnergyW_target_pos
plain-language theorem explainer
The dark-energy equation-of-state dataset attachment carries a strictly positive Recognition Science target scale. Auditors of the quantum-gravity falsifier register cite this to confirm the w(z) row is numerically well-formed before packaging status certificates. The proof unfolds the positivity predicate and the attachment record, then discharges the inequality by numeric normalization on the stored float.
Claim. The Recognition Science target scale recorded on the dark-energy equation-of-state dataset attachment is strictly positive: $0 < 6.376\times 10^{-10}$.
background
This module attaches named observational channels and numerical sensitivity records to every row of the quantum-gravity master plan §7 falsifier register. A row is attached when it has a named dataset, a sensitivity scale, an RS target scale or band, and an honest flag for whether current data already reach that target. The purpose is falsifiability accounting, not empirical confirmation; zero sorry and no new RS axioms.
The dark-energy equation-of-state attachment points at DESI BAO + Planck CMB + supernovae $w_0$–$w_a$ analyses, with observational sensitivity $0.03$ in units of $w$. Its structural RS target scale is $\varphi^{-44}z\approx 6.38\times 10^{-10}$ at $z=1$, far below present cosmological equation-of-state precision. The positivity predicate simply requires that recorded target scale to be strictly greater than zero.
proof idea
Tactic proof in two steps: unfold the positivity predicate (which is $0 < D.\mathrm{rsTargetScale}$) together with the dark-energy attachment record, then run numeric normalization on the concrete literal $6.376\times 10^{-10}$. No lemmas beyond definitional unfolding are required.
why it matters
Supplies the target-positivity conjunct in the dark-energy dataset attachment status theorem, which packages sensitivity positivity, target positivity, and the explicit not-currently-sensitive flag for the $w(z)$ row. Also fills the dark-energy target field of the aggregate falsifier dataset register certificate that bundles every §7 row. In the Recognition verification layer this is pure structural bookkeeping: every falsifier channel must expose a well-defined positive RS comparison scale before likelihood or sensitivity claims are stated. The recorded scale itself sits many orders below Planck+BAO+SNe precision, so the row remains attached but not currently sensitive.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.