Add modular polynomial identity verification

src/jacobian/contracts/number_theory.py

@@ -294,6 +294,35 @@ def require_canonical_bounded_polynomial(self) -> Self:
         return self
 
 
+class ModularPolynomialIdentityRequest(ContractModel):
+    """Two bounded sparse integer polynomials compared coefficientwise modulo m."""
+
+    modulus: StrictInt = Field(ge=2, le=_MAX_POLYNOMIAL_RESIDUE_MODULUS)
+    variables: tuple[ResidueVariableName, ...] = Field(
+        min_length=1,
+        max_length=_MAX_RESIDUE_VARIABLES,
+    )
+    left: tuple[ModularPolynomialTerm, ...] = Field(
+        min_length=0,
+        max_length=_MAX_RESIDUE_TERMS,
+    )
+    right: tuple[ModularPolynomialTerm, ...] = Field(
+        min_length=0,
+        max_length=_MAX_RESIDUE_TERMS,
+    )
+
+    @model_validator(mode="after")
+    def require_bounded_polynomials(self) -> Self:
+        if len(self.variables) != len(set(self.variables)):
+            raise ValueError("polynomial variable names must be unique")
+        if any(
+            len(term.exponents) != len(self.variables)
+            for term in (*self.left, *self.right)
+        ):
+            raise ValueError("every term exponent vector must match the variable count")
+        return self
+
+
 class ChineseRemainderRequest(ContractModel):
     """A finite system of integer congruences with parallel residues and moduli."""
 
@@ -475,6 +504,51 @@ class NormalizedModularPolynomialTerm(ContractModel):
     )
 
 
+class ModularPolynomialIdentityResult(ContractModel):
+    """Canonical coefficientwise comparison in a formal polynomial ring."""
+
+    semantics_version: Literal["modular-polynomial-identity.v1"]
+    modulus: StrictInt = Field(ge=2, le=_MAX_POLYNOMIAL_RESIDUE_MODULUS)
+    variable_order: tuple[ResidueVariableName, ...] = Field(
+        min_length=1,
+        max_length=_MAX_RESIDUE_VARIABLES,
+    )
+    normalized_left: tuple[NormalizedModularPolynomialTerm, ...] = Field(
+        min_length=0,
+        max_length=_MAX_RESIDUE_TERMS,
+    )
+    normalized_right: tuple[NormalizedModularPolynomialTerm, ...] = Field(
+        min_length=0,
+        max_length=_MAX_RESIDUE_TERMS,
+    )
+    residual: tuple[NormalizedModularPolynomialTerm, ...] = Field(
+        min_length=0,
+        max_length=_MAX_RESIDUE_TERMS * 2,
+    )
+    identical: StrictBool
+    comparison_scope: Literal["FORMAL_COEFFICIENTWISE_IDENTITY"]
+
+    @model_validator(mode="after")
+    def require_canonical_comparison(self) -> Self:
+        for terms in (
+            self.normalized_left,
+            self.normalized_right,
+            self.residual,
+        ):
+            if any(
+                len(term.exponents) != len(self.variable_order)
+                or term.coefficient >= self.modulus
+                for term in terms
+            ):
+                raise ValueError("normalized terms do not match the result scope")
+            exponents = [term.exponents for term in terms]
+            if exponents != sorted(set(exponents)):
+                raise ValueError("normalized term exponents must be canonical")
+        if self.identical != (not self.residual):
+            raise ValueError("identity decision must match the canonical residual")
+        return self
+
+
 class ModularPolynomialResidueCount(ContractModel):
     """Multiplicity of one reachable residue in the declared assignment table."""
 

src/jacobian/domains/number_theory/checkers.py

@@ -3,6 +3,7 @@
 from jacobian.checker_operations import ExactReplayCheckerDeclaration
 from jacobian.contracts.number_theory import (
     FactorizationRequest,
+    ModularPolynomialIdentityRequest,
     ModularPolynomialResidueImageRequest,
     PowerfulNumberRequest,
 )
@@ -60,6 +61,33 @@
             "powerful-number",
         ),
     ),
+    ExactReplayCheckerDeclaration(
+        "modular.polynomial_identity.compute",
+        ModularPolynomialIdentityRequest,
+        "check_modular_polynomial_identity",
+        "modular.polynomial-identity.flint-replay",
+        entrypoint_module=_EXACT_DOMAIN_ENTRYPOINT,
+        replay_method="Python-FLINT coefficientwise modular-polynomial replay",
+        reason=(
+            "operator-authorized Python-FLINT checker independently canonicalizes "
+            "and compares every formal polynomial coefficient modulo m"
+        ),
+        verification_capability_id="modular.polynomial_identity.verify",
+        verification_title="Verify a modular polynomial identity",
+        verification_description=(
+            "Independently verify one formal coefficientwise polynomial identity "
+            "over Z/mZ; this does not compare induced polynomial functions."
+        ),
+        verification_tags=(
+            "verification",
+            "exact",
+            "number-theory",
+            "modular",
+            "polynomial",
+            "identity",
+            "coefficientwise",
+        ),
+    ),
     ExactReplayCheckerDeclaration(
         "modular.polynomial_residue_image.compute",
         ModularPolynomialResidueImageRequest,

src/jacobian/domains/number_theory/modular.py

@@ -6,6 +6,8 @@
     IntegerValueResult,
     JacobiSymbolRequest,
     JacobiSymbolResult,
+    ModularPolynomialIdentityRequest,
+    ModularPolynomialIdentityResult,
     ModularPolynomialResidueImageRequest,
     ModularPolynomialResidueImageResult,
     ModularValueRequest,
@@ -23,6 +25,7 @@
 from jacobian.domains.number_theory.operations import (
     compute_jacobi_symbol,
     compute_modular_inverse,
+    compute_modular_polynomial_identity,
     compute_modular_polynomial_residue_image,
     compute_multiplicative_order,
     enumerate_quadratic_residues,
@@ -101,6 +104,36 @@
             ),
         ),
     ),
+    number_theory_operation(
+        "modular.polynomial_identity.compute",
+        "Compare modular polynomial coefficients",
+        (
+            "Canonicalize two sparse integer polynomials and compare their formal "
+            "coefficients modulo m. This is polynomial-ring identity, not equality "
+            "of the induced functions on residue assignments."
+        ),
+        ModularPolynomialIdentityRequest,
+        ModularPolynomialIdentityResult,
+        compute_modular_polynomial_identity,
+        "number-theory",
+        "modular",
+        "polynomial",
+        "identity",
+        "coefficientwise",
+        relation_id="modular.polynomial_identity.relation",
+        invocation_examples=(
+            example(
+                "coefficientwise_identity_mod_4",
+                "Compare two formal polynomial coefficients modulo 4.",
+                {
+                    "modulus": 4,
+                    "variables": ["z"],
+                    "left": [{"coefficient": "9", "exponents": [6]}],
+                    "right": [{"coefficient": "-7", "exponents": [6]}],
+                },
+            ),
+        ),
+    ),
     number_theory_operation(
         "modular.polynomial_residue_image.compute",
         "Compute modular polynomial residue image",

src/jacobian/domains/number_theory/operations.py

@@ -17,6 +17,7 @@
 import math
 from typing import Literal, cast
 
+from jacobian.canonical import format_canonical_integer, parse_canonical_integer
 from jacobian.contracts.number_theory import (
     ArithmeticFunctionRequest,
     BooleanResult,
@@ -37,11 +38,14 @@
     JacobiSymbolResult,
     LegendreSymbolRequest,
     LegendreSymbolResult,
+    ModularPolynomialIdentityRequest,
+    ModularPolynomialIdentityResult,
     ModularPolynomialResidueCount,
     ModularPolynomialResidueImageRequest,
     ModularPolynomialResidueImageResult,
     ModularPolynomialResidueTableRow,
     ModularPolynomialResidueWitness,
+    ModularPolynomialTerm,
     ModularValueRequest,
     ModulusRequest,
     NonnegativeIntegerRequest,
@@ -69,6 +73,7 @@
     "compute_legendre_symbol",
     "compute_mobius",
     "compute_modular_inverse",
+    "compute_modular_polynomial_identity",
     "compute_modular_polynomial_residue_image",
     "compute_multiplicative_order",
     "compute_next_prime",
@@ -442,6 +447,57 @@ def compute_modular_polynomial_residue_image(
     return _compute_modular_polynomial_residue_image(request, include_table=False)
 
 
+def compute_modular_polynomial_identity(
+    request: ModularPolynomialIdentityRequest,
+) -> ModularPolynomialIdentityResult:
+    """Compare canonical sparse coefficients in ``(Z/mZ)[x_1, ..., x_n]``."""
+    left = _normalize_modular_terms(request.left, request.modulus)
+    right = _normalize_modular_terms(request.right, request.modulus)
+    residual = _normalize_modular_terms(
+        (
+            *request.left,
+            *(
+                term.model_copy(
+                    update={
+                        "coefficient": format_canonical_integer(
+                            -parse_canonical_integer(term.coefficient)
+                        )
+                    }
+                )
+                for term in request.right
+            ),
+        ),
+        request.modulus,
+    )
+    return ModularPolynomialIdentityResult(
+        semantics_version="modular-polynomial-identity.v1",
+        modulus=request.modulus,
+        variable_order=request.variables,
+        normalized_left=left,
+        normalized_right=right,
+        residual=residual,
+        identical=not residual,
+        comparison_scope="FORMAL_COEFFICIENTWISE_IDENTITY",
+    )
+
+
+def _normalize_modular_terms(
+    terms: tuple[ModularPolynomialTerm, ...],
+    modulus: int,
+) -> tuple[NormalizedModularPolynomialTerm, ...]:
+    coefficients: dict[tuple[int, ...], int] = {}
+    for term in terms:
+        coefficients[term.exponents] = (
+            coefficients.get(term.exponents, 0)
+            + parse_canonical_integer(term.coefficient)
+        ) % modulus
+    return tuple(
+        NormalizedModularPolynomialTerm(coefficient=coefficient, exponents=exponents)
+        for exponents, coefficient in sorted(coefficients.items())
+        if coefficient
+    )
+
+
 def materialize_modular_polynomial_residue_assignments(
     request: ModularPolynomialResidueImageRequest,
 ) -> ModularPolynomialResidueImageResult: