`weak_coupling_cert`

proved

show as: view math explainer →

module: IndisputableMonolith.StandardModel.WeakCoupling
domain: StandardModel
line: 102 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.StandardModel.WeakCoupling on GitHub at line 102.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

  99  alpha_W_positive : 0 < alpha_W
 100  alpha_W_exceeds_alpha : alpha < alpha_W
 101
 102theorem weak_coupling_cert : WeakCouplingCert where
 103  alpha_from_cube := rfl
 104  sin2_from_phi := rfl
 105  alpha_W_def := rfl
 106  alpha_W_positive := alpha_W_pos
 107  alpha_W_exceeds_alpha := alpha_W_gt_alpha
 108
 109end
 110
 111end WeakCoupling
 112end StandardModel
 113end IndisputableMonolith

papers checked against this theorem

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