mixingAnglesDefault
plain-language theorem explainer
Canonical CKM mixing-angle magnitudes at the RecogSpec layer: three dimensionless entries built as successive inverse powers of φ. Anyone assembling the explicit dimensionless pack or the universal-dimless witness cites this default. The body is a one-line structure constructor, not a derived identity.
Claim. For $\varphi \in \mathbb{R}$, the default CKM mixing-angle magnitudes are $V_{us} = 1/\varphi$, $V_{cb} = 1/\varphi^{2}$, $V_{ub} = 1/\varphi^{3}$.
background
RecogSpec packages dimensionless Standard-Model observables that the Recognition ledger is asked to match. Among them are the CKM mixing-angle magnitudes: three real numbers $V_{us}$, $V_{cb}$, $V_{ub}$ collected in the structure CkmMixingAngles (doc: "CKM mixing-angle magnitudes (dimensionless)").
The golden ratio $\varphi$ is the self-similar fixed point forced by the Recognition Composition Law (forcing chain T5–T6). Spec-level defaults for several dimensionless quantities are written as short algebraic expressions in $\varphi$, so that later band checks and honest-closure certificates can treat them as $\varphi$-closed data rather than free parameters.
This declaration is the mixing-angle slot of that pattern. The module doc and CERT tag mark it as a definitional, legacy placeholder at the specification layer, not a derived fit to measured CKM angles.
proof idea
Pure definition: the three fields of the CKM mixing-angle structure are filled by the term $\langle 1/\varphi,, 1/\varphi^{2},, 1/\varphi^{3}\rangle$. No lemmas are applied; the @[simp] attribute exposes the components for later rewriting in pack constructors.
why it matters
Feeds the explicit dimensionless pack (dimlessPack_explicit) and the explicit universal-dimless record (UD_explicit), both of which set mixingAngles := mixingAnglesDefault φ (resp. mixingAngles0). Those packs are the data side of band-matching and of the honest-closure certificate, whose Part A requires observables to be $\varphi$-closed.
In the Recognition framework this is scaffolding for the dimensionless sector of the forcing story: once masses, $\alpha$, and mixings sit on the $\varphi$-ladder, the same ledger that forces $D=3$ and the eight-tick octave can be checked against SM bands. The CERT tag and "legacy placeholder" wording signal that a sharper derivation of the three exponents may replace this default without changing the pack API.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.