def
definition
def or abbrev
base_shift
show as:
view Lean formalization →
formal statement (Lean)
56noncomputable def base_shift : ℝ := 2 * W + ledger_fraction
proof body
Definition body.
57
58/-! ## Radiative Corrections -/
59
60/-- Primary radiative correction: α². -/
used by (18)
-
base_shift_denominator_forced -
base_shift_denominator_forced_no_hk -
base_shift_denominator_scale_forced_no_hc_pos -
base_shift_eq_34_plus_29_over_44 -
base_shift_kn_forced_under_passive_bound -
base_shift_kn_forced_under_passive_bound_no_hk -
base_shift_numerator_offset_forced -
base_shift_wallpaper_multiplier_forced -
base_shift_weight_split_forced -
o4_channel_closure_certificate -
radiative_cubic_coeff_forced -
refined_shift_channel_form -
refined_shift_cubic_coeff_forced -
refined_shift_full_affine_forced_from_base_role -
refined_shift_wallpaper_iff_cubic_from_base_role -
refined_shift_wallpaper_multiplier_forced_from_cubic_scale -
base_shift_bounds -
refined_shift