derived_parameters
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not derive the numerical values of the parameters inside this module.
- Does not include fermion mass predictions or the phi-ladder mass formula.
- Does not perform renormalization-group evolution beyond the locked alpha value.
- Does not incorporate experimental error bars or higher-order corrections.
formal statement (Lean)
30noncomputable def derived_parameters : SMDerivation := {
proof body
Definition body.
31 cabibbo_angle_Vus := CKMGeometry.V_us_pred
32 ckm_Vcb := CKMGeometry.V_cb_pred
33 ckm_Vub := CKMGeometry.V_ub_pred
34 pmns_sin2_theta13 := MixingDerivation.sin2_theta13_pred
35 pmns_sin2_theta12 := MixingDerivation.sin2_theta12_pred
36 pmns_sin2_theta23 := MixingDerivation.sin2_theta23_pred
37 alpha_inv_lock := 1 / Constants.alphaLock
38 qcd_b0 := b0_qcd_rs
39 lepton_rungs := [RSBridge.rung .e, RSBridge.rung .mu, RSBridge.rung .tau]
40 quark_steps := [MixingGeometry.step_top_bottom, MixingGeometry.step_bottom_charm, MixingGeometry.step_charm_strange]
41}
42
43end IndisputableMonolith.Physics.Summary