theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachPositiveScalar_exp_cancel (x : ℝ) : Real.exp (-Real.eulerMascheroniConstant) * (Real.exp Real.eulerMascheroniConstant * x) = x

Exact cancellation of the Euler normalization, without an estimate for gamma.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachPositiveScalar_change (v : ℝ) (hv : 3 ≤ v) : have z := (v - 3) / (v - 1); 0 ≤ z ∧ z < 1 ∧ (3 - z) / (1 - z) = v ∧ (1 / (1 - z) - 1 / (3 - z)) * (2 / (v - 1) ^ 2) = 1 / v

Literal change of variables used only on the existing lower-factor domain.