Documentation

Atlas.EllipticCurves.code.WeilPairing

def WeilPairing.functionEvalAtDivisor {P : Type u_1} [DecidableEq P] {k : Type u_2} [CommGroup k] (f : P → k) (D : P →₀ ℤ) :
k

Evaluation of a function f : P → k at a divisor D = ∑ nₚ [P], producing the product ∏ f(p) ^ nₚ (Definition 23.18 in Sutherland's notes).

Instances For
    theorem WeilPairing.functionEvalAtDivisor_mul {P : Type u_1} [DecidableEq P] {k : Type u_2} [CommGroup k] (f : P → k) (D₁ D₂ : P →₀ ℤ) :

    Evaluation at a divisor is multiplicative in the divisor: f(D₁ + D₂) = f(D₁) · f(D₂).

    theorem WeilPairing.weilReciprocity {P : Type u_1} [DecidableEq P] {k : Type u_2} [CommGroup k] (Φ : CurveDiv.FunctionFieldDiv P) (evalAt : Φ.F → P → k) (f g : Additive Φ.F) (hdisjoint : Disjoint (Φ.divMap f).support (Φ.divMap g).support) :

    Weil reciprocity (Theorem 23.20): for functions f, g on a smooth projective curve whose divisors have disjoint support, we have f(div g) = g(div f).

    noncomputable def WeilPairing.lineFunction {F : Type u_1} [Field F] [DecidableEq F] (W : WeierstrassCurve.Affine F) (P Q R : W.Point) :
    F

    The numerator L_{P,Q} of the line function from Definition 23.16, evaluated at a third point R. Returns the value of the line through P and Q (or the tangent at P if P = Q).

    Instances For
      noncomputable def WeilPairing.lineFunctionG {F : Type u_1} [Field F] [DecidableEq F] (W : WeierstrassCurve.Affine F) :
      W.Point → W.Point → W.Point → Fˣ

      The function G_{P,Q} := L_{P,Q} / L_{P+Q, -(P+Q)} from Definition 23.16, packaged as a function into Fˣ and forced to 1 when the denominator/value vanishes.

      Instances For
        noncomputable def WeilPairing.divLine {F₀ : Type u_1} [Field F₀] [DecidableEq F₀] {W : WeierstrassCurve.Affine F₀} (P Q : W.Point) :

        The divisor of the line L_{P,Q}, namely [P] + [Q] + [-(P+Q)] - 3[0].

        Instances For
          noncomputable def WeilPairing.divG {F₀ : Type u_1} [Field F₀] [DecidableEq F₀] {W : WeierstrassCurve.Affine F₀} (P Q : W.Point) :

          The divisor of G_{P,Q}, namely [P] + [Q] - [P+Q] - [0].

          Instances For
            noncomputable def WeilPairing.divFunG_ax {F : Type u_2} [Field F] [DecidableEq F] (W : WeierstrassCurve.Affine F) :
            (W.Point → Fˣ) → W.Point →₀ ℤ

            Axiomatized "divisor of a function" map sending a function W.Point → Fˣ to its formal divisor. Used as a placeholder for the algebraic-geometric div operator.

            Instances For
              noncomputable def WeilPairing.divFunG {F : Type u_2} [Field F] [DecidableEq F] (W : WeierstrassCurve.Affine F) :
              (W.Point → Fˣ) → W.Point →₀ ℤ

              The "divisor of a function" map for lineFunctionG-style functions, defined via divFunG_ax.

              Instances For

                The divisor of the function G_{P,Q} is [P] + [Q] - [P+Q] - [0], as expected from Definition 23.16.

                def WeilPairing.LinearlyEquivalent {F₀ : Type u_1} [Field F₀] {W : WeierstrassCurve.Affine F₀} (PrincE : AddSubgroup (W.Point →₀ ℤ)) (D₁ D₂ : W.Point →₀ ℤ) :

                Two divisors D₁, D₂ are linearly equivalent (with respect to a subgroup of principal divisors PrincE) when D₁ - D₂ ∈ PrincE.

                Instances For
                  def WeilPairing.millerFunctionNat {F : Type u_2} [Field F] [DecidableEq F] (W : WeierstrassCurve.Affine F) (P : W.Point) :
                  ℕ → W.Point → Fˣ

                  The Miller function f_{n,P} for natural n, defined recursively (Definition 23.23): f_{0,P} = f_{1,P} = 1 and f_{n+2,P} = f_{n+1,P} · G_{P, (n+1)P}.

                  Instances For
                    noncomputable def WeilPairing.millerFunction {F : Type u_2} [Field F] [DecidableEq F] (W : WeierstrassCurve.Affine F) (P : W.Point) (n : ℤ) :
                    W.Point → Fˣ

                    The Miller function f_{n,P} extended to all integers (Definition 23.23): for n < 0, f_{-n,P} := (f_{n,P} · G_{nP, -nP})⁻¹.

                    Instances For
                      @[simp]
                      theorem WeilPairing.millerFunction_zero {F : Type u_2} [Field F] [DecidableEq F] (W : WeierstrassCurve.Affine F) (P : W.Point) :
                      millerFunction W P 0 = fun (x : W.Point) => 1

                      The Miller function at index 0 is the constant function 1.

                      @[simp]
                      theorem WeilPairing.millerFunction_one {F : Type u_2} [Field F] [DecidableEq F] (W : WeierstrassCurve.Affine F) (P : W.Point) :
                      millerFunction W P 1 = fun (x : W.Point) => 1

                      The Miller function at index 1 is the constant function 1.

                      theorem WeilPairing.millerFunctionNat_succ {F : Type u_2} [Field F] [DecidableEq F] (W : WeierstrassCurve.Affine F) (P : W.Point) (n : ℕ) (hn : 1 ≤ n) (R : W.Point) :
                      millerFunctionNat W P (n + 1) R = millerFunctionNat W P n R * lineFunctionG W P (↑n • P) R

                      Recursive step for the natural-index Miller function: f_{n+1,P}(R) = f_{n,P}(R) · G_{P, nP}(R) for n ≥ 1.

                      theorem WeilPairing.millerFunction_neg {F : Type u_2} [Field F] [DecidableEq F] (W : WeierstrassCurve.Affine F) (P : W.Point) (n : ℕ) (hn : 0 < n) (R : W.Point) :
                      millerFunction W P (-↑n) R = (millerFunction W P (↑n) R * lineFunctionG W (↑n • P) (-↑n • P) R)⁻¹

                      Relation between the Miller function at -n and at n, for positive natural n.

                      noncomputable def WeilPairing.millerFunctionDivisor {F : Type u_3} [Field F] [DecidableEq F] (W : WeierstrassCurve.Affine F) :
                      W.Point → ℤ → W.Point →₀ ℤ

                      The divisor of f_{n,P}, namely n[P] - (n-1)[0] - [nP] (Lemma 23.24(i)).

                      Instances For

                        Expands the definition of millerFunctionDivisor as n[P] - (n-1)[0] - [nP] (Lemma 23.24(i)).

                        theorem WeilPairing.millerFunction_add {F : Type u_2} [Field F] [DecidableEq F] (W : WeierstrassCurve.Affine F) (P : W.Point) (m n : ℤ) (R : W.Point) :
                        millerFunction W P (m + n) R = millerFunction W P m R * millerFunction W P n R * lineFunctionG W (m • P) (n • P) R

                        Additivity in the index (Lemma 23.24(ii)): f_{m+n,P} = f_{m,P} · f_{n,P} · G_{mP, nP}.

                        theorem WeilPairing.millerFunction_mul {F : Type u_2} [Field F] [DecidableEq F] (W : WeierstrassCurve.Affine F) (P : W.Point) (m n : ℤ) (R : W.Point) :
                        millerFunction W P (m * n) R = millerFunction W P m R ^ n * millerFunction W (m • P) n R

                        Multiplicativity in the index (Lemma 23.24(iii)): f_{mn,P} = f_{m,P}^n · f_{n, mP}.

                        theorem WeilPairing.millerFunction_mul' {F : Type u_2} [Field F] [DecidableEq F] (W : WeierstrassCurve.Affine F) (P : W.Point) (m n : ℤ) (R : W.Point) :
                        millerFunction W P (m * n) R = millerFunction W P n R ^ m * millerFunction W (n • P) m R

                        The symmetric form of Lemma 23.24(iii): f_{mn,P} = f_{n,P}^m · f_{m, nP}.

                        theorem WeilPairing.millerFunction_divisor_deg_zero {F : Type u_2} [Field F] [DecidableEq F] (W : WeierstrassCurve.Affine F) (P : W.Point) (n : ℤ) :
                        ((millerFunctionDivisor W P n).sum fun (x : W.Point) (k : ℤ) => k) = 0

                        The divisor n[P] - (n-1)[0] - [nP] has degree zero.

                        theorem WeilPairing.millerFunction_double {F : Type u_2} [Field F] [DecidableEq F] (W : WeierstrassCurve.Affine F) (P : W.Point) (n : ℤ) (R : W.Point) :
                        millerFunction W P (n + n) R = millerFunction W P n R * millerFunction W P n R * lineFunctionG W (n • P) (n • P) R

                        Doubling formula for the Miller function: f_{2n,P} = f_{n,P}² · G_{nP, nP}. Specialization of millerFunction_add.

                        theorem WeilPairing.millerFunction_succ_int {F : Type u_2} [Field F] [DecidableEq F] (W : WeierstrassCurve.Affine F) (P : W.Point) (n : ℤ) (R : W.Point) :
                        millerFunction W P (n + 1) R = millerFunction W P n R * millerFunction W P 1 R * lineFunctionG W (n • P) (1 • P) R

                        Adding one to the integer index of the Miller function: f_{n+1,P} = f_{n,P} · f_{1,P} · G_{nP, P}.

                        theorem WeilPairing.millerFunction_sq {F : Type u_2} [Field F] [DecidableEq F] (W : WeierstrassCurve.Affine F) (P : W.Point) (n : ℤ) (R : W.Point) :
                        millerFunction W P (n * n) R = millerFunction W P n R ^ n * millerFunction W (n • P) n R

                        Squaring formula for the Miller function: f_{n²,P} = f_{n,P}^n · f_{n, nP}. Specialization of millerFunction_mul.

                        def WeilPairing.muN (N : ℕ) (F : Type u_2) [CommMonoid F] :

                        The group μ_N(F) of N-th roots of unity inside Fˣ.

                        Instances For
                          noncomputable def WeilPairing.weilPairingVal {F : Type u_3} [Field F] [DecidableEq F] (W : WeierstrassCurve.Affine F) (N : ℕ) (P Q T : W.Point) :

                          The raw Weil pairing value (Lemma 23.26): e_n(P, Q) = f_{n,Q}(T) · f_{n,P}(Q - T) / (f_{n,P}(-T) · f_{n,Q}(P + T)) for an auxiliary point T.

                          Instances For
                            theorem WeilPairing.weilPairingVal_mem_muN {F : Type u_3} [Field F] [DecidableEq F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] (N : ℕ) (hN : 0 < N) (hchar : ¬ringChar F ∣ N) (P Q : ↥(W.torsionSubgroup ↑N)) (T : W.Point) (hT_ne_zero : T ≠ 0) (hT_ne_Q : T ≠ ↑Q) (hT_ne_negP : T ≠ -↑P) (hT_ne_QsubP : T ≠ ↑Q - ↑P) :
                            weilPairingVal W N (↑P) (↑Q) T ∈ muN N F

                            The raw Weil pairing value weilPairingVal W N P Q T lies in μ_N(F) for P, Q ∈ E[N] when T avoids the forbidden points {0, Q, -P, Q - P} (consequence of Lemma 23.21).

                            theorem WeilPairing.weilPairingVal_indep_T {F : Type u_3} [Field F] [DecidableEq F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] (N : ℕ) (hN : 0 < N) (hchar : ¬ringChar F ∣ N) (P Q : ↥(W.torsionSubgroup ↑N)) (T₁ T₂ : W.Point) (hT₁_ne_zero : T₁ ≠ 0) (hT₁_ne_Q : T₁ ≠ ↑Q) (hT₁_ne_negP : T₁ ≠ -↑P) (hT₁_ne_QsubP : T₁ ≠ ↑Q - ↑P) (hT₂_ne_zero : T₂ ≠ 0) (hT₂_ne_Q : T₂ ≠ ↑Q) (hT₂_ne_negP : T₂ ≠ -↑P) (hT₂_ne_QsubP : T₂ ≠ ↑Q - ↑P) :
                            weilPairingVal W N (↑P) (↑Q) T₁ = weilPairingVal W N (↑P) (↑Q) T₂

                            The Weil pairing value weilPairingVal W N P Q T does not depend on the choice of valid auxiliary point T (Lemma 23.21).

                            theorem WeilPairing.exists_valid_T {F : Type u_3} [Field F] [DecidableEq F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] (N : ℕ) (hN : 0 < N) (hchar : ¬ringChar F ∣ N) (P Q : ↥(W.torsionSubgroup ↑N)) :
                            ∃ (T : W.Point), T ≠ 0 ∧ T ≠ ↑Q ∧ T ≠ -↑P ∧ T ≠ ↑Q - ↑P

                            Existence of a valid auxiliary point T for the Weil pairing: there is some T avoiding the four forbidden points {0, Q, -P, Q - P}.

                            noncomputable def WeilPairing.weilPairing {F : Type u_3} [Field F] [DecidableEq F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] (N : ℕ) (hN : 0 < N) (hchar : ¬ringChar F ∣ N) :
                            ↥(W.torsionSubgroup ↑N) → ↥(W.torsionSubgroup ↑N) → ↥(muN N F)

                            The Weil pairing e_N : E[N] × E[N] → μ_N(F) as a function valued in μ_N(F), obtained by choosing a valid auxiliary T and packaging the resulting unit.

                            Instances For
                              theorem WeilPairing.millerFunction_compose_translate {F : Type u_3} [Field F] [DecidableEq F] (W : WeierstrassCurve.Affine F) (P : W.Point) (n : ℤ) (hn : n • P = 0) (T Q : W.Point) :
                              millerFunction W P n (Q - T) * (millerFunction W P n (-T))⁻¹ = functionEvalAtDivisor (fun (R : W.Point) => millerFunction W P n (R - T)) (Finsupp.single Q 1 - Finsupp.single 0 1)

                              For an N-torsion point P, the ratio f_{n,P}(Q - T) / f_{n,P}(-T) equals the evaluation of R ↦ f_{n,P}(R - T) at the divisor [Q] - [0].

                              theorem WeilPairing.weilPairing_millerFunction {F : Type u_3} [Field F] [DecidableEq F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] (N : ℕ) (hN : 0 < N) (hchar : ¬ringChar F ∣ N) (P Q : ↥(W.torsionSubgroup ↑N)) (T : W.Point) (hT_ne_zero : T ≠ 0) (hT_ne_Q : T ≠ ↑Q) (hT_ne_negP : T ≠ -↑P) (hT_ne_QsubP : T ≠ ↑Q - ↑P) :
                              ↑(weilPairing W N hN hchar P Q) = millerFunction W (↑Q) (↑N) T * millerFunction W (↑P) (↑N) (↑Q - T) * (millerFunction W (↑P) (↑N) (-T) * millerFunction W (↑Q) (↑N) (↑P + T))⁻¹

                              The value of weilPairing W N hN hchar P Q as a unit Fˣ equals the explicit Miller-function formula for any valid auxiliary point T (Lemma 23.26).

                              theorem WeilPairing.millerFunction_simplification_identity {F : Type u_3} [Field F] [DecidableEq F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] (N : ℕ) (hN : 1 < N) (hchar : ¬ringChar F ∣ N) (P Q : ↥(W.torsionSubgroup ↑N)) (hPQ : ↑P ≠ ↑Q) :
                              ∃ (T : W.Point), T ≠ 0 ∧ T ≠ ↑Q ∧ T ≠ -↑P ∧ T ≠ ↑Q - ↑P ∧ millerFunction W (↑Q) (↑N) T * millerFunction W (↑P) (↑N) (↑Q - T) * (millerFunction W (↑P) (↑N) (-T) * millerFunction W (↑Q) (↑N) (↑P + T))⁻¹ = (-1) ^ N * (millerFunction W ↑P ↑N ↑Q * (millerFunction W ↑Q ↑N ↑P)⁻¹)

                              Existence of an auxiliary point T realizing the simplification of the Weil pairing to the Corollary 23.27 form (-1)^N · f_{N,P}(Q) / f_{N,Q}(P) for distinct N-torsion points P ≠ Q.

                              theorem WeilPairing.weilPairing_millerFunction_simplified {F : Type u_3} [Field F] [DecidableEq F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] (N : ℕ) (hN : 1 < N) (hchar : ¬ringChar F ∣ N) (P Q : ↥(W.torsionSubgroup ↑N)) (hPQ : ↑P ≠ ↑Q) :
                              ↑(weilPairing W N ⋯ hchar P Q) = (-1) ^ N * (millerFunction W ↑P ↑N ↑Q * (millerFunction W ↑Q ↑N ↑P)⁻¹)

                              Corollary 23.27: for distinct N-torsion points P ≠ Q, e_N(P, Q) = (-1)^N · f_{N,P}(Q) / f_{N,Q}(P).

                              def WeilPairing.weilPairingDiv {P : Type u_3} [DecidableEq P] {k : Type u_4} [CommGroup k] (f₁ f₂ : P → k) (D₁ D₂ : P →₀ ℤ) :
                              k

                              Divisor-level Weil pairing (Definition 23.19): given functions f₁, f₂ representing the n-torsion of the divisors D₁, D₂ (i.e., div fᵢ = n · Dᵢ), define e_n(D₁, D₂) := f₁(D₂) / f₂(D₁).

                              Instances For
                                theorem WeilPairing.weilPairingDiv_add_div_left {P : Type u_3} [DecidableEq P] {k : Type u_4} [CommGroup k] (Φ : CurveDiv.FunctionFieldDiv P) (evalAt : Φ.F → P → k) (n : ℤ) (f₁ f₂ : P → k) (D₁ D₂ : P →₀ ℤ) (g : Additive Φ.F) (hD₁_D₂_disjoint : Disjoint D₁.support D₂.support) (hg_D₁_disjoint : Disjoint (Φ.divMap g).support D₁.support) (hg_D₂_disjoint : Disjoint (Φ.divMap g).support D₂.support) :
                                weilPairingDiv (fun (p : P) => f₁ p * evalAt (Additive.toMul g) p ^ n) f₂ (D₁ + Φ.divMap g) D₂ = weilPairingDiv f₁ f₂ D₁ D₂

                                Invariance of the divisor-level Weil pairing under adding a principal divisor on the left: modifying f₁ by a function g and adjusting D₁ by div g does not change the value (Lemma 23.21).

                                theorem WeilPairing.weilPairingDiv_add_div_right {P : Type u_3} [DecidableEq P] {k : Type u_4} [CommGroup k] (Φ : CurveDiv.FunctionFieldDiv P) (evalAt : Φ.F → P → k) (n : ℤ) (f₁ f₂ : P → k) (D₁ D₂ : P →₀ ℤ) (g : Additive Φ.F) (hD₁_D₂_disjoint : Disjoint D₁.support D₂.support) (hg_D₁_disjoint : Disjoint (Φ.divMap g).support D₁.support) (hg_D₂_disjoint : Disjoint (Φ.divMap g).support D₂.support) :
                                weilPairingDiv f₁ (fun (p : P) => f₂ p * evalAt (Additive.toMul g) p ^ n) D₁ (D₂ + Φ.divMap g) = weilPairingDiv f₁ f₂ D₁ D₂

                                Invariance of the divisor-level Weil pairing under adding a principal divisor on the right (Lemma 23.21).

                                theorem WeilPairing.functionEvalAtDivisor_zsmul {P : Type u_3} [DecidableEq P] {k : Type u_4} [CommGroup k] (f : P → k) (n : ℤ) (D : P →₀ ℤ) :

                                Scaling a divisor by an integer n exponentiates the evaluation: f(n • D) = f(D)^n.

                                theorem WeilPairing.weilPairingDiv_pow_eq_one {P : Type u_3} [DecidableEq P] {k : Type u_4} [CommGroup k] (Φ : CurveDiv.FunctionFieldDiv P) (evalAt : Φ.F → P → k) (n : ℤ) (f₁ f₂ : Additive Φ.F) (D₁ D₂ : P →₀ ℤ) (hf₁ : Φ.divMap f₁ = n • D₁) (hf₂ : Φ.divMap f₂ = n • D₂) (hdisjoint : Disjoint D₁.support D₂.support) (hf₁_D₂ : Disjoint (Φ.divMap f₁).support D₂.support) (hf₂_D₁ : Disjoint (Φ.divMap f₂).support D₁.support) :
                                weilPairingDiv (evalAt (Additive.toMul f₁)) (evalAt (Additive.toMul f₂)) D₁ D₂ ^ n = 1

                                The divisor-level Weil pairing raised to the power n is trivial when div fᵢ = n · Dᵢ, i.e., it lies in μ_n (key step in Lemma 23.21).

                                theorem WeilPairing.weilPairingDiv_alternating {P : Type u_3} [DecidableEq P] {k : Type u_4} [CommGroup k] (f₁ f₂ : P → k) (D₁ D₂ : P →₀ ℤ) :
                                weilPairingDiv f₁ f₂ D₁ D₂ * weilPairingDiv f₂ f₁ D₂ D₁ = 1

                                The divisor-level Weil pairing is alternating: e_n(D₁, D₂) · e_n(D₂, D₁) = 1.

                                theorem WeilPairing.weilPairingDiv_alternating_inv {P : Type u_3} [DecidableEq P] {k : Type u_4} [CommGroup k] (f₁ f₂ : P → k) (D₁ D₂ : P →₀ ℤ) :
                                weilPairingDiv f₁ f₂ D₁ D₂ = (weilPairingDiv f₂ f₁ D₂ D₁)⁻¹

                                Inverse form of the alternating property: e_n(D₁, D₂) = e_n(D₂, D₁)⁻¹.

                                theorem WeilPairing.weilPairing_bilinear_left {F : Type u_3} [Field F] [DecidableEq F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] (N : ℕ) (hN : 0 < N) (hchar : ¬ringChar F ∣ N) (P Q R : ↥(W.torsionSubgroup ↑N)) :
                                weilPairing W N hN hchar (P + Q) R = weilPairing W N hN hchar P R * weilPairing W N hN hchar Q R

                                Bilinearity of the Weil pairing in the first argument (Theorem 23.29): e_N(P + Q, R) = e_N(P, R) · e_N(Q, R).

                                theorem WeilPairing.weilPairing_alternating {F : Type u_3} [Field F] [DecidableEq F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] (N : ℕ) (hN : 0 < N) (hchar : ¬ringChar F ∣ N) (P Q : ↥(W.torsionSubgroup ↑N)) :
                                weilPairing W N hN hchar P Q * weilPairing W N hN hchar Q P = 1

                                The Weil pairing is alternating (Theorem 23.29): e_N(P, Q) · e_N(Q, P) = 1.

                                theorem WeilPairing.weilPairing_alternating_inv {F : Type u_3} [Field F] [DecidableEq F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] (N : ℕ) (hN : 0 < N) (hchar : ¬ringChar F ∣ N) (P Q : ↥(W.torsionSubgroup ↑N)) :
                                weilPairing W N hN hchar P Q = (weilPairing W N hN hchar Q P)⁻¹

                                Inverse form of the alternating property: e_N(P, Q) = e_N(Q, P)⁻¹.

                                theorem WeilPairing.weilPairing_bilinear_right {F : Type u_3} [Field F] [DecidableEq F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] (N : ℕ) (hN : 0 < N) (hchar : ¬ringChar F ∣ N) (P Q R : ↥(W.torsionSubgroup ↑N)) :
                                weilPairing W N hN hchar P (Q + R) = weilPairing W N hN hchar P Q * weilPairing W N hN hchar P R

                                Bilinearity of the Weil pairing in the second argument (Theorem 23.29): e_N(P, Q + R) = e_N(P, Q) · e_N(P, R). Derived from weilPairing_bilinear_left via the alternating property.

                                theorem WeilPairing.weilPairing_self {F : Type u_3} [Field F] [DecidableEq F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] (N : ℕ) (hN : 0 < N) (hchar : ¬ringChar F ∣ N) (P : ↥(W.torsionSubgroup ↑N)) :
                                weilPairing W N hN hchar P P = 1

                                The Weil pairing is trivial on the diagonal (Theorem 23.29): e_N(P, P) = 1.

                                theorem WeilPairing.weilPairing_nondegenerate {F : Type u_3} [Field F] [DecidableEq F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] (N : ℕ) (hN : 0 < N) (hchar : ¬ringChar F ∣ N) (P : ↥(W.torsionSubgroup ↑N)) (hP : P ≠ 0) :
                                ∃ (Q : ↥(W.torsionSubgroup ↑N)), weilPairing W N hN hchar P Q ≠ 1

                                Non-degeneracy of the Weil pairing (Theorem 23.29): if P ≠ 0 then there exists Q ∈ E[N] with e_N(P, Q) ≠ 1.

                                theorem WeilPairing.weilPairing_compatibility {F : Type u_3} [Field F] [DecidableEq F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] (M N : ℕ) (hMN : 0 < M * N) (hN : 0 < N) (hcharMN : ¬ringChar F ∣ M * N) (hcharN : ¬ringChar F ∣ N) (P : ↥(W.torsionSubgroup ↑(M * N))) (Q : ↥(W.torsionSubgroup ↑N)) (hQ_MN : ↑Q ∈ W.torsionSubgroup ↑(M * N)) (hMP : ↑M • ↑P ∈ W.torsionSubgroup ↑N) :
                                ↑(weilPairing W (M * N) hMN hcharMN P ⟨↑Q, hQ_MN⟩) = ↑(weilPairing W N hN hcharN ⟨↑M • ↑P, hMP⟩ Q)

                                Compatibility of the Weil pairing across different N (Theorem 23.29): e_{MN}(P, Q) = e_N(M·P, Q) for P ∈ E[MN] and Q ∈ E[N].

                                noncomputable def WeilPairing.galoisActionOnTorsion {F : Type u_3} [Field F] [DecidableEq F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] (N : ℕ) (hN : 0 < N) (hchar : ¬ringChar F ∣ N) (σ : F ≃+* F) :
                                ↥(W.torsionSubgroup ↑N) →+ ↥(W.torsionSubgroup ↑N)

                                A Galois automorphism σ : F ≃+* F induces an additive automorphism of the N-torsion subgroup E[N].

                                Instances For
                                  noncomputable def WeilPairing.galoisActionOnMuN {F : Type u_3} [Field F] [DecidableEq F] (N : ℕ) (_hN : 0 < N) (_hchar : ¬ringChar F ∣ N) (σ : F ≃+* F) :
                                  ↥(muN N F) →* ↥(muN N F)

                                  A Galois automorphism σ : F ≃+* F induces a multiplicative automorphism of μ_N(F) ⊆ Fˣ.

                                  Instances For
                                    theorem WeilPairing.weilPairing_galois_equivariant {F : Type u_3} [Field F] [DecidableEq F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] (N : ℕ) (hN : 0 < N) (hchar : ¬ringChar F ∣ N) (σ : F ≃+* F) (P Q : ↥(W.torsionSubgroup ↑N)) :
                                    weilPairing W N hN hchar ((galoisActionOnTorsion W N hN hchar σ) P) ((galoisActionOnTorsion W N hN hchar σ) Q) = (galoisActionOnMuN N hN hchar σ) (weilPairing W N hN hchar P Q)

                                    Galois-equivariance of the Weil pairing (Theorem 23.29): e_N(σ·P, σ·Q) = σ·e_N(P, Q) for every σ ∈ Gal(F̄/F).

                                    theorem WeilPairing.weilPairing_endomorphism {F : Type u_3} [Field F] [DecidableEq F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] (N : ℕ) (hN : 0 < N) (hchar : ¬ringChar F ∣ N) (α : Isogeny W W) (P Q : ↥(W.torsionSubgroup ↑N)) (hαP : α.toAddMonoidHom ↑P ∈ W.torsionSubgroup ↑N) (hαQ : α.toAddMonoidHom ↑Q ∈ W.torsionSubgroup ↑N) :
                                    weilPairing W N hN hchar ⟨α.toAddMonoidHom ↑P, hαP⟩ ⟨α.toAddMonoidHom ↑Q, hαQ⟩ = weilPairing W N hN hchar P Q ^ ↑α.degree

                                    Behavior of the Weil pairing under endomorphisms (Theorem 23.29): e_N(α(P), α(Q)) = e_N(P, Q)^{deg α} for every isogeny/endomorphism α.

                                    theorem WeilPairing.weilPairing_surjective {F : Type u_3} [Field F] [DecidableEq F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] (N : ℕ) (hN : 0 < N) (hchar : ¬ringChar F ∣ N) (P : ↥(W.torsionSubgroup ↑N)) (ζ : ↥(muN N F)) (hζ : orderOf ↑ζ ∣ addOrderOf ↑P) :
                                    ∃ (Q : ↥(W.torsionSubgroup ↑N)), ↑(weilPairing W N hN hchar P Q) = ↑ζ

                                    Surjectivity of the Weil pairing onto μ_r ⊆ μ_N for r = |P| (Theorem 23.29): every root of unity ζ whose order divides |P| is hit by some Q ∈ E[N].

                                    theorem WeilPairing.weilPairing_order_dvd {F : Type u_3} [Field F] [DecidableEq F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] (N : ℕ) (hN : 0 < N) (hchar : ¬ringChar F ∣ N) (P Q : ↥(W.torsionSubgroup ↑N)) :
                                    orderOf ↑(weilPairing W N hN hchar P Q) ∣ addOrderOf ↑P

                                    The order of e_N(P, Q) divides the additive order of P.

                                    theorem WeilPairing.weilPairing_zero_left {F : Type u_3} [Field F] [DecidableEq F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] (N : ℕ) (hN : 0 < N) (hchar : ¬ringChar F ∣ N) (Q : ↥(W.torsionSubgroup ↑N)) :
                                    weilPairing W N hN hchar 0 Q = 1

                                    The Weil pairing vanishes when the first argument is 0: e_N(0, Q) = 1. Consequence of bilinearity.

                                    theorem WeilPairing.weilPairing_zero_right {F : Type u_3} [Field F] [DecidableEq F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] (N : ℕ) (hN : 0 < N) (hchar : ¬ringChar F ∣ N) (P : ↥(W.torsionSubgroup ↑N)) :
                                    weilPairing W N hN hchar P 0 = 1

                                    The Weil pairing vanishes when the second argument is 0: e_N(P, 0) = 1.

                                    noncomputable def WeilPairing.NTorsionContainedIn {K : Type u_3} [Field K] (W : WeierstrassCurve.Affine K) (n : ℕ) (L : Type u_4) [Field L] [Algebra K L] :

                                    The predicate "the n-torsion E[n] is contained in E(L)" for a field extension L/K (used to define the embedding degree, Definition 23.32).

                                    Instances For

                                      k is the embedding degree of W with respect to n (Definition 23.32): there exists a field extension L/K of degree k containing E[n], and k is the minimal such degree.

                                      Instances For
                                        def WeilPairing.IsPairingFriendly {K : Type u_3} [Field K] (W : WeierstrassCurve.Affine K) (n k bound : ℕ) :

                                        W is pairing-friendly for parameters (n, k, bound) if k is its embedding degree with respect to n and k ≤ bound (small embedding degree makes the Tate pairing efficiently computable in cryptographic applications).

                                        Instances For
                                          theorem WeilPairing.pow_div_mem_rootsOfUnity {G : Type u_3} [CommGroup G] [Fintype G] (u : G) (n : ℕ) (hn : n ∣ Fintype.card G) :
                                          (u ^ (Fintype.card G / n)) ^ n = 1

                                          For any element u of a finite commutative group G and any divisor n of |G|, the power (u ^ (|G| / n))^n = 1.

                                          noncomputable def WeilPairing.tatePairing {F : Type u_3} [Field F] [DecidableEq F] [Fintype F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] (n : ℕ) (hn : 2 < n) (hchar : ¬ringChar F ∣ n) (k : ℕ) (hk : IsEmbeddingDegree W n k) (hdvd : n ∣ Fintype.card F ^ k - 1) :
                                          ↥(W.torsionSubgroup ↑n) → ↥(W.torsionSubgroup ↑n) → ↥(muN n F)

                                          The (modified) Tate pairing t_n : E[n] × E[n] → μ_n (Definition 23.34), defined on a finite field F with embedding degree k: t_n(P, Q) := (f_{n,P}(Q) / f_{n,P}(0))^{(|F|^k - 1)/n}.

                                          Instances For

                                            The Frobenius endomorphism π_E : E(F̄) → E(F̄) on a finite-field elliptic curve, packaged as an additive group homomorphism on W.Point.

                                            Instances For

                                              The Frobenius endomorphism is surjective on the group of points.

                                              The Frobenius endomorphism as an Isogeny W W of degree |F|.

                                              Instances For

                                                The degree of the Frobenius isogeny equals |F|.

                                                The trace of Frobenius a_q := q + 1 - #E(F_q) for an elliptic curve over a finite field.

                                                Instances For

                                                  Counting formula: #E(F_q) = q + 1 - tr(π_E).

                                                  theorem WeilPairing.frobenius_charPoly_factors_on_torsion {F : Type u_4} [Field F] [DecidableEq F] [Fintype F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] [Fintype W.Point] (n : ℕ) (hn_prime : Nat.Prime n) (hn_cop : n.Coprime (Fintype.card F)) (hn_dvd : ↑n ∣ ↑(Fintype.card W.Point)) (P : W.Point) (hP : P ∈ W.torsionSubgroup ↑n) :

                                                  The characteristic polynomial of Frobenius (π - 1)(π - q) = 0 factors on the n-torsion when n is prime and divides #E(F_q) (key input to Lemma 23.33).

                                                  theorem WeilPairing.torsion_contained_if_q_cong_one {F : Type u_4} [Field F] [DecidableEq F] [Fintype F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] [Fintype W.Point] (n : ℕ) (hn_prime : Nat.Prime n) (hn_cop : n.Coprime (Fintype.card F)) (hn_dvd : ↑n ∣ ↑(Fintype.card W.Point)) (hq_cong : ↑(Fintype.card F) ≡ 1 [ZMOD ↑n]) (P : W.Point) (hP : P ∈ W.torsionSubgroup ↑n) :

                                                  If q ≡ 1 (mod n) then Frobenius acts trivially on every n-torsion point — equivalently, E[n] ⊆ E(F_q) (case of Lemma 23.33).

                                                  theorem WeilPairing.torsion_eigenspace_decomposition {F : Type u_4} [Field F] [DecidableEq F] [Fintype F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] [Fintype W.Point] (n : ℕ) (hn_prime : Nat.Prime n) (hn_cop : n.Coprime (Fintype.card F)) (hn_dvd : ↑n ∣ ↑(Fintype.card W.Point)) (hq_not_cong : ¬↑(Fintype.card F) ≡ 1 [ZMOD ↑n]) (P : W.Point) (hP : P ∈ W.torsionSubgroup ↑n) :
                                                  ∃ (P₁ : W.Point) (Pq : W.Point), P₁ ∈ W.torsionSubgroup ↑n ∧ Pq ∈ W.torsionSubgroup ↑n ∧ P = P₁ + Pq ∧ (frobeniusIsogeny W).toAddMonoidHom P₁ = P₁ ∧ (frobeniusIsogeny W).toAddMonoidHom Pq = ↑(Fintype.card F) • Pq

                                                  Eigenspace decomposition of E[n] under Frobenius when q ≢ 1 (mod n): every n-torsion point P writes as P = P₁ + P_q with π(P₁) = P₁ and π(P_q) = q · P_q (Lemma 23.33: E[n] ≅ ker(π_n - 1) ⊕ ker(π_n - q)).

                                                  theorem WeilPairing.nTorsionContainedIn_implies_dvd {F : Type u_4} [Field F] [DecidableEq F] [Fintype F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] [Fintype W.Point] (n : ℕ) (hn_prime : Nat.Prime n) (hn_cop : n.Coprime (Fintype.card F)) (hn_dvd : ↑n ∣ ↑(Fintype.card W.Point)) (L : Type u_5) [Field L] [Algebra F L] (hL : NTorsionContainedIn W n L) :

                                                  If E[n] ⊆ E(L) for a finite extension L/F, then [L : F] > 0 and n ∣ |F|^[L:F] - 1 (forward direction of Lemma 23.33).

                                                  theorem WeilPairing.dvd_implies_nTorsionContainedIn {F : Type u_4} [Field F] [DecidableEq F] [Fintype F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] [Fintype W.Point] (n : ℕ) (hn_prime : Nat.Prime n) (hn_cop : n.Coprime (Fintype.card F)) (hn_dvd : ↑n ∣ ↑(Fintype.card W.Point)) (k : ℕ) (hk_pos : 0 < k) (hk_dvd : n ∣ Fintype.card F ^ k - 1) :
                                                  ∃ (L : Type u_5) (x : Field L) (x_1 : Algebra F L), NTorsionContainedIn W n L ∧ Module.finrank F L = k

                                                  Converse: if n ∣ |F|^k - 1 then there exists a degree-k extension L/F containing E[n] (reverse direction of Lemma 23.33).

                                                  theorem WeilPairing.embeddingDegree_is_multiplicativeOrder_of_q_mod_n {F : Type u_4} [Field F] [DecidableEq F] [Fintype F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] [Fintype W.Point] (n : ℕ) (hn_prime : Nat.Prime n) (hn_cop : n.Coprime (Fintype.card F)) (hn_dvd : ↑n ∣ ↑(Fintype.card W.Point)) (k : ℕ) (hk_pos : 0 < k) (hk_dvd : n ∣ Fintype.card F ^ k - 1) (hk_least : ∀ (j : ℕ), 0 < j → j < k → ¬n ∣ Fintype.card F ^ j - 1) :

                                                  Lemma 23.33: the embedding degree of E/F_q with respect to a prime n dividing #E(F_q) (coprime to q) equals the multiplicative order of q modulo n.

                                                  @[irreducible]

                                                  The Miller "double-and-add" algorithm: efficient evaluation of f_{n,P}(Q) using O(log n) field operations (Corollary 23.25). At each step we either square the accumulator (via the line G_{mP, mP}) or square and multiply by G_{2mP, P}.

                                                  Instances For

                                                    Correctness of the Miller double-and-add algorithm: millerDoubleAndAdd W P Q n = f_{n,P}(Q).

                                                    @[irreducible]

                                                    Operation cost of the Miller double-and-add algorithm: roughly log₂ n doublings plus a few extra operations per "add" step.

                                                    Instances For

                                                      Logarithmic bound on the Miller evaluation cost: millerEvalCost n ≤ 2 log₂ n + 2, giving the O(log n) complexity of Corollary 23.25.

                                                      theorem WeilPairing.muN_contained_if_torsion_contained {K : Type u_3} [Field K] (W : WeierstrassCurve.Affine K) (n : ℕ) (hn : 0 < n) (hchar : ¬ringChar K ∣ n) (L : Type u_4) [Field L] [Algebra K L] (hL : NTorsionContainedIn W n L) (ζ : Lˣ) :
                                                      ζ ∈ rootsOfUnity n L → ↑ζ ∈ (algebraMap K L).range

                                                      Galois-equivariance refinement (Corollary 23.30): if E[n] ⊆ E(L) then every n-th root of unity in L actually lies in (the image of) K.

                                                      theorem WeilPairing.corollary_23_30_finite_field {F : Type u_3} [Field F] [DecidableEq F] [Fintype F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] [Fintype W.Point] (n : ℕ) (hn_prime : Nat.Prime n) (hn_cop : n.Coprime (Fintype.card F)) (hn_dvd : ↑n ∣ ↑(Fintype.card W.Point)) (hcontained : NTorsionContainedIn W n F) :

                                                      Corollary 23.30 over finite fields: if E[n] ⊆ E(F_q) then n ∣ q - 1.

                                                      theorem WeilPairing.corollary_23_30_finite_field_cong {F : Type u_3} [Field F] [DecidableEq F] [Fintype F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] [Fintype W.Point] (n : ℕ) (hn_prime : Nat.Prime n) (hn_cop : n.Coprime (Fintype.card F)) (hn_dvd : ↑n ∣ ↑(Fintype.card W.Point)) (hcontained : NTorsionContainedIn W n F) :

                                                      Congruence form of Corollary 23.30: if E[n] ⊆ E(F_q) then q ≡ 1 (mod n).

                                                      theorem WeilPairing.corollary_23_31_full_torsion {F : Type u_4} [Field F] [DecidableEq F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] (N : ℕ) (hN : 0 < N) (hchar : ¬ringChar F ∣ N) (P Q : ↥(W.torsionSubgroup ↑N)) (hP_order : addOrderOf ↑P = N) (hPQ_generate : ∀ R ∈ W.torsionSubgroup ↑N, R ∈ AddSubgroup.closure {↑P, ↑Q}) :
                                                      orderOf ↑(weilPairing W N hN hchar P Q) = N

                                                      Corollary 23.31, full-torsion case: if P has additive order N and together with Q generates E[N], then the Weil pairing e_N(P, Q) has order exactly N (so it is a primitive N-th root of unity).

                                                      theorem WeilPairing.corollary_23_31_order_dvd_of_mem_zmultiples {F : Type u_4} [Field F] [DecidableEq F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] (N : ℕ) (hN : 0 < N) (hchar : ¬ringChar F ∣ N) (P Q : ↥(W.torsionSubgroup ↑N)) (hP_order : addOrderOf ↑P = N) (m : ℕ) (hm : 0 < m) (hQ_in_P : ↑m • ↑Q ∈ AddSubgroup.zmultiples ↑P) :
                                                      orderOf ↑(weilPairing W N hN hchar P Q) ∣ m

                                                      Corollary 23.31 (one direction): if m · Q ∈ ⟨P⟩ then the order of e_N(P, Q) divides m.

                                                      theorem WeilPairing.corollary_23_31_mem_zmultiples_of_order_dvd {F : Type u_4} [Field F] [DecidableEq F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] (N : ℕ) (hN : 0 < N) (hchar : ¬ringChar F ∣ N) (P Q : ↥(W.torsionSubgroup ↑N)) (hP_order : addOrderOf ↑P = N) (m : ℕ) (hm : 0 < m) (h_dvd : orderOf ↑(weilPairing W N hN hchar P Q) ∣ m) :

                                                      Corollary 23.31 (other direction): if the order of e_N(P, Q) divides m, then m · Q ∈ ⟨P⟩.

                                                      theorem WeilPairing.corollary_23_31_order_eq_least_m {F : Type u_4} [Field F] [DecidableEq F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] (N : ℕ) (hN : 0 < N) (hchar : ¬ringChar F ∣ N) (P Q : ↥(W.torsionSubgroup ↑N)) (hP_order : addOrderOf ↑P = N) (m : ℕ) (hm : 0 < m) :
                                                      orderOf ↑(weilPairing W N hN hchar P Q) ∣ m ↔ ↑m • ↑Q ∈ AddSubgroup.zmultiples ↑P

                                                      Corollary 23.31 (equivalent form): orderOf e_N(P, Q) ∣ m iff m · Q ∈ ⟨P⟩. The order of e_N(P, Q) equals the least integer m for which m · Q ∈ ⟨P⟩.

                                                      theorem WeilPairing.corollary_23_31_weilPairing_eq_one_iff_mem_zmultiples {F : Type u_4} [Field F] [DecidableEq F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] (N : ℕ) (hN : 0 < N) (hchar : ¬ringChar F ∣ N) (P Q : ↥(W.torsionSubgroup ↑N)) (hP_order : addOrderOf ↑P = N) :
                                                      ↑(weilPairing W N hN hchar P Q) = 1 ↔ ↑Q ∈ AddSubgroup.zmultiples ↑P

                                                      Corollary 23.31 specialized to m = 1: e_N(P, Q) = 1 iff Q ∈ ⟨P⟩.

                                                      The predicate "the subgroup generated by P and Q is cyclic": there exists a single generator R whose multiples coincide with ⟨P, Q⟩.

                                                      Instances For
                                                        theorem WeilPairing.corollary_23_31_cyclic_of_weilPairing_eq_one {F : Type u_4} [Field F] [DecidableEq F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] (N : ℕ) (hN : 0 < N) (hchar : ¬ringChar F ∣ N) (P Q : ↥(W.torsionSubgroup ↑N)) (hP_order : addOrderOf ↑P = N) (h_eq_one : ↑(weilPairing W N hN hchar P Q) = 1) :

                                                        Corollary 23.31 (one direction of the cyclic characterization): if e_N(P, Q) = 1 then ⟨P, Q⟩ is cyclic.

                                                        theorem WeilPairing.corollary_23_31_weilPairing_eq_one_of_cyclic {F : Type u_4} [Field F] [DecidableEq F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] (N : ℕ) (hN : 0 < N) (hchar : ¬ringChar F ∣ N) (P Q : ↥(W.torsionSubgroup ↑N)) (hP_order : addOrderOf ↑P = N) (hcyclic : IsSubgroupCyclicPair ↑P ↑Q) :
                                                        ↑(weilPairing W N hN hchar P Q) = 1

                                                        Corollary 23.31 (other direction): if ⟨P, Q⟩ is cyclic then e_N(P, Q) = 1.

                                                        theorem WeilPairing.corollary_23_31_weilPairing_eq_one_iff_cyclic {F : Type u_4} [Field F] [DecidableEq F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] (N : ℕ) (hN : 0 < N) (hchar : ¬ringChar F ∣ N) (P Q : ↥(W.torsionSubgroup ↑N)) (hP_order : addOrderOf ↑P = N) :
                                                        ↑(weilPairing W N hN hchar P Q) = 1 ↔ IsSubgroupCyclicPair ↑P ↑Q

                                                        Corollary 23.31, equivalence form: e_N(P, Q) = 1 iff the subgroup ⟨P, Q⟩ is cyclic.