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
Evaluation at a divisor is multiplicative in the divisor:
f(D₁ + D₂) = f(D₁) · f(D₂).
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).
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
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
The divisor of the line L_{P,Q}, namely [P] + [Q] + [-(P+Q)] - 3[0].
Instances For
The divisor of G_{P,Q}, namely [P] + [Q] - [P+Q] - [0].
Instances For
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
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.
Two divisors D₁, D₂ are linearly equivalent (with respect to a subgroup of principal
divisors PrincE) when D₁ - D₂ ∈ PrincE.
Instances For
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
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
The Miller function at index 0 is the constant function 1.
The Miller function at index 1 is the constant function 1.
Recursive step for the natural-index Miller function:
f_{n+1,P}(R) = f_{n,P}(R) · G_{P, nP}(R) for n ≥ 1.
Relation between the Miller function at -n and at n, for positive natural n.
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)).
Additivity in the index (Lemma 23.24(ii)):
f_{m+n,P} = f_{m,P} · f_{n,P} · G_{mP, nP}.
Multiplicativity in the index (Lemma 23.24(iii)):
f_{mn,P} = f_{m,P}^n · f_{n, mP}.
The symmetric form of Lemma 23.24(iii):
f_{mn,P} = f_{n,P}^m · f_{m, nP}.
The divisor n[P] - (n-1)[0] - [nP] has degree zero.
Doubling formula for the Miller function:
f_{2n,P} = f_{n,P}² · G_{nP, nP}. Specialization of millerFunction_add.
Adding one to the integer index of the Miller function:
f_{n+1,P} = f_{n,P} · f_{1,P} · G_{nP, P}.
Squaring formula for the Miller function:
f_{n²,P} = f_{n,P}^n · f_{n, nP}. Specialization of millerFunction_mul.
The group μ_N(F) of N-th roots of unity inside Fˣ.
Instances For
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
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).
The Weil pairing value weilPairingVal W N P Q T does not depend on the choice of valid
auxiliary point T (Lemma 23.21).
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}.
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
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].
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).
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.
Corollary 23.27: for distinct N-torsion points P ≠ Q,
e_N(P, Q) = (-1)^N · f_{N,P}(Q) / f_{N,Q}(P).
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
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).
Invariance of the divisor-level Weil pairing under adding a principal divisor on the right (Lemma 23.21).
Scaling a divisor by an integer n exponentiates the evaluation:
f(n • D) = f(D)^n.
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).
The divisor-level Weil pairing is alternating: e_n(D₁, D₂) · e_n(D₂, D₁) = 1.
Inverse form of the alternating property:
e_n(D₁, D₂) = e_n(D₂, D₁)⁻¹.
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).
The Weil pairing is alternating (Theorem 23.29):
e_N(P, Q) · e_N(Q, P) = 1.
Inverse form of the alternating property:
e_N(P, Q) = e_N(Q, P)⁻¹.
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.
The Weil pairing is trivial on the diagonal (Theorem 23.29):
e_N(P, P) = 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.
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].
A Galois automorphism σ : F ≃+* F induces an additive automorphism of the N-torsion
subgroup E[N].
Instances For
Galois-equivariance of the Weil pairing (Theorem 23.29):
e_N(σ·P, σ·Q) = σ·e_N(P, Q) for every σ ∈ Gal(F̄/F).
Behavior of the Weil pairing under endomorphisms (Theorem 23.29):
e_N(α(P), α(Q)) = e_N(P, Q)^{deg α} for every isogeny/endomorphism α.
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].
The order of e_N(P, Q) divides the additive order of P.
The Weil pairing vanishes when the first argument is 0:
e_N(0, Q) = 1. Consequence of bilinearity.
The Weil pairing vanishes when the second argument is 0:
e_N(P, 0) = 1.
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
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
For any element u of a finite commutative group G and any divisor n of |G|,
the power (u ^ (|G| / n))^n = 1.
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).
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).
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).
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)).
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).
Converse: if n ∣ |F|^k - 1 then there exists a degree-k extension L/F containing
E[n] (reverse direction of Lemma 23.33).
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.
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).
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.
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.
Corollary 23.30 over finite fields: if E[n] ⊆ E(F_q) then n ∣ q - 1.
Congruence form of Corollary 23.30: if E[n] ⊆ E(F_q) then q ≡ 1 (mod 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).
Corollary 23.31 (one direction): if m · Q ∈ ⟨P⟩ then the order of e_N(P, Q) divides m.
Corollary 23.31 (other direction): if the order of e_N(P, Q) divides m, then
m · Q ∈ ⟨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⟩.
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
Corollary 23.31 (one direction of the cyclic characterization):
if e_N(P, Q) = 1 then ⟨P, Q⟩ is cyclic.
Corollary 23.31 (other direction): if ⟨P, Q⟩ is cyclic then e_N(P, Q) = 1.
Corollary 23.31, equivalence form: e_N(P, Q) = 1 iff the subgroup ⟨P, Q⟩ is cyclic.