lambda_correction_target
plain-language theorem explainer
A real number exists in the open band (0.222, 0.228) within 0.003 of the PDG 2024 Wolfenstein λ value 0.2265. Anyone citing the Recognition Science face-flux correction for Cabibbo λ uses this as the numerical target interval. The proof is a one-line existential witness with decimal arithmetic.
Claim. There exists a real number $c$ such that $0.222 < c < 0.228$ and $|c - 0.2265| < 0.003$, where $0.2265$ is the PDG 2024 Wolfenstein $\lambda$ parameter ($|V_{us}|$).
background
The module derives Wolfenstein CKM parameters from $Q_3$ geometry: Gray-code flip counts $(4,2,2)$ on the three axes, generation torsion gaps $\Delta\tau_{12}=11$ and $\Delta\tau_{23}=6$, and face-flux ratios. Its headline result is $A_{\mathrm{corrected}}=9/11\approx 0.818$, within $0.6\sigma$ of PDG.
Wolfenstein $\lambda$ is the Cabibbo angle parameter, fixed by PDG 2024 at $0.2265$. The structural RS estimate sits near $(0.234,0.238)$; the PDG band is roughly $(0.222,0.232)$. The gap is closed by a hypothesized face-flux correction $({\mathrm{faceFlux}}{23}/{\mathrm{faceFlux}}{12})^{1/8}=(2/3)^{1/8}\approx 0.95$, which multiplies the structural value down into the experimental window and ties the power $1/8$ to eight-tick periodicity.
Upstream, lambda_PDG is the bare constant $0.2265$. This theorem only pins a concrete numerical target band around that constant; it does not yet prove the rpow correction itself.
proof idea
Term-mode existential: the witness $c=0.225$ is supplied, then three norm_num goals discharge $0.222<0.225$, $0.225<0.228$, and (after unfolding the PDG constant) $|0.225-0.2265|<0.003$. No lemmas beyond decimal arithmetic.
why it matters
The declaration records the precise numerical landing zone that the face-flux $\lambda$ correction is supposed to hit: roughly $(0.222,0.228)$ and within $0.003$ of PDG $\lambda$. The module doc ties the same $Q_3$ chirality (Gray code $[4,2,2]$ times generation torsion) to $\alpha^{-1}$, $\eta_B\sim\varphi^{-44}$, and $A_{\mathrm{corrected}}=9/11$; the $\lambda$ correction is the remaining Cabibbo-side piece, with the $1/8$ power linking to the eight-tick octave (T7).
No downstream consumers are wired yet. The doc-comment still flags an open formal obligation: prove $\mathrm{Real.rpow}$ bounds $(2/3)^{1/8}\in(0.948,0.955)$ so that $\lambda_{\mathrm{RS}}\times(2/3)^{1/8}$ lands inside this target. Until that rpow lemma is closed, the correction remains a precise numerical hypothesis rather than a fully chained theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.