SMDerivation
open lean source
IndisputableMonolith.Physics.ParticleSummary on GitHub at line 13.
browse module
All declarations in this module, on Recognition.
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.
depends on
used by
formal source
10namespace IndisputableMonolith.Physics.Summary
11
12/-- Standard Model Parameters derived from Recognition Science. -/
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. -/
30noncomputable def derived_parameters : SMDerivation := {
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