hypothesis6
plain-language theorem explainer
The declaration assigns the Wolfenstein parameter λ the closed-form value (φ − 1)² / φ. Quark-mixing specialists examining Recognition Science derivations of the CKM matrix cite this expression when testing golden-ratio predictions against the observed Cabibbo angle. The assignment is a direct algebraic definition with no lemmas or reduction steps.
Claim. Let φ be the golden ratio. The Wolfenstein parameter λ is defined by λ = (φ − 1)² / φ.
background
The CKM module derives quark mixing angles from φ-quantized phases linked to the eight-tick structure. The golden ratio φ enters as the self-similar fixed point forced in the T0–T8 chain. This definition supplies the leading first-generation mixing parameter for the approximate CKM matrix whose magnitudes are listed in the module header.
proof idea
The body is a one-line noncomputable definition that directly evaluates the algebraic expression (phi - 1)^2 / phi. No tactics, no upstream lemmas, and no reduction are applied.
why it matters
The definition is referenced by bestCabibboFit, which performs the numerical comparison to the measured Cabibbo angle and notes the 4 % discrepancy. It contributes the concrete φ-expression required by the paper proposition on CKM elements from golden-ratio geometry. The comment leaves open whether higher-order phi-ladder corrections can reduce the residual.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.