pith. machine review for the scientific record. sign in
def definition def or abbrev high

V_cb

show as:
view Lean formalization →

The definition sets the CKM matrix element V_cb to the product of Wolfenstein parameters A and lambda squared. Particle physicists deriving quark mixing angles from Recognition Science would cite this when linking the eight-tick phase structure to experimental CKM values. The construction is a direct one-line definition that multiplies the imported constants.

claimThe CKM matrix element $V_{cb}$ equals $A lambda^2$, where $A approx 0.82$ is the Wolfenstein parameter and $lambda = sin theta_C approx 0.227$ is the sine of the Cabibbo angle.

background

The module derives CKM matrix elements from phi-quantized mixing angles tied to the eight-tick phase structure in Recognition Science. The Wolfenstein parameterization approximates the 3x3 unitary matrix with four parameters, and this definition supplies the (2,3) element magnitude. Upstream, wolfenstein_lambda is defined as cabibboAngle and wolfenstein_A as the constant 0.82.

proof idea

This is a one-line definition that multiplies the Wolfenstein A parameter by the square of the lambda parameter.

why it matters in Recognition Science

This definition supplies the V_cb value used in downstream results such as the Jarlskog witness positivity theorem and the T11 certificate for geometric origin from cube edges. It fills the SM-012 target of deriving CKM elements from phi-angles in the eight-tick structure. It connects to the broader RS derivation of Standard Model parameters via the Recognition Composition Law and D=3 spatial dimensions.

scope and limits

formal statement (Lean)

  79noncomputable def V_cb : ℂ := wolfenstein_A * wolfenstein_lambda^2

used by (24)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (3)

Lean names referenced from this declaration's body.