English
Let x,y,n be natural numbers with y < x, 2 ∣ x − y, and x not divisible by 2; for even n and n ≠ 0, the 2-adic padding satisfies: padicValNat 2 (x^n − y^n) + 1 = padicValNat 2 (x + y) + padicValNat 2 (x − y) + padicValNat 2 n.
Русский
Пусть x,y,n натуральные, y < x, 2 | x − y и x нечетно; при чётном n, n ≠ 0: padicValNat 2 (x^n − y^n) + 1 = padicValNat 2 (x + y) + padicValNat 2 (x − y) + padicValNat 2 n.
LaTeX
$$$\\forall x,y,n \\in \\mathbb{N},\\ y < x \\land 2 \\mid (x - y) \\land x \\not\\mid 2 \\Rightarrow \\mathrm{padicVal}_2(x^n - y^n) + 1 = \\mathrm{padicVal}_2(x+y) + \\mathrm{padicVal}_2(x-y) + \\mathrm{padicVal}_2(n)$$$
Lean4
theorem pow_two_sub_pow (hyx : y < x) (hxy : 2 ∣ x - y) (hx : ¬2 ∣ x) {n : ℕ} (hn : n ≠ 0) (hneven : Even n) :
padicValNat 2 (x ^ n - y ^ n) + 1 = padicValNat 2 (x + y) + padicValNat 2 (x - y) + padicValNat 2 n :=
by
simp only [← Nat.cast_inj (R := ℕ∞), Nat.cast_add]
iterate 4 rw [padicValNat_eq_emultiplicity]
· exact Nat.two_pow_sub_pow hxy hx hneven
· exact hn
· exact Nat.sub_ne_zero_of_lt hyx
· cutsat
· simp [← Nat.pos_iff_ne_zero, tsub_pos_iff_lt, Nat.pow_lt_pow_left hyx hn]
