lambda_PDG_in_window

The module CKMExact derives the Wolfenstein $A$ parameter from $Q_3$ geometry: Gray-code flip counts $(4,2,2)$, generation torsion gaps $\Delta\tau_{12}=11$ and $\Delta\tau_{23}=6$, and a face-flux correction $3/2$, yielding $A_{\mathrm{corrected}}=9/11\approx 0.818$ (PDG $0.826\pm 0.013$). The same $Q_3$ chirality ties into the 44-factor that appears in $\alpha^{-1}$ and $\eta_B$.

Wolfenstein $\lambda$ is the Cabibbo-scale mixing angle, experimentally $|V_{us}|\approx 0.2265$. In this file it is frozen as the real constant $0.2265$. A nearby claim records that the RS value (rooted in $\varphi^{-3}$) differs from this PDG figure by less than 6%, with a small geometric correction still pending.

The present theorem only certifies that the frozen PDG number sits in a fixed open interval used as a comparison window.

One-line tactic proof. Unfold the definition $\lambda_{\mathrm{PDG}}=0.2265$, split the conjunction, and run norm_num on each strict inequality $0.222<0.2265$ and $0.2265<0.232$. No lemmas beyond the definition are required.

Places the experimental Wolfenstein $\lambda$ inside a concrete numeric band so later RS-vs-PDG comparisons (the $<6%$ gap to the $\varphi^{-3}$ origin, and the $A=9/11$ match) can quote a proved window rather than a raw float. It sits in the CKMExact stack that already closes $A_{\mathrm{corrected}}=9/11$ from $Q_3$ face flux and generation torsion, linking CKM to the same 44-structure that governs $\alpha^{-1}$ and $\eta_B$. No downstream theorems depend on it yet; it is a local sanity gate for the PDG side of the comparison. It does not itself derive $\lambda$ from the forcing chain (T5–T8) or from RCL.