Pith. sign in
module module high

IndisputableMonolith.StandardModel.CKMMatrix

show as:
view Lean formalization →

The CKMMatrix module defines the Cabibbo angle and Wolfenstein-parameterized CKM matrix elements for quark mixing in the Recognition Science Standard Model. Flavor physicists or model builders extending RS to weak interactions would reference these values. The module is a pure collection of definitions that imports the Constants module for RS-native units and lists explicit parameters without theorems.

claimThe module defines the Cabibbo angle $\theta_c$ (mixing between first and second quark generations) together with Wolfenstein parameters $\lambda, A, \rho, \eta$ and the CKM matrix elements $V_{ud}, V_{us}, V_{ub}, V_{cd}, V_{cs}, V_{cb}$.

background

The module resides in the StandardModel domain and imports IndisputableMonolith.Constants, whose sole documented object is the fundamental RS time quantum $\tau_0 = 1$ tick. It introduces the Cabibbo angle $\theta_c$ for 1-2 generation mixing and the full set of Wolfenstein parameters plus the six listed matrix elements as named constants or functions.

No additional notation or upstream theorems beyond the Constants import appear in the supplied facts. The module therefore supplies the concrete numerical or symbolic entries needed for any CKM-dependent calculation inside the RS Standard Model.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the CKM matrix definitions required by the Standard Model sector of Recognition Science. It extends the base Constants module into flavor physics and would be referenced by any future theorems constructing the full weak-interaction Lagrangian or CP-violating observables, although no downstream uses are currently recorded.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (40)