derived_parameters
plain-language theorem explainer
Derived parameters assembles a record of Standard Model observables including CKM and PMNS mixing angles, the locked inverse fine-structure constant, the QCD beta coefficient, lepton rung indices, and quark step differences. A particle physicist testing geometric predictions against collider data would cite the record as the canonical output of the Recognition Science derivation chain. The body is a direct record construction that pulls each field from upstream geometric lemmas without further reduction.
Claim. Let $V_{us}$, $V_{cb}$, $V_{ub}$ be the Cabibbo-Kobayashi-Maskawa matrix elements, let $s^2_{13}$, $s^2_{12}$, $s^2_{23}$ be the squared sine of the Pontecorvo-Maki-Nakagawa-Sakata angles, let $a^{-1}$ be the locked inverse fine-structure constant, let $b_0$ be the leading QCD beta-function coefficient, and let the lepton rungs and quark steps be the integer indices on the phi-ladder. Then derived_parameters is the record whose fields are exactly these quantities, each taken from the corresponding geometric prediction.
background
Recognition Science obtains all Standard Model parameters from a single functional equation whose self-similar fixed point is the golden ratio phi. The structure SMDerivation collects the three CKM elements and three PMNS mixing parameters from geometric constructions, the locked coupling from the algebraic identity alphaLock = (1 - 1/phi)/2, the QCD coefficient b0 from the Recognition Science beta function, and the rung and step lists from the phi-ladder indexing of fermion generations. Upstream results supply the rung definition as a natural-number index on the ladder and the algebraic simplification that removes the factor of one-half in alphaLock.
proof idea
The definition is a record literal. Each field is populated by direct reference: cabibbo_angle_Vus to CKMGeometry.V_us_pred, alpha_inv_lock to the reciprocal of Constants.alphaLock, lepton_rungs to the list of RSBridge.rung applications on the three lepton flavors, and the remaining fields to the corresponding geometric or bridge lemmas. No tactics or reductions occur beyond the construction.
why it matters
The definition packages the complete set of low-energy Standard Model parameters that follow from the forcing chain T5 through T8 and the Recognition Composition Law. It supplies the concrete output that downstream modules can use to compare geometric predictions with experiment, thereby closing the derivation from the eight-tick octave and D=3 spatial dimensions to observable mixing angles and the alpha band. No open question is left inside the module; the record simply records the leading-order geometric values.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.