English
Given S' with a,b,c in a cyclotomic extension, a^3 and b^3 have a certain congruence modulo λ^4
Русский
Для S' в циклотомическом расширении a^3 и b^3 удовлетворяют заданной конгруэнции moduλ λ^4
LaTeX
$$$a^3 \equiv \text{something} \mod \lambda^4$, $b^3 \equiv \text{something} \mod \lambda^4$$$
Lean4
/-- Given `S' : Solution'`, then `S'.a` and `S'.b` are both congruent to `1` modulo `λ ^ 4` or are
both congruent to `-1`. -/
theorem a_cube_b_cube_congr_one_or_neg_one :
λ ^ 4 ∣ S'.a ^ 3 - 1 ∧ λ ^ 4 ∣ S'.b ^ 3 + 1 ∨ λ ^ 4 ∣ S'.a ^ 3 + 1 ∧ λ ^ 4 ∣ S'.b ^ 3 - 1 :=
by
obtain ⟨z, hz⟩ := S'.hcdvd
rcases lambda_pow_four_dvd_cube_sub_one_or_add_one_of_lambda_not_dvd hζ S'.ha with ⟨x, hx⟩ | ⟨x, hx⟩ <;>
rcases lambda_pow_four_dvd_cube_sub_one_or_add_one_of_lambda_not_dvd hζ S'.hb with ⟨y, hy⟩ | ⟨y, hy⟩
· exfalso
replace hζ : IsPrimitiveRoot ζ (3 ^ 1) := by rwa [pow_one]
refine hζ.toInteger_sub_one_not_dvd_two (by decide) ⟨S'.u * λ ^ 2 * z ^ 3 - λ ^ 3 * (x + y), ?_⟩
symm
calc
_ = S'.u * (λ * z) ^ 3 - λ ^ 4 * x - λ ^ 4 * y := by ring
_ = (S'.a ^ 3 + S'.b ^ 3) - (S'.a ^ 3 - 1) - (S'.b ^ 3 - 1) := by rw [← hx, ← hy, ← hz, ← S'.H]
_ = 2 := by ring
· left
exact ⟨⟨x, hx⟩, ⟨y, hy⟩⟩
· right
exact ⟨⟨x, hx⟩, ⟨y, hy⟩⟩
· exfalso
replace hζ : IsPrimitiveRoot ζ (3 ^ 1) := by rwa [pow_one]
refine hζ.toInteger_sub_one_not_dvd_two (by decide) ⟨λ ^ 3 * (x + y) - S'.u * λ ^ 2 * z ^ 3, ?_⟩
symm
calc
_ = λ ^ 4 * x + λ ^ 4 * y - S'.u * (λ * z) ^ 3 := by ring
_ = (S'.a ^ 3 + 1) + (S'.b ^ 3 + 1) - (S'.a ^ 3 + S'.b ^ 3) := by rw [← hx, ← hy, ← hz, ← S'.H]
_ = 2 := by ring
