cabibbo_value
plain-language theorem explainer
The Cabibbo angle satisfies 0.22 < θ_C < 0.23 with θ_C set to 0.227 in the RS CKM construction. Quark flavor physicists would cite the bound when validating φ-quantized mixing angles against data. The proof unfolds the constant definition of the angle and applies numerical normalization to confirm the interval.
Claim. $0.22 < θ_C < 0.23$ where $θ_C$ is the Cabibbo mixing angle between the first and second quark generations.
background
The StandardModel.CKMMatrix module derives the CKM matrix from φ-quantized mixing angles linked to the eight-tick phase structure. The Cabibbo angle θ_C parametrizes mixing between the first and second generations, with the local definition fixing its value at 0.227. Upstream in Physics.ThreeGenerations the same angle is introduced as arcsin(1/φ²), which yields the numerical value used here and aligns with the module's target of obtaining CKM elements from golden ratio geometry.
proof idea
The term proof first unfolds the definition of cabibboAngle to the constant 0.227. It then splits the conjunction with constructor and applies norm_num to verify both sides of the interval 0.22 < 0.227 < 0.23.
why it matters
The theorem supplies the numerical anchor for the Cabibbo angle inside the φ-angle derivation of the CKM matrix, directly supporting the SM-012 goal stated in the module documentation. It confirms consistency between the local constant and the upstream arcsin(1/φ²) definition from ThreeGenerations. The result therefore contributes to the broader claim that CKM parameters emerge from the Recognition Science eight-tick structure without additional free parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.