English
There is a noncomputable descent operation that constructs S' from S, yielding a new Solution' with smaller multiplicity.
Русский
Существуют переходы по нисхождению, создающие S' из S и уменьшающие кратность.
LaTeX
$$noncomputable def Solution'_descent : Solution' hζ where …$$
Lean4
/-- Given `(S : Solution)`, we have that `λ ^ 2` does not divide `S.a + η ^ 2 * S.b`. -/
theorem lambda_sq_not_dvd_a_add_eta_sq_mul_b : ¬λ ^ 2 ∣ (S.a + η ^ 2 * S.b) :=
by
intro ⟨k, hk⟩
rcases S.hab with ⟨k', hk'⟩
refine S.hb ⟨(k - k') * (-η), ?_⟩
rw [show S.a + η ^ 2 * S.b = S.a + S.b - S.b + η ^ 2 * S.b by ring, hk',
show λ ^ 2 * k' - S.b + η ^ 2 * S.b = λ * (S.b * (η + 1) + λ * k') by rw [coe_eta]; ring, pow_two, mul_assoc] at hk
simp only [mul_eq_mul_left_iff, hζ.zeta_sub_one_prime'.ne_zero, or_false] at hk
apply_fun (· * -↑η) at hk
rw [show (S.b * (η + 1) + λ * k') * -η = (-S.b) * (η ^ 2 + η + 1 - 1) - η * λ * k' by ring, eta_sq,
show -S.b * (-↑η - 1 + ↑η + 1 - 1) = S.b by ring, sub_eq_iff_eq_add] at hk
rw [hk]
ring
