rho_bar_interval
plain-language theorem explainer
The Wolfenstein parameter ρ-bar is shown to lie in the open interval (0.10, 0.20) under the Recognition Science assignment of its value. Flavor physicists comparing RS-derived CKM elements to experimental data on the unitarity triangle would reference this bound. The proof reduces to unfolding the constant definition 0.14 and discharging the inequalities by numerical normalization.
Claim. $0.10 < {bar rho} < 0.20$, where ${bar rho}$ denotes the real part of the Wolfenstein parameter in the RS model of the CKM matrix.
background
The StandardModel.CKMMatrix module derives the CKM matrix from φ-quantized mixing angles linked to the eight-tick phase structure. The Wolfenstein parametrization is used with parameters λ, A, ρ-bar, η-bar; ρ-bar is fixed at the constant 0.14, stated to arise from the unitarity triangle with CP phase δ = π/2 giving real part approximately 0.13. The module imports Mathlib and Constants. Upstream results include the inflaton potential V(φ_inf) = J(1 + φ_inf) from J-cost, binary-cube vertex count V(D) = 2^D, and the vantage type abbreviation, though the direct dependency is the local constant definition of the Wolfenstein parameter.
proof idea
The proof is a term-mode one-liner. It unfolds the definition of the Wolfenstein parameter to expose the literal 0.14, then applies constructor to split the conjunction and norm_num to verify both inequalities hold.
why it matters
This theorem supplies a concrete numerical anchor for the real part of the Wolfenstein parameter in the RS-derived CKM matrix, consistent with the predicted interval from the unitarity triangle. It supports the module claim that CKM elements emerge from φ-angles. No downstream uses are recorded, indicating it serves as a terminal fact for experimental comparison. It touches the T7 eight-tick octave through the phase structure but does not invoke it explicitly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.