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

wolfenstein_lambda

show as:
view Lean formalization →

Wolfenstein lambda supplies the leading mixing parameter in the RS-derived CKM matrix by equating it to the sine of the Cabibbo angle. Quark-flavor physicists cite the value when writing the standard Wolfenstein expansion for weak decay amplitudes. The definition is a direct one-line alias to the cabibboAngle constant already fixed in the module.

claim$λ = sin(θ_C) ≈ 0.227$, where $θ_C$ is the Cabibbo angle between the first and second quark generations.

background

The CKM matrix in Recognition Science is constructed from φ-quantized mixing angles that arise from the eight-tick phase structure. The Cabibbo angle θ_C is the dominant off-diagonal element connecting the first two generations. Upstream, cabibboAngle is supplied in the same module as the numerical constant 0.227 and in ThreeGenerations as arcsin(1/φ²).

proof idea

The declaration is a one-line wrapper that aliases the cabibboAngle definition already present in the module.

why it matters in Recognition Science

This definition supplies the λ parameter required by every Wolfenstein-form CKM element (V_ud through V_ts) in the module. It links the φ-derived Cabibbo angle to the experimental parametrization used in particle phenomenology. The module targets the PRD paper on CKM Matrix from Golden Ratio Geometry and sits inside the T7 eight-tick octave landmark of the forcing chain.

scope and limits

formal statement (Lean)

  54noncomputable def wolfenstein_lambda : ℝ := cabibboAngle

proof body

Definition body.

  55
  56/-- The Wolfenstein parameter A ≈ 0.82. -/

used by (8)

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

depends on (5)

Lean names referenced from this declaration's body.