SMDerivation
SMDerivation records the derived Standard Model mixing angles from CKM and PMNS sectors, the locked inverse fine-structure constant, the QCD beta coefficient, lepton rung indices, and quark steps on the quarter-ladder. A physicist assembling unification predictions would cite this record to access the complete observable set in one typed container. The definition is a direct structure declaration whose fields are populated by explicit assignments from upstream geometric results.
claimThe record type contains the Cabibbo angle $V_{us}$, CKM elements $V_{cb}$ and $V_{ub}$, PMNS parameters $sin^2 theta_{13}$, $sin^2 theta_{12}$, $sin^2 theta_{23}$, the locked inverse fine-structure constant $alpha^{-1}$, the QCD beta coefficient $b_0$, the lepton rung list, and the quark step list under the quarter-ladder map $k mapsto k/4$.
background
Recognition Science obtains particle masses from the phi-ladder formula (yardstick times phi to the power of rung minus eight plus gap) and the eight-tick octave. The lepton_rungs theorem fixes the electron, muon and tau at baseline indices 2, 13 and 19. The quarter definition embeds integer steps as rational fractions k/4. The Quark inductive type enumerates the six flavors while the Coupling abbrev encodes the sparse FEP Markov-blanket condition. The from theorem reduces seven axioms to four structural conditions that underwrite these embeddings.
proof idea
The declaration is a plain structure definition that introduces a record type with ten named fields of types real, list of integers and list of rationals. No tactics or lemmas are invoked inside the structure; it serves only as a typed container. Downstream code in the same module populates the fields by direct assignment from CKMGeometry and MixingDerivation predictions.
why it matters in Recognition Science
SMDerivation supplies the complete set of derived Standard Model observables that derived_parameters instantiates. It closes the chain from the mass formula and T5 J-uniqueness to concrete predictions for alpha inverse inside the 137.03 band and the quark-lepton hierarchies. It touches the open question of whether the quarter-ladder hypothesis for Gap 6 quarks remains consistent with the full Recognition Composition Law across sectors.
scope and limits
- Does not derive the numerical values of the mixing angles or couplings.
- Does not prove the underlying phi-ladder rung assignments.
- Does not verify unitarity of the CKM or PMNS matrices.
- Does not address neutrino mass eigenvalues beyond the listed PMNS parameters.
formal statement (Lean)
13structure SMDerivation where
14 -- Mixing
15 cabibbo_angle_Vus : ℝ
16 ckm_Vcb : ℝ
17 ckm_Vub : ℝ
18 pmns_sin2_theta13 : ℝ
19 pmns_sin2_theta12 : ℝ
20 pmns_sin2_theta23 : ℝ
21 -- Coupling
22 alpha_inv_lock : ℝ
23 qcd_b0 : ℝ
24 -- Hierarchy
25 lepton_rungs : List ℤ
26 /-- Quark step sizes (quarter-ladder hypothesis lane; Gap 6). -/
27 quark_steps : List ℚ
28
29/-- Derived parameters from the geometric foundations. -/