theorem
proved
tactic proof
mass_match_pos
show as:
view Lean formalization →
formal statement (Lean)
76theorem mass_match_pos (mass_above alpha_at_threshold : ℝ)
77 (h_mass_pos : 0 < mass_above) (h_alpha_pos : 0 < alpha_at_threshold)
78 (h_alpha_small : alpha_at_threshold < 1) :
79 0 < mass_match mass_above alpha_at_threshold := by
proof body
Tactic-mode proof.
80 unfold mass_match
81 apply mul_pos h_mass_pos
82 -- d_2_mass = -89/432 ≈ -0.206. We bound (a/π)^2 < 1, so the correction is > -1.
83 have h_d_gt : (-1 : ℝ) < d_2_mass := by unfold d_2_mass; norm_num
84 have h_d_neg : d_2_mass < 0 := by unfold d_2_mass; norm_num
85 have h_a_pos : 0 < alpha_at_threshold / Real.pi := div_pos h_alpha_pos Real.pi_pos
86 have h_a_sq_pos : 0 < (alpha_at_threshold / Real.pi) ^ 2 := pow_pos h_a_pos 2
87 -- Bound (a/π)^2 < 1: a < 1 and π > 1, so a/π < 1, so (a/π)^2 < 1.
88 have h_pi_gt_one : (1 : ℝ) < Real.pi := by
89 linarith [Real.pi_gt_three]
90 have h_a_over_pi_lt_one : alpha_at_threshold / Real.pi < 1 := by
91 rw [div_lt_one Real.pi_pos]; linarith
92 have h_a_sq_lt_one : (alpha_at_threshold / Real.pi) ^ 2 < 1 := by
93 have : (alpha_at_threshold / Real.pi) ^ 2 < 1 ^ 2 := by
94 apply sq_lt_sq' <;> nlinarith [h_a_pos]
95 simpa using this
96 -- d_2_mass * x where x ∈ (0, 1), d_2_mass ∈ (-1, 0), so product ∈ (-1, 0).
97 have h_prod_gt : -1 < d_2_mass * (alpha_at_threshold / Real.pi) ^ 2 := by
98 nlinarith [h_d_gt, h_d_neg, h_a_sq_pos, h_a_sq_lt_one]
99 linarith
100
101/-! ## Round-trip: matching plus its inverse is the identity to leading order -/
102
103/-- The matching at any threshold is a multiplicative perturbation; its inverse
104 factor at NLO is `1 - c_2_alpha * (a/pi)^2 + O(a^4)`. We expose this as a
105 structural definition rather than re-proving the perturbative inverse. -/