pith. machine review for the scientific record. sign in
def definition def or abbrev

derived_parameters

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  30noncomputable def derived_parameters : SMDerivation := {

proof body

Definition body.

  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

depends on (21)

Lean names referenced from this declaration's body.