diff --git a/Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Basic.lean b/Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Basic.lean index 2b6ff77d21496c..a9b0ebc8e1f1cc 100644 --- a/Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Basic.lean +++ b/Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Basic.lean @@ -3,20 +3,20 @@ Copyright (c) 2024 David Kurniadi Angdinata. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: David Kurniadi Angdinata -/ -import Mathlib.AlgebraicGeometry.EllipticCurve.Affine +import Mathlib.AlgebraicGeometry.EllipticCurve.Group import Mathlib.NumberTheory.EllipticDivisibilitySequence /-! # Division polynomials of Weierstrass curves This file defines certain polynomials associated to division polynomials of Weierstrass curves. -These are defined in terms of the auxiliary sequences of normalised elliptic divisibility sequences -defined in `Mathlib.NumberTheory.EllipticDivisibilitySequence`. +These are defined in terms of the auxiliary sequences for normalised elliptic divisibility sequences +(EDS) as defined in `Mathlib.NumberTheory.EllipticDivisibilitySequence`. ## Mathematical background Let $W$ be a Weierstrass curve over a commutative ring $R$. The sequence of $n$-division polynomials -$\psi_n \in R[X, Y]$ of $W$ is the normalised elliptic divisibility sequence with initial values +$\psi_n \in R[X, Y]$ of $W$ is the normalised EDS with initial values * $\psi_0 := 0$, * $\psi_1 := 1$, * $\psi_2 := 2Y + a_1X + a_3$, @@ -25,37 +25,39 @@ $\psi_n \in R[X, Y]$ of $W$ is the normalised elliptic divisibility sequence wit (2X^6 + b_2X^5 + 5b_4X^4 + 10b_6X^3 + 10b_8X^2 + (b_2b_8 - b_4b_6)X + (b_4b_8 - b_6^2))$. Furthermore, define the associated sequences $\phi_n, \omega_n \in R[X, Y]$ by - * $\phi_n := X\psi_n^2 - \psi_{n + 1}\psi_{n - 1}$, and - * $\omega_n := \tfrac{1}{2} \cdot (\psi_{2n} / \psi_n - \psi_n(a_1\phi_n + a_3\psi_n^2))$. - -Note that $\omega_n$ is always well-defined as a polynomial. As a start, it can be shown by -induction that $\psi_n$ always divides $\psi_{2n}$, so that $\psi_{2n} / \psi_n$ is always -well-defined as a polynomial, while division by 2 is well-defined when $R$ has characteristic -different from 2. In general, it can be shown that 2 always divides the polynomial -$\psi_{2n} / \psi_n - \psi_n(a_1\phi_n + a_3\psi_n^2)$ in the characteristic zero universal ring -$\mathbb{Z}[A_i][X, Y]$ of $W$, where $A_i$ are indeterminates. Then $\omega_n$ can be equivalently -defined as its image under the associated universal morphism $\mathbb{Z}[A_i][X, Y] \to R[X, Y]$. + * $\phi_n := X\psi_n^2 - \psi_{n + 1} \cdot \psi_{n - 1}$, and + * $\omega_n := (\psi_{2n} / \psi_n - \psi_n \cdot (a_1\phi_n + a_3\psi_n^2)) / 2$. + +Note that $\omega_n$ is always well-defined as a polynomial in $R[X, Y]$. As a start, it can be +shown by induction that $\psi_n$ always divides $\psi_{2n}$ in $R[X, Y]$, so that +$\psi_{2n} / \psi_n$ is always well-defined as a polynomial, while division by 2 is well-defined +when $R$ has characteristic different from 2. In general, it can be shown that 2 always divides the +polynomial $\psi_{2n} / \psi_n - \psi_n \cdot (a_1\phi_n + a_3\psi_n^2)$ in the characteristic zero +universal ring $\mathcal{R}[X, Y] := \mathbb{Z}[A_1, A_2, A_3, A_4, A_6][X, Y]$ of $W$, where the +$A_i$ are indeterminates. Then $\omega_n$ can be equivalently defined as the image of this division +under the associated universal morphism $\mathcal{R}[X, Y] \to R[X, Y]$ mapping $A_i$ to $a_i$. Now, in the coordinate ring $R[W]$, note that $\psi_2^2$ is congruent to the polynomial $\Psi_2^{[2]} := 4X^3 + b_2X^2 + 2b_4X + b_6 \in R[X]$. As such, in $R[W]$, the recurrences -associated to a normalised elliptic divisibility sequence show that $\psi_n / \psi_2$ are congruent -to certain polynomials in $R[X]$. In particular, define $\tilde{\Psi}_n \in R[X]$ as the auxiliary -sequence for a normalised elliptic divisibility sequence with initial values +associated to a normalised EDS show that $\psi_n / \psi_2$ are congruent to certain polynomials in +$R[X]$. In particular, define $\tilde{\Psi}_n \in R[X]$ as the auxiliary sequence for a normalised +EDS with extra parameter $(\Psi_2^{[2]})^2$ and initial values * $\tilde{\Psi}_0 := 0$, * $\tilde{\Psi}_1 := 1$, * $\tilde{\Psi}_2 := 1$, * $\tilde{\Psi}_3 := \psi_3$, and * $\tilde{\Psi}_4 := \psi_4 / \psi_2$. -The corresponding normalised elliptic divisibility sequence $\Psi_n \in R[X, Y]$ is then given by - * $\Psi_n := \tilde{\Psi}_n\psi_2$ if $n$ is even, and +The corresponding normalised EDS $\Psi_n \in R[X, Y]$ is then given by + * $\Psi_n := \tilde{\Psi}_n \cdot \psi_2$ if $n$ is even, and * $\Psi_n := \tilde{\Psi}_n$ if $n$ is odd. Furthermore, define the associated sequences $\Psi_n^{[2]}, \Phi_n \in R[X]$ by - * $\Psi_n^{[2]} := \tilde{\Psi}_n^2\Psi_2^{[2]}$ if $n$ is even, + * $\Psi_n^{[2]} := \tilde{\Psi}_n^2 \cdot \Psi_2^{[2]}$ if $n$ is even, * $\Psi_n^{[2]} := \tilde{\Psi}_n^2$ if $n$ is odd, - * $\Phi_n := X\Psi_n^{[2]} - \tilde{\Psi}_{n + 1}\tilde{\Psi}_{n - 1}$ if $n$ is even, and - * $\Phi_n := X\Psi_n^{[2]} - \tilde{\Psi}_{n + 1}\tilde{\Psi}_{n - 1}\Psi_2^{[2]}$ if $n$ is odd. + * $\Phi_n := X\Psi_n^{[2]} - \tilde{\Psi}_{n + 1} \cdot \tilde{\Psi}_{n - 1}$ if $n$ is even, and + * $\Phi_n := X\Psi_n^{[2]} - \tilde{\Psi}_{n + 1} \cdot \tilde{\Psi}_{n - 1} \cdot \Psi_2^{[2]}$ + if $n$ is odd. With these definitions in mind, $\psi_n \in R[X, Y]$ and $\phi_n \in R[X, Y]$ are congruent in $R[W]$ to $\Psi_n \in R[X, Y]$ and $\Phi_n \in R[X]$ respectively, which are defined in terms of @@ -73,13 +75,13 @@ $\Psi_2^{[2]} \in R[X]$ and $\tilde{\Psi}_n \in R[X]$. ## Implementation notes -Analogously to `Mathlib.NumberTheory.EllipticDivisibilitySequence`, the $n$-division bivariate -polynomials $\Psi_n$ are defined in terms of the univariate polynomials $\tilde{\Psi}_n$. This is -done partially to avoid ring division, but more crucially to allow the definition of $\Psi_n^{[2]}$ -and $\Phi_n$ as univariate polynomials without needing to work under the coordinate ring, and to -allow the computation of their leading terms without ambiguity. Furthermore, evaluating these -polynomials at a rational point on $W$ recovers their original definition up to linear combinations -of the Weierstrass equation of $W$, hence also avoiding the need to work under the coordinate ring. +Analogously to `Mathlib.NumberTheory.EllipticDivisibilitySequence`, the bivariate polynomials +$\Psi_n$ are defined in terms of the univariate polynomials $\tilde{\Psi}_n$. This is done partially +to avoid ring division, but more crucially to allow the definition of $\Psi_n^{[2]}$ and $\Phi_n$ as +univariate polynomials without needing to work under the coordinate ring, and to allow the +computation of their leading terms without ambiguity. Furthermore, evaluating these polynomials at a +rational point on $W$ recovers their original definition up to linear combinations of the +Weierstrass equation of $W$, hence also avoiding the need to work in the coordinate ring. TODO: implementation notes for the definition of $\omega_n$. @@ -97,11 +99,17 @@ open Polynomial PolynomialPolynomial local macro "C_simp" : tactic => `(tactic| simp only [map_ofNat, C_0, C_1, C_neg, C_add, C_sub, C_mul, C_pow]) -universe u +local macro "map_simp" : tactic => + `(tactic| simp only [map_ofNat, map_neg, map_add, map_sub, map_mul, map_pow, map_div₀, + Polynomial.map_ofNat, Polynomial.map_one, map_C, map_X, Polynomial.map_neg, Polynomial.map_add, + Polynomial.map_sub, Polynomial.map_mul, Polynomial.map_pow, Polynomial.map_div, coe_mapRingHom, + apply_ite <| mapRingHom _, WeierstrassCurve.map]) + +universe r s u v namespace WeierstrassCurve -variable {R : Type u} [CommRing R] (W : WeierstrassCurve R) +variable {R : Type r} {S : Type s} [CommRing R] [CommRing S] (W : WeierstrassCurve R) section Ψ₂Sq @@ -115,11 +123,17 @@ noncomputable def ψ₂ : R[X][Y] := noncomputable def Ψ₂Sq : R[X] := C 4 * X ^ 3 + C W.b₂ * X ^ 2 + C (2 * W.b₄) * X + C W.b₆ -lemma C_Ψ₂Sq_eq : C W.Ψ₂Sq = W.ψ₂ ^ 2 - 4 * W.toAffine.polynomial := by +lemma C_Ψ₂Sq : C W.Ψ₂Sq = W.ψ₂ ^ 2 - 4 * W.toAffine.polynomial := by rw [Ψ₂Sq, ψ₂, b₂, b₄, b₆, Affine.polynomialY, Affine.polynomial] C_simp ring1 +lemma ψ₂_sq : W.ψ₂ ^ 2 = C W.Ψ₂Sq + 4 * W.toAffine.polynomial := by + rw [C_Ψ₂Sq, sub_add_cancel] + +lemma Affine.CoordinateRing.mk_ψ₂_sq : mk W W.ψ₂ ^ 2 = mk W (C W.Ψ₂Sq) := by + rw [C_Ψ₂Sq, map_sub, map_mul, AdjoinRoot.mk_self, mul_zero, sub_zero, map_pow] + -- TODO: remove `twoTorsionPolynomial` in favour of `Ψ₂Sq` lemma Ψ₂Sq_eq : W.Ψ₂Sq = W.twoTorsionPolynomial.toPoly := rfl @@ -315,7 +329,7 @@ lemma Ψ_odd (m : ℕ) : W.Ψ (2 * (m + 2) + 1) = else -W.preΨ' (m + 1) * W.preΨ' (m + 3) ^ 3) := by repeat erw [Ψ_ofNat] simp_rw [preΨ'_odd, if_neg (m + 2).not_even_two_mul_add_one, Nat.even_add_one, ite_not] - split_ifs <;> C_simp <;> rw [C_Ψ₂Sq_eq] <;> ring1 + split_ifs <;> C_simp <;> rw [C_Ψ₂Sq] <;> ring1 lemma Ψ_even (m : ℕ) : W.Ψ (2 * (m + 3)) * W.ψ₂ = W.Ψ (m + 2) ^ 2 * W.Ψ (m + 3) * W.Ψ (m + 5) - W.Ψ (m + 1) * W.Ψ (m + 3) * W.Ψ (m + 4) ^ 2 := by @@ -327,6 +341,10 @@ lemma Ψ_even (m : ℕ) : W.Ψ (2 * (m + 3)) * W.ψ₂ = lemma Ψ_neg (n : ℤ) : W.Ψ (-n) = -W.Ψ n := by simp only [Ψ, preΨ_neg, C_neg, neg_mul (α := R[X][Y]), even_neg] +lemma Affine.CoordinateRing.mk_Ψ_sq (n : ℤ) : mk W (W.Ψ n) ^ 2 = mk W (C <| W.ΨSq n) := by + simp only [Ψ, ΨSq, map_one, map_mul, map_pow, one_pow, mul_pow, ite_pow, apply_ite C, + apply_ite <| mk W, mk_ψ₂_sq] + end Ψ section Φ @@ -386,6 +404,8 @@ section ψ protected noncomputable def ψ (n : ℤ) : R[X][Y] := normEDS W.ψ₂ (C W.Ψ₃) (C W.preΨ₄) n +open WeierstrassCurve (Ψ ψ) + @[simp] lemma ψ_zero : W.ψ 0 = 0 := normEDS_zero .. @@ -418,6 +438,9 @@ lemma ψ_even (m : ℕ) : W.ψ (2 * (m + 3)) * W.ψ₂ = lemma ψ_neg (n : ℤ) : W.ψ (-n) = -W.ψ n := normEDS_neg .. +lemma Affine.CoordinateRing.mk_ψ (n : ℤ) : mk W (W.ψ n) = mk W (W.Ψ n) := by + simp only [ψ, normEDS, Ψ, preΨ, map_mul, map_pow, map_preNormEDS, ← mk_ψ₂_sq, ← pow_mul] + end ψ section φ @@ -428,7 +451,7 @@ section φ protected noncomputable def φ (n : ℤ) : R[X][Y] := C X * W.ψ n ^ 2 - W.ψ (n + 1) * W.ψ (n - 1) -open WeierstrassCurve (φ) +open WeierstrassCurve (Ψ Φ φ) @[simp] lemma φ_zero : W.φ 0 = 1 := by @@ -458,6 +481,106 @@ lemma φ_neg (n : ℤ) : W.φ (-n) = W.φ n := by rw [φ, ψ_neg, neg_sq (R := R[X][Y]), neg_add_eq_sub, ← neg_sub n, ψ_neg, ← neg_add', ψ_neg, neg_mul_neg (α := R[X][Y]), mul_comm <| W.ψ _, φ] +lemma Affine.CoordinateRing.mk_φ (n : ℤ) : mk W (W.φ n) = mk W (C <| W.Φ n) := by + simp_rw [φ, Φ, map_sub, map_mul, map_pow, mk_ψ, mk_Ψ_sq, Ψ, map_mul, + mul_mul_mul_comm _ <| mk W <| ite .., Int.even_add_one, Int.even_sub_one, ← sq, ite_not, + apply_ite C, apply_ite <| mk W, ite_pow, map_one, one_pow, mk_ψ₂_sq] + end φ +section Map + +/-! ### Maps across ring homomorphisms -/ + +open WeierstrassCurve (Ψ Φ ψ φ) + +variable (f : R →+* S) + +lemma map_ψ₂ : (W.map f).ψ₂ = W.ψ₂.map (mapRingHom f) := by + simp only [ψ₂, Affine.map_polynomialY] + +lemma map_Ψ₂Sq : (W.map f).Ψ₂Sq = W.Ψ₂Sq.map f := by + simp only [Ψ₂Sq, map_b₂, map_b₄, map_b₆] + map_simp + +lemma map_Ψ₃ : (W.map f).Ψ₃ = W.Ψ₃.map f := by + simp only [Ψ₃, map_b₂, map_b₄, map_b₆, map_b₈] + map_simp + +lemma map_preΨ₄ : (W.map f).preΨ₄ = W.preΨ₄.map f := by + simp only [preΨ₄, map_b₂, map_b₄, map_b₆, map_b₈] + map_simp + +lemma map_preΨ' (n : ℕ) : (W.map f).preΨ' n = (W.preΨ' n).map f := by + simp only [preΨ', map_Ψ₂Sq, map_Ψ₃, map_preΨ₄, ← coe_mapRingHom, map_preNormEDS'] + map_simp + +lemma map_preΨ (n : ℤ) : (W.map f).preΨ n = (W.preΨ n).map f := by + simp only [preΨ, map_Ψ₂Sq, map_Ψ₃, map_preΨ₄, ← coe_mapRingHom, map_preNormEDS] + map_simp + +lemma map_ΨSq (n : ℤ) : (W.map f).ΨSq n = (W.ΨSq n).map f := by + simp only [ΨSq, map_preΨ, map_Ψ₂Sq, ← coe_mapRingHom] + map_simp + +lemma map_Ψ (n : ℤ) : (W.map f).Ψ n = (W.Ψ n).map (mapRingHom f) := by + simp only [Ψ, map_preΨ, map_ψ₂, ← coe_mapRingHom] + map_simp + +lemma map_Φ (n : ℤ) : (W.map f).Φ n = (W.Φ n).map f := by + simp only [Φ, map_ΨSq, map_preΨ, map_Ψ₂Sq, ← coe_mapRingHom] + map_simp + +lemma map_ψ (n : ℤ) : (W.map f).ψ n = (W.ψ n).map (mapRingHom f) := by + simp only [ψ, map_ψ₂, map_Ψ₃, map_preΨ₄, ← coe_mapRingHom, map_normEDS] + map_simp + +lemma map_φ (n : ℤ) : (W.map f).φ n = (W.φ n).map (mapRingHom f) := by + simp only [φ, map_ψ] + map_simp + +end Map + +section BaseChange + +/-! ### Base changes across algebra homomorphisms -/ + +variable [Algebra R S] {A : Type u} [CommRing A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] + {B : Type v} [CommRing B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] (f : A →ₐ[S] B) + +lemma baseChange_ψ₂ : (W.baseChange B).ψ₂ = (W.baseChange A).ψ₂.map (mapRingHom f) := by + rw [← map_ψ₂, map_baseChange] + +lemma baseChange_Ψ₂Sq : (W.baseChange B).Ψ₂Sq = (W.baseChange A).Ψ₂Sq.map f := by + rw [← map_Ψ₂Sq, map_baseChange] + +lemma baseChange_Ψ₃ : (W.baseChange B).Ψ₃ = (W.baseChange A).Ψ₃.map f := by + rw [← map_Ψ₃, map_baseChange] + +lemma baseChange_preΨ₄ : (W.baseChange B).preΨ₄ = (W.baseChange A).preΨ₄.map f := by + rw [← map_preΨ₄, map_baseChange] + +lemma baseChange_preΨ' (n : ℕ) : (W.baseChange B).preΨ' n = ((W.baseChange A).preΨ' n).map f := by + rw [← map_preΨ', map_baseChange] + +lemma baseChange_preΨ (n : ℤ) : (W.baseChange B).preΨ n = ((W.baseChange A).preΨ n).map f := by + rw [← map_preΨ, map_baseChange] + +lemma baseChange_ΨSq (n : ℤ) : (W.baseChange B).ΨSq n = ((W.baseChange A).ΨSq n).map f := by + rw [← map_ΨSq, map_baseChange] + +lemma baseChange_Ψ (n : ℤ) : (W.baseChange B).Ψ n = ((W.baseChange A).Ψ n).map (mapRingHom f) := by + rw [← map_Ψ, map_baseChange] + +lemma baseChange_Φ (n : ℤ) : (W.baseChange B).Φ n = ((W.baseChange A).Φ n).map f := by + rw [← map_Φ, map_baseChange] + +lemma baseChange_ψ (n : ℤ) : (W.baseChange B).ψ n = ((W.baseChange A).ψ n).map (mapRingHom f) := by + rw [← map_ψ, map_baseChange] + +lemma baseChange_φ (n : ℤ) : (W.baseChange B).φ n = ((W.baseChange A).φ n).map (mapRingHom f) := by + rw [← map_φ, map_baseChange] + +end BaseChange + end WeierstrassCurve diff --git a/Mathlib/NumberTheory/EllipticDivisibilitySequence.lean b/Mathlib/NumberTheory/EllipticDivisibilitySequence.lean index d86085a3d61ed0..5b9b7bfca33077 100644 --- a/Mathlib/NumberTheory/EllipticDivisibilitySequence.lean +++ b/Mathlib/NumberTheory/EllipticDivisibilitySequence.lean @@ -65,7 +65,7 @@ elliptic, divisibility, sequence universe u v w -variable {R : Type u} [CommRing R] (W : ℤ → R) +variable {R : Type u} {S : Type v} [CommRing R] [CommRing S] (W : ℤ → R) (f : R →+* S) /-- The proposition that a sequence indexed by integers is an elliptic sequence. -/ def IsEllSequence : Prop := @@ -102,8 +102,8 @@ lemma IsDivSequence.smul (h : IsDivSequence W) (x : R) : IsDivSequence (x • W) lemma IsEllDivSequence.smul (h : IsEllDivSequence W) (x : R) : IsEllDivSequence (x • W) := ⟨h.left.smul x, h.right.smul x⟩ -/-- The auxiliary sequence for a normalised EDS `W : ℕ → R`, -with initial values `W(0) = 0`, `W(1) = 1`, `W(2) = 1`, `W(3) = c`, and `W(4) = d`. -/ +/-- The auxiliary sequence for a normalised EDS `W : ℕ → R`, with initial values +`W(0) = 0`, `W(1) = 1`, `W(2) = 1`, `W(3) = c`, and `W(4) = d` and extra parameter `b`. -/ def preNormEDS' (b c d : R) : ℕ → R | 0 => 0 | 1 => 1 @@ -159,8 +159,8 @@ lemma preNormEDS'_even (m : ℕ) : preNormEDS' b c d (2 * (m + 3)) = simp only [Nat.mul_add_div two_pos] rfl -/-- The auxiliary sequence for a normalised EDS `W : ℤ → R`, -with initial values `W(0) = 0`, `W(1) = 1`, `W(2) = 1`, `W(3) = c`, and `W(4) = d`. +/-- The auxiliary sequence for a normalised EDS `W : ℤ → R`, with initial values +`W(0) = 0`, `W(1) = 1`, `W(2) = 1`, `W(3) = c`, and `W(4) = d` and extra parameter `b`. This extends `preNormEDS'` by defining its values at negative integers. -/ def preNormEDS (n : ℤ) : R := @@ -208,17 +208,17 @@ lemma preNormEDS_even (m : ℕ) : preNormEDS b c d (2 * (m + 3)) = lemma preNormEDS_neg (n : ℤ) : preNormEDS b c d (-n) = -preNormEDS b c d n := by rw [preNormEDS, Int.sign_neg, Int.cast_neg, neg_mul, Int.natAbs_neg, preNormEDS] -/-- The canonical example of a normalised EDS `W : ℤ → R`, -with initial values `W(0) = 0`, `W(1) = 1`, `W(2) = b`, `W(3) = c`, and `W(4) = d * b`. +/-- The canonical example of a normalised EDS `W : ℤ → R`, with initial values +`W(0) = 0`, `W(1) = 1`, `W(2) = b`, `W(3) = c`, and `W(4) = d * b`. This is defined in terms of `preNormEDS` whose even terms differ by a factor of `b`. -/ def normEDS (n : ℤ) : R := - preNormEDS (b ^ 4) c d n * if Even n.natAbs then b else 1 + preNormEDS (b ^ 4) c d n * if Even n then b else 1 @[simp] lemma normEDS_ofNat (n : ℕ) : normEDS b c d n = preNormEDS' (b ^ 4) c d n * if Even n then b else 1 := by - rw [normEDS, preNormEDS_ofNat, Int.natAbs_ofNat] + simp only [normEDS, preNormEDS_ofNat, Int.even_coe_nat] @[simp] lemma normEDS_zero : normEDS b c d 0 = 0 := by @@ -256,7 +256,7 @@ lemma normEDS_even (m : ℕ) : normEDS b c d (2 * (m + 3)) * b = @[simp] lemma normEDS_neg (n : ℤ) : normEDS b c d (-n) = -normEDS b c d n := by - rw [normEDS, preNormEDS_neg, Int.natAbs_neg, neg_mul, normEDS] + simp only [normEDS, preNormEDS_neg, neg_mul, even_neg] /-- Strong recursion principle for a normalised EDS: if we have * `P 0`, `P 1`, `P 2`, `P 3`, and `P 4`, @@ -287,3 +287,20 @@ noncomputable def normEDSRec {P : ℕ → Sort u} normEDSRec' zero one two three four (fun _ ih => by apply even <;> exact ih _ <| by linarith only) (fun _ ih => by apply odd <;> exact ih _ <| by linarith only) n + +lemma map_preNormEDS' (n : ℕ) : f (preNormEDS' b c d n) = preNormEDS' (f b) (f c) (f d) n := by + induction n using normEDSRec' with + | zero => rw [preNormEDS'_zero, map_zero, preNormEDS'_zero] + | one => rw [preNormEDS'_one, map_one, preNormEDS'_one] + | two => rw [preNormEDS'_two, map_one, preNormEDS'_two] + | three => rw [preNormEDS'_three, preNormEDS'_three] + | four => rw [preNormEDS'_four, preNormEDS'_four] + | _ _ ih => + simp only [preNormEDS'_odd, preNormEDS'_even, map_one, map_sub, map_mul, map_pow, apply_ite f] + repeat rw [ih _ <| by linarith only] + +lemma map_preNormEDS (n : ℤ) : f (preNormEDS b c d n) = preNormEDS (f b) (f c) (f d) n := by + rw [preNormEDS, map_mul, map_intCast, map_preNormEDS', preNormEDS] + +lemma map_normEDS (n : ℤ) : f (normEDS b c d n) = normEDS (f b) (f c) (f d) n := by + rw [normEDS, map_mul, map_preNormEDS, map_pow, apply_ite f, map_one, normEDS]