`ckmlambdaCert`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.CKMLambdaFromPhiLadder
domain: Foundation
line: 73 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.CKMLambdaFromPhiLadder on GitHub at line 73.

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

  70  cabibbo_phi3 : phi ^ 3 = 2 * phi + 1
  71  cabibbo_band : (0.225 : ℝ) < cabibboPhi ∧ cabibboPhi < 0.240
  72
  73noncomputable def ckmlambdaCert : CKMLambdaCert where
  74  wolfenstein_A := wolfensteinA_val
  75  A_in_pdg := wolfensteinA_in_pdg_band
  76  cabibbo_phi3 := phi3_eq
  77  cabibbo_band := cabibbo_in_band
  78
  79end IndisputableMonolith.Foundation.CKMLambdaFromPhiLadder

papers checked against this theorem

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