pith. sign in
module module high

IndisputableMonolith.StandardModel.CKMMatrix

show as:
view Lean formalization →

The CKMMatrix module defines the Cabibbo angle θ_c together with Wolfenstein parameters and explicit CKM matrix elements for the Standard Model in Recognition Science. Researchers modeling quark flavor mixing or CP violation in the RS framework would cite these declarations. The module consists entirely of definitions with no theorems or proofs.

claimThe Cabibbo angle $θ_c$ (first-second generation mixing), Wolfenstein parameters $λ, A, ρ, η$, and CKM matrix elements $V_{ud}, V_{us}, V_{ub}, V_{cd}, V_{cs}, V_{cb}$.

background

The module sits in the StandardModel domain and imports the Constants module, which defines the fundamental RS time quantum τ₀ = 1 tick. It introduces the Cabibbo angle as the mixing parameter between the first and second quark generations along with the Wolfenstein parameterization of the CKM matrix. These sit inside RS-native units where c = 1, ħ = φ^{-5}, and G = φ^5 / π, next to the phi-ladder mass formulas and the Recognition Composition Law.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the CKM matrix structure for the Standard Model sector in Recognition Science. It completes the flavor-mixing parameter set that connects to the J-functional equation, the eight-tick octave, and the alpha inverse band (137.030, 137.039). No downstream theorems are listed yet, but the definitions prepare the ground for quark-mass and mixing calculations on the phi-ladder.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (40)