IndisputableMonolith.Physics.ParticleSummary

   1import IndisputableMonolith.Physics.MixingDerivation
   2import IndisputableMonolith.Physics.RunningCouplings
   3import IndisputableMonolith.Physics.LeptonGenerations.Necessity
   4import IndisputableMonolith.Physics.QuarkMasses
   5import IndisputableMonolith.Physics.NeutrinoSector
   6import IndisputableMonolith.Physics.AnomalousMoments
   7import IndisputableMonolith.Physics.Hadrons
   8import IndisputableMonolith.Physics.MixingGeometry
   9
  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
  44