def definition def or abbrev

`lambShiftProofs`

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

formal statement (Lean)

 194def lambShiftProofs : LambShiftProofs where
 195  shift_range := lamb_shift_approx

proof body

Definition body.

 196  s_wave_l_zero := rfl
 197  p_wave_l_positive := p_wave_excluded_from_origin
 198  precision := precision_agreement
 199  alpha_power := alpha_fifth_power
 200
 201/-! ## Related QED Effects -/
 202
 203/-- Other precision QED tests. -/

depends on (6)

Lean names referenced from this declaration's body.

tests in IndisputableMonolith.ILG.CPMInstance decl_use
alpha_fifth_power in IndisputableMonolith.QFT.LambShift decl_use
lamb_shift_approx in IndisputableMonolith.QFT.LambShift decl_use
LambShiftProofs in IndisputableMonolith.QFT.LambShift decl_use
precision_agreement in IndisputableMonolith.QFT.LambShift decl_use
p_wave_excluded_from_origin in IndisputableMonolith.QFT.LambShift decl_use