wolfenstein_A
plain-language theorem explainer
The declaration supplies the constant 0.82 for the Wolfenstein parameter A in the standard four-parameter parametrization of the CKM quark mixing matrix. Flavor physicists constructing explicit CKM elements from Recognition Science inputs would cite this value when scaling the λ² and λ³ terms. The definition is a direct numerical assignment with no computation or reduction steps.
Claim. The Wolfenstein parameter $A$ is the real number $0.82$.
background
The StandardModel.CKMMatrix module derives the 3×3 unitary CKM matrix from φ-quantized mixing angles tied to the eight-tick phase structure. The Wolfenstein parametrization approximates the matrix elements with four real parameters λ, A, ρ, η, and the module supplies approximate magnitudes for the unitary matrix V with entries such as 0.974, 0.227, 0.041 in the first row. This definition provides the numerical value for A that scales the off-diagonal blocks.
proof idea
Direct constant definition assigning the real number 0.82.
why it matters
This definition supplies the A parameter required by the CKMLambdaCert structure, which certifies wolfenstein_A = 9/11 together with the PDG band check |(wolfensteinA : ℝ) - 0.826| < 0.013. It is used to define the explicit CKM elements V_cb, V_td, V_ts, and V_ub. The construction aligns with the paper proposition on CKM Matrix from Golden Ratio Geometry and the T7 eight-tick octave landmark.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.