cabibboAngle
plain-language theorem explainer
This definition supplies the numerical value 0.227 for sin of the Cabibbo angle in the Recognition Science treatment of quark flavor mixing. Particle physicists constructing CKM elements or Wolfenstein parameters would cite it to anchor numerical checks against experimental mixing data. The definition is a direct numerical assignment drawn from the upstream phi-structure result.
Claim. The Cabibbo angle satisfies $sin θ_c = 0.227$.
background
The module derives CKM matrix elements from φ-quantized mixing angles tied to the eight-tick phase structure. The Cabibbo angle parametrizes mixing between first and second quark generations. Upstream, the three-generations module states that the Cabibbo angle θ_C ≈ 13° emerges from φ-structure and defines it via arcsin(1/φ²), which evaluates numerically to approximately 0.227.
proof idea
One-line definition that directly assigns the constant 0.227. No lemmas or tactics are invoked.
why it matters
The definition feeds the cabibbo_value theorem that verifies the interval (0.22, 0.23) and the wolfenstein_lambda parameter. It fills the SM-012 target of deriving the CKM matrix from RS, linking to the T7 eight-tick octave and the paper proposition on CKM matrix from golden ratio geometry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.