module module

`IndisputableMonolith.Physics.AnomalousMagneticMoment`

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

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cost.JcostCore module_import
IndisputableMonolith.Foundation.EightTick module_import

declarations in this module (14)

abbrev rs_alpha_inverse L19
def schwinger_term L22
theorem schwinger_term_positive L25
theorem schwinger_is_alpha_over_2pi L29
theorem eight_tick_sum L35
theorem vacuum_phase_one L36
def ae_leading L40
theorem ae_leading_positive L42
theorem schwinger_lt_002 L45
theorem schwinger_in_range L55
def electron_g_factor L59
theorem g_exceeds_dirac L61
def known_ae_coeffs L65
theorem c1_half L71