SMDerivation
plain-language theorem explainer
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.
Claim. The 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.