pith. sign in
module module high

IndisputableMonolith.StandardModel.CKMMatrix

show as:
view Lean formalization →

The CKMMatrix module supplies definitions for the Cabibbo angle θ_c and Wolfenstein-parameterized CKM matrix elements in the Recognition Science setting. Flavor physicists embedding the Standard Model into the unified forcing chain would cite these when computing quark mixing amplitudes. The module contains only definitions and imports the base Constants module with no proofs or theorems.

claimThe Cabibbo angle is the mixing parameter θ_c between the first and second quark generations. The CKM matrix is parameterized by Wolfenstein variables λ, A, ρ, η, yielding the elements V_ud, V_us, V_ub, V_cd, V_cs, V_cb.

background

The module operates in the StandardModel domain of Recognition Science, which derives all physics from the single functional equation and the forcing chain T0-T8. It imports the Constants module whose sole content is the RS time quantum τ₀ = 1 tick. Definitions here introduce θ_c for 1-2 generation mixing and the full set of CKM elements expressed through the Wolfenstein parameterization.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

These definitions feed the Standard Model constructions that connect to the mass formula yardstick * φ^(rung - 8 + gap(Z)) and the Berry creation threshold. The module supplies the CKM structure needed for any RS treatment of weak interactions and CP violation, consistent with the eight-tick octave and D = 3.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (40)