cabibbo_in_band
plain-language theorem explainer
The theorem establishes that 1 over phi cubed lies strictly between 0.225 and 0.240, bracketing the PDG value of the Cabibbo angle parameter lambda. Particle physicists fitting CKM matrix elements would cite this bound when comparing Recognition Science phi-ladder outputs to experimental data. The proof is a short term-mode sequence that unfolds the cabibboPhi definition, substitutes the cubic identity, invokes the supplied phi bounds, and applies reciprocal inequalities with linarith.
Claim. $0.225 < 1/phi^3 < 0.240$
background
In the CKM Lambda from Phi-Ladder module the Cabibbo angle proxy is introduced as the definition cabibboPhi := 1/phi^3. The module situates this inside the Wolfenstein parameterisation of the CKM matrix, noting that the leading Recognition Science approximation 1/phi^3 ≈ 0.236 sits near the PDG lambda = 0.2247. Upstream results supply the tight bounds phi > 1.61 and phi < 1.62 together with the identity phi^3 = 2*phi + 1 that converts the cubic into an explicit real number.
proof idea
The proof unfolds cabibboPhi to 1/phi^3, rewrites via the theorem phi3_eq, then splits the conjunction. The lower bound applies lt_inv_comm0 followed by linarith on phi > 1.61; the upper bound applies inv_lt_comm0 followed by linarith on phi < 1.62.
why it matters
This theorem populates the cabibbo_band field inside the ckmlambdaCert definition that certifies Wolfenstein parameters against PDG data. It completes the phi-ladder step for the Cabibbo angle inside the Recognition Science forcing chain, consistent with the self-similar fixed point phi and the eight-tick octave. It leaves open the precise higher-order correction that would map the J-cost function exactly onto sin(theta_C).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 2 of 2)
-
RG evolution turns Wolfenstein lepton mixing small to large
"Starting with the Wolfenstein form for the leptonic mixing matrix we show that renormalization group evolution brings that to the observed large mixing at low energies... sinθ12≈λ, sinθ23≈λ², sinθ31≈λ³"
-
Quark mass hierarchies reveal dual matrix structures
"the normalized quark mass matrix in the hierarchy limit hq23 → 0 ... Mq0 = (KqL)† MqN KqL ... flat matrix MqF = 1/3 [[1,1,1],[1,1,1],[1,1,1]]"