`derived_parameters`

definition

show as: view math explainer →

module: IndisputableMonolith.Physics.ParticleSummary
domain: Physics
line: 30 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Physics.ParticleSummary on GitHub at line 30.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

  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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.