eta_bar_interval
plain-language theorem explainer
The Wolfenstein CP-violation parameter η-bar satisfies the strict bounds 0.28 < η-bar < 0.40 in the Recognition Science treatment of the CKM matrix. Quark flavor physicists comparing RS-derived mixing to the Jarlskog invariant would cite this interval. The proof is a one-line wrapper that unfolds the constant definition and verifies the numerical inequalities with norm_num.
Claim. $0.28 < {0.35} < 0.40$, where the constant 0.35 is the Wolfenstein parameter η-bar obtained from $J_{CP} = A^2 λ^6 η-bar$ with $A = 9/11$ and $λ ∈ (0.234, 0.238)$.
background
The StandardModel.CKMMatrix module derives the 3×3 CKM matrix from φ-quantized mixing angles tied to the eight-tick phase structure. Wolfenstein parametrization expresses the matrix to O(λ³) with parameters λ, A, ρ-bar, and η-bar; the latter encodes the CP-violating phase. The upstream definition states: noncomputable def wolfenstein_eta : ℝ := 0.35, with the accompanying note that η ≈ 0.35 (CP violation phase).
proof idea
The proof is a one-line wrapper that unfolds the definition of wolfenstein_eta, splits the conjunction with constructor, and confirms both inequalities by norm_num.
why it matters
This bound supplies a concrete numerical anchor for the SM-012 target of CKM elements from φ-angles and the 8-tick octave. It directly implements the derivation J_CP = A²λ⁶η-bar with the stated values of A and λ, placing the CP phase inside the RS-predicted window. No downstream theorems are recorded, leaving the result as a self-contained numerical check within the quark-mixing development.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.