Evaluate a low-to-high quotient-coefficient list at a quotient point.
The list [c₀, c₁, ...] denotes c₀ + β * (c₁ + β * (...)). This
proof-facing evaluator is used by quotient-field root-count arguments where
the coefficients already live in F_p[X] / (g).
Equations
Instances For
Evaluating the empty quotient-coefficient list gives zero.
Evaluating a nonempty quotient-coefficient list unfolds one Horner step.
Synthetic quotient coefficients for the divided difference of cs at the
base point α.
If P is represented by cs, this list represents the quotient
(P(T) - P(α)) / (T - α). Its length is one less than the input list, which
is the measure used by root-count induction.
Equations
Instances For
The divided-difference coefficient list of the empty list is empty.
A constant polynomial has empty divided-difference coefficient list.
The divided-difference coefficient recursion peels the constant term and evaluates the remaining tail at the base point.
The synthetic divided-difference coefficient list has one fewer entry.
The synthetic divided-difference coefficient list is strictly shorter for nonempty input.
Evaluate the divided difference of a quotient-coefficient polynomial between
the base point α and target point β.
Equations
Instances For
The divided difference of the empty coefficient list is zero.
A nonconstant divided difference unfolds as a Horner step over the synthetic coefficient tail.
The quotient-coefficient divided difference satisfies the usual identity
P(β) - P(α) = (β - α) * DD(P, α, β).
Evaluate an FpPoly at a quotient element by Horner iteration in the quotient.
The coefficients are embedded as constant quotient classes. This is a
project-side evaluation layer for root-counting arguments over
F_p[X] / (g), without introducing a ring typeclass for the executable
quotient representation.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Stored FpPoly coefficients embedded as quotient constants, in low-to-high
coefficient order.
Equations
- Hex.FpPoly.Quotient.Internal.evalQuotientCoeffs f = List.map (fun (coeff : Hex.ZMod64 p) => Hex.FpPoly.Quotient.reduce (Hex.DensePoly.C coeff)) (Hex.DensePoly.toList f)
Instances For
Evaluating the zero polynomial in the quotient gives zero.
Evaluating a constant polynomial gives the corresponding constant quotient class.
Evaluating the polynomial indeterminate gives the input quotient element.
Quotient evaluation of an FpPoly agrees with the proof-facing
quotient-coefficient evaluator on the embedded stored coefficient list.
FpPoly-specific divided-difference quotient evaluated between α and
β, using the existing executable coefficient representation.
Equations
Instances For
Synthetic quotient coefficients for the FpPoly divided difference at
α.
Equations
Instances For
Evaluating the executable divided difference is the quotient-coefficient evaluator applied to its synthetic coefficient list.
The executable divided-difference coefficient list has one fewer entry than the embedded coefficient list.
The executable divided-difference coefficient list is strictly shorter whenever the embedded input coefficient list is nonempty.
FpPoly quotient evaluation satisfies the divided-difference identity.
If α is a quotient root of f, every value of f factors by
β - α through the executable-coefficient divided difference.
Evaluation of a sum equals the sum of the evaluations.
Evaluation of a difference equals the difference of the evaluations.
Evaluation of a constant multiple equals the reduced constant times the evaluation.
Evaluating monomial n c yields the reduced constant C c times the
n-th power of the evaluation point.
For a monic irreducible positive-degree modulus, the product of two nonzero quotient elements is nonzero.
Left multiplication by a nonzero quotient element is injective on the quotient under an irreducible modulus.
The highest coefficient in a low-to-high quotient coefficient list is nonzero.
This predicate is the syntactic degree witness used by root-count induction:
such a list represents a nonzero quotient-coefficient polynomial of degree
cs.length - 1.
Equations
Instances For
Roots of a quotient-coefficient polynomial inside the canonical quotient enumeration.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Membership in rootsOfCoeffList cs is exactly vanishing of the
quotient-coefficient evaluator.
The quotient-coefficient root list has no duplicate roots.
A nonzero quotient-coefficient polynomial has at most its degree many roots in the duplicate-free quotient enumeration.
The coefficient list is low-to-high, and coeffListTopNonzero cs says the
highest listed coefficient is nonzero, so the degree bound is cs.length - 1.
Direct root-count bound for the canonical elements filter form used by
callers.
Roots of an FpPoly quotient evaluation inside the canonical quotient
enumeration.
Equations
- Hex.FpPoly.Quotient.Internal.rootsOfFpPoly f = List.filter (fun (β : g.Quotient hmonic hg_pos) => decide (Hex.FpPoly.Quotient.eval f β = 0)) Hex.FpPoly.Quotient.Internal.elements
Instances For
Membership in rootsOfFpPoly f is exactly vanishing of quotient
evaluation of f.
The FpPoly quotient-evaluation root list has no duplicate roots.
A nonzero FpPoly has at most f.size - 1 quotient roots in the
duplicate-free quotient enumeration, provided the modulus is irreducible.
Direct root-count bound for the canonical elements filter form used by
callers evaluating an FpPoly in the quotient.
Multiplication by a nonzero quotient element permutes the nonzero
enumeration. The list of nonzero elements multiplied on the left by a is a
permutation of the original nonzero list.
The quotient is nontrivial: 1 and 0 are distinct quotient elements
under a positive-degree modulus.
Product of a list of quotient elements (right fold).
Equations
- Hex.FpPoly.Quotient.Internal.listProd xs = List.foldr (fun (x1 x2 : g.Quotient hmonic hg_pos) => x1 * x2) 1 xs
Instances For
The product of an empty quotient list is one.
The product of a cons list multiplies the head by the product of the tail.
The product of an appended quotient list factors as the product of the two pieces.
The list product is invariant under List.Perm.
Mapping a list by left-multiplication factors out as a power of the multiplier times the original list product.
The product of a list of nonzero quotient elements is nonzero, under a monic irreducible positive-degree modulus.
Finite-field exponent theorem for the quotient: every nonzero quotient
element raised to the cardinality of the nonzero group equals 1.
Frobenius fixed-point theorem for the quotient: every element of the
finite-field quotient F_p[X] / (g) is fixed by raising to the cardinality
p ^ deg(g).
Adding any multiple of the modulus degree to a Frobenius exponent does not change the quotient Frobenius iterate.
If a quotient element is fixed by the nth Frobenius iterate, then it is
fixed by the remainder of n modulo the modulus degree.
If every element of the irreducible quotient is fixed by the nth Frobenius
iterate, then the modulus degree divides n.
This is the quotient-side order theorem used by Rabin soundness: a nonzero
remainder r = n % deg(g) would make every quotient element a root of
T^(p^r) - T, contradicting the root-count bound because the quotient has
p^deg(g) elements.