eta_bar_interval
The declaration establishes that the Wolfenstein CP-violation parameter η-bar lies in the open interval (0.28, 0.40). Researchers deriving CKM matrix elements from Recognition Science would cite this bound to fix the phase in the Wolfenstein parametrization. The proof is a term-mode reduction that unfolds the constant definition of wolfenstein_eta to 0.35 and discharges both inequalities by numerical normalization.
claimThe Wolfenstein parameter $0.28 < 0.35 < 0.40$, where the value 0.35 is fixed by the relation $J_{CP} = A^2 λ^6 η̄$ with $A = 9/11$, $λ ∈ (0.234, 0.238)$, and $J_{CP} ≈ 3.05 × 10^{-5}$.
background
The StandardModel.CKMMatrix module derives the CKM matrix from φ-quantized mixing angles linked to the 8-tick phase structure. The Wolfenstein parametrization writes the matrix in terms of λ, A, ρ-bar, and η-bar, with η-bar encoding the CP-violating phase. The constant wolfenstein_eta is defined as the literal real number 0.35. This choice follows from the Jarlskog invariant together with the supplied values of A and λ. Upstream results supply the spacetime interval definition and structural predicates that maintain consistency across the Recognition Science ledger.
proof idea
The proof is a one-line term reduction. It unfolds wolfenstein_eta to expose the constant 0.35, splits the conjunction via constructor, and applies norm_num to verify the two numerical inequalities.
why it matters in Recognition Science
The theorem supplies the explicit numerical interval for the CP-violating phase in the CKM matrix, closing the claim stated in the module doc-comment. It supports the broader derivation of quark mixing from the Recognition Science forcing chain (T5–T7) and the eight-tick octave. No downstream theorems are recorded, leaving the result as a self-contained numerical anchor for the Standard Model embedding.
scope and limits
- Does not derive the numerical value of η-bar from the phi-ladder or J-uniqueness.
- Does not compare the interval against experimental measurements.
- Does not address higher-order terms in the Wolfenstein expansion.
- Does not extend the bound to the full unitarity triangle.
formal statement (Lean)
245theorem eta_bar_interval : (0.28 : ℝ) < wolfenstein_eta ∧ wolfenstein_eta < 0.40 := by
proof body
Term-mode proof.
246 unfold wolfenstein_eta; constructor <;> norm_num
247
248/-- ρ̄ is in the RS-predicted interval (0.10, 0.20).
249 From unitarity triangle with δ = π/2: the real part ρ̄ ≈ 0.13. -/