add verified finite group factorizations

Author: Grace Lee Rui Yue

docs/reference/capabilities/number-theory/finite-abelian-group-factorization.md

@@ -0,0 +1,24 @@
+# Finite abelian group exact factorization
+
+`finite_abelian_group.exact_factorization.compute` works in a bounded product
+of cyclic groups `Z/n1 x ... x Z/nr`. It normalizes two supplied lists of
+integer vectors and exhaustively counts representations of every group element
+as `a+b` with `a` from the left factor and `b` from the right factor.
+
+The result contains the normalized factors, the complete representation-count
+histogram, an exact-factorization decision, and the first missing and duplicate
+representation witnesses when the decision is false. A complete coset
+transversal is the special case where the right factor contains only zero.
+
+The current contract supports rank at most six, group order at most 4,096,
+factor sizes at most 256, and a factor Cartesian product no larger than the
+group order. Coordinates may be noncanonical integers and are reduced by their
+corresponding cyclic moduli.
+
+The producer returns `COMPUTED` evidence. The operator-authorized companion
+`finite_abelian_group.exact_factorization.verify` independently normalizes the
+payload and replays every group sum, binding the accepted record to the exact
+group presentation, factors, histogram, decision, and witnesses.
+
+This capability verifies only the supplied finite factorization. It does not
+decide infinite lattice tiling, periodicity, or orbit-closure properties.

docs/reference/capabilities/number-theory/index.md

@@ -4,3 +4,4 @@
 
 - [Powerful-number decision](integer-powerful-number-decision.md)
 - [Integer prime-factorization verification](integer-prime-factorization-verification.md)
+- [Finite abelian group exact factorization](finite-abelian-group-factorization.md)

src/jacobian/contracts/number_theory.py

@@ -39,6 +39,9 @@
 _MAX_RESIDUE_EXPONENT = 32
 _MAX_RESIDUE_ASSIGNMENTS = 4_096
 _MAX_POLYNOMIAL_RESIDUE_MODULUS = 1_000_000
+_MAX_FINITE_GROUP_ORDER = 4_096
+_MAX_FINITE_GROUP_RANK = 6
+_MAX_FINITE_GROUP_FACTOR_SIZE = 256
 
 BoundedInteger = Annotated[
     str,
@@ -294,6 +297,43 @@ def require_canonical_bounded_polynomial(self) -> Self:
         return self
 
 
+class FiniteAbelianGroupFactorizationRequest(ContractModel):
+    """Two bounded integer-vector factors in a product of cyclic groups."""
+
+    moduli: tuple[StrictInt, ...] = Field(
+        min_length=1, max_length=_MAX_FINITE_GROUP_RANK
+    )
+    left: tuple[tuple[StrictInt, ...], ...] = Field(
+        min_length=1, max_length=_MAX_FINITE_GROUP_FACTOR_SIZE
+    )
+    right: tuple[tuple[StrictInt, ...], ...] = Field(
+        min_length=1, max_length=_MAX_FINITE_GROUP_FACTOR_SIZE
+    )
+
+    @model_validator(mode="after")
+    def require_bounded_product_group(self) -> Self:
+        if any(modulus < 2 or modulus > 1_000_000 for modulus in self.moduli):
+            raise ValueError("cyclic moduli must be between 2 and 1,000,000")
+        if math.prod(self.moduli) > _MAX_FINITE_GROUP_ORDER:
+            raise ValueError("finite abelian group exceeds the 4,096-element bound")
+        if len(self.left) * len(self.right) > _MAX_FINITE_GROUP_ORDER:
+            raise ValueError("factor Cartesian product exceeds the group-order bound")
+        if any(
+            len(element) != len(self.moduli)
+            for factor in (self.left, self.right)
+            for element in factor
+        ):
+            raise ValueError("every factor element must match the group rank")
+        if any(
+            abs(coordinate) > 1_000_000
+            for factor in (self.left, self.right)
+            for element in factor
+            for coordinate in element
+        ):
+            raise ValueError("factor coordinates exceed the input bound")
+        return self
+
+
 class ChineseRemainderRequest(ContractModel):
     """A finite system of integer congruences with parallel residues and moduli."""
 
@@ -541,6 +581,90 @@ def bind_complete_residue_image(self) -> Self:
         return self
 
 
+class FiniteAbelianRepresentationCount(ContractModel):
+    representation_count: StrictInt = Field(ge=0, le=_MAX_FINITE_GROUP_ORDER)
+    element_count: StrictInt = Field(ge=1, le=_MAX_FINITE_GROUP_ORDER)
+
+
+class FiniteAbelianRepresentationWitness(ContractModel):
+    element: tuple[StrictInt, ...] = Field(
+        min_length=1, max_length=_MAX_FINITE_GROUP_RANK
+    )
+    left: tuple[StrictInt, ...] = Field(min_length=1, max_length=_MAX_FINITE_GROUP_RANK)
+    right: tuple[StrictInt, ...] = Field(
+        min_length=1, max_length=_MAX_FINITE_GROUP_RANK
+    )
+    other_left: tuple[StrictInt, ...] | None = Field(
+        default=None, min_length=1, max_length=_MAX_FINITE_GROUP_RANK
+    )
+    other_right: tuple[StrictInt, ...] | None = Field(
+        default=None, min_length=1, max_length=_MAX_FINITE_GROUP_RANK
+    )
+
+
+class FiniteAbelianGroupFactorizationResult(ContractModel):
+    """Complete unique-representation summary for ``G = left + right``."""
+
+    semantics_version: Literal["finite-abelian-group-factorization.v1"]
+    moduli: tuple[StrictInt, ...] = Field(
+        min_length=1, max_length=_MAX_FINITE_GROUP_RANK
+    )
+    normalized_left: tuple[tuple[StrictInt, ...], ...] = Field(
+        min_length=1, max_length=_MAX_FINITE_GROUP_FACTOR_SIZE
+    )
+    normalized_right: tuple[tuple[StrictInt, ...], ...] = Field(
+        min_length=1, max_length=_MAX_FINITE_GROUP_FACTOR_SIZE
+    )
+    group_order: StrictInt = Field(ge=2, le=_MAX_FINITE_GROUP_ORDER)
+    pair_count: StrictInt = Field(ge=1, le=_MAX_FINITE_GROUP_ORDER)
+    distinct_sum_count: StrictInt = Field(ge=1, le=_MAX_FINITE_GROUP_ORDER)
+    representation_histogram: tuple[FiniteAbelianRepresentationCount, ...] = Field(
+        min_length=1
+    )
+    is_exact_factorization: StrictBool
+    first_missing: tuple[StrictInt, ...] | None = Field(
+        default=None, min_length=1, max_length=_MAX_FINITE_GROUP_RANK
+    )
+    first_duplicate: FiniteAbelianRepresentationWitness | None = None
+
+    @model_validator(mode="after")
+    def bind_factorization_summary(self) -> Self:
+        if self.group_order != math.prod(self.moduli):
+            raise ValueError("group order must equal the product of cyclic moduli")
+        if self.pair_count != len(self.normalized_left) * len(self.normalized_right):
+            raise ValueError("pair count must equal the factor Cartesian-product size")
+        counts = tuple(
+            item.representation_count for item in self.representation_histogram
+        )
+        if counts != tuple(sorted(set(counts))):
+            raise ValueError(
+                "representation histogram counts must be unique and increasing"
+            )
+        if (
+            sum(item.element_count for item in self.representation_histogram)
+            != self.group_order
+        ):
+            raise ValueError("representation histogram must cover the complete group")
+        if (
+            sum(
+                item.representation_count * item.element_count
+                for item in self.representation_histogram
+            )
+            != self.pair_count
+        ):
+            raise ValueError("representation histogram must cover every factor pair")
+        expected = self.pair_count == self.group_order and all(
+            item.representation_count == 1 for item in self.representation_histogram
+        )
+        if self.is_exact_factorization != expected:
+            raise ValueError(
+                "factorization decision does not match the complete histogram"
+            )
+        if self.is_exact_factorization and (self.first_missing or self.first_duplicate):
+            raise ValueError("exact factorizations cannot carry failure witnesses")
+        return self
+
+
 def _evaluate_normalized_modular_polynomial(
     terms: tuple[NormalizedModularPolynomialTerm, ...],
     assignment: tuple[int, ...],

src/jacobian/domains/number_theory/checkers.py

@@ -3,13 +3,40 @@
 from jacobian.checker_operations import ExactReplayCheckerDeclaration
 from jacobian.contracts.number_theory import (
     FactorizationRequest,
+    FiniteAbelianGroupFactorizationRequest,
     ModularPolynomialResidueImageRequest,
     PowerfulNumberRequest,
 )
 
 _EXACT_DOMAIN_ENTRYPOINT = "jacobian_checkers.exact_domain_operations"
 
 NUMBER_THEORY_EXACT_REPLAY_CHECKERS = (
+    ExactReplayCheckerDeclaration(
+        "finite_abelian_group.exact_factorization.compute",
+        FiniteAbelianGroupFactorizationRequest,
+        "check_finite_abelian_group_exact_factorization",
+        "finite-abelian-group.exact-factorization.stdlib-replay",
+        entrypoint_module=_EXACT_DOMAIN_ENTRYPOINT,
+        replay_method="Python standard-library exhaustive group replay",
+        reason=(
+            "operator-authorized checker independently normalizes both factors "
+            "and replays every sum in the complete finite group"
+        ),
+        verification_capability_id="finite_abelian_group.exact_factorization.verify",
+        verification_title="Verify a finite abelian group exact factorization",
+        verification_description=(
+            "Independently verify the complete representation histogram, exact "
+            "factorization decision, and first failure witnesses."
+        ),
+        verification_tags=(
+            "verification",
+            "exact",
+            "number-theory",
+            "finite-abelian-group",
+            "factorization",
+            "coset-transversal",
+        ),
+    ),
     ExactReplayCheckerDeclaration(
         "integer.compute.prime_factorization",
         FactorizationRequest,

src/jacobian/domains/number_theory/modular.py

@@ -3,6 +3,8 @@
 from jacobian.contracts.number_theory import (
     ChineseRemainderRequest,
     ChineseRemainderResult,
+    FiniteAbelianGroupFactorizationRequest,
+    FiniteAbelianGroupFactorizationResult,
     IntegerValueResult,
     JacobiSymbolRequest,
     JacobiSymbolResult,
@@ -21,6 +23,7 @@
     DISCRETE_LOGARITHM_CAPABILITY,
 )
 from jacobian.domains.number_theory.operations import (
+    compute_finite_abelian_group_factorization,
     compute_jacobi_symbol,
     compute_modular_inverse,
     compute_modular_polynomial_residue_image,
@@ -31,6 +34,45 @@
 )
 
 MODULAR_CAPABILITIES = (
+    number_theory_operation(
+        "finite_abelian_group.exact_factorization.compute",
+        "Compute a finite abelian group exact factorization",
+        (
+            "Normalize two supplied integer-vector factors in a bounded product "
+            "of cyclic groups and exhaustively decide whether every group element "
+            "has exactly one representation as a left-plus-right sum."
+        ),
+        FiniteAbelianGroupFactorizationRequest,
+        FiniteAbelianGroupFactorizationResult,
+        compute_finite_abelian_group_factorization,
+        "number-theory",
+        "finite-abelian-group",
+        "exact-factorization",
+        "coset-transversal",
+        "unique-representation",
+        "enumeration",
+        relation_id="finite_abelian_group.exact_factorization.relation",
+        invocation_examples=(
+            example(
+                "transversal_mod_2_4",
+                "Verify eight representatives of Z/2 x Z/4.",
+                {
+                    "moduli": [2, 4],
+                    "left": [
+                        [0, 0],
+                        [3, 0],
+                        [0, 2],
+                        [3, 2],
+                        [1, 1],
+                        [4, 1],
+                        [1, 3],
+                        [4, 3],
+                    ],
+                    "right": [[0, 0]],
+                },
+            ),
+        ),
+    ),
     number_theory_operation(
         "number_theory.compute.jacobi_symbol",
         "Compute Jacobi symbol",

src/jacobian/domains/number_theory/operations.py

@@ -28,6 +28,10 @@
     FactorialValuationRequest,
     FactorialValuationResult,
     FactorizationRequest,
+    FiniteAbelianGroupFactorizationRequest,
+    FiniteAbelianGroupFactorizationResult,
+    FiniteAbelianRepresentationCount,
+    FiniteAbelianRepresentationWitness,
     FloorSquareRootRequest,
     FloorSquareRootResult,
     IntegerPairRequest,
@@ -62,6 +66,7 @@
     "compute_euler_totient",
     "compute_extended_gcd",
     "compute_factorial_valuation",
+    "compute_finite_abelian_group_factorization",
     "compute_floor_square_root",
     "compute_gcd",
     "compute_jacobi_symbol",
@@ -442,6 +447,77 @@ def compute_modular_polynomial_residue_image(
     return _compute_modular_polynomial_residue_image(request, include_table=False)
 
 
+def compute_finite_abelian_group_factorization(
+    request: FiniteAbelianGroupFactorizationRequest,
+) -> FiniteAbelianGroupFactorizationResult:
+    """Exhaustively test unique representation in a product of cyclic groups."""
+    from collections import Counter
+    from itertools import product
+
+    moduli = request.moduli
+
+    def normalize(element: tuple[int, ...]) -> tuple[int, ...]:
+        return tuple(
+            coordinate % modulus
+            for coordinate, modulus in zip(element, moduli, strict=True)
+        )
+
+    left = tuple(normalize(element) for element in request.left)
+    right = tuple(normalize(element) for element in request.right)
+    representations: dict[
+        tuple[int, ...], list[tuple[tuple[int, ...], tuple[int, ...]]]
+    ] = {}
+    for left_element in left:
+        for right_element in right:
+            total = tuple(
+                (left_coordinate + right_coordinate) % modulus
+                for left_coordinate, right_coordinate, modulus in zip(
+                    left_element, right_element, moduli, strict=True
+                )
+            )
+            representations.setdefault(total, []).append((left_element, right_element))
+    group = tuple(product(*(range(modulus) for modulus in moduli)))
+    histogram = Counter(len(representations.get(element, ())) for element in group)
+    first_missing = next(
+        (element for element in group if element not in representations), None
+    )
+    duplicate_element = next(
+        (element for element in group if len(representations.get(element, ())) > 1),
+        None,
+    )
+    duplicate = None
+    if duplicate_element is not None:
+        first, second = representations[duplicate_element][:2]
+        duplicate = FiniteAbelianRepresentationWitness(
+            element=duplicate_element,
+            left=first[0],
+            right=first[1],
+            other_left=second[0],
+            other_right=second[1],
+        )
+    group_order = math.prod(moduli)
+    exact = len(left) * len(right) == group_order and histogram == {1: group_order}
+    return FiniteAbelianGroupFactorizationResult(
+        semantics_version="finite-abelian-group-factorization.v1",
+        moduli=moduli,
+        normalized_left=left,
+        normalized_right=right,
+        group_order=group_order,
+        pair_count=len(left) * len(right),
+        distinct_sum_count=len(representations),
+        representation_histogram=tuple(
+            FiniteAbelianRepresentationCount(
+                representation_count=count,
+                element_count=histogram[count],
+            )
+            for count in sorted(histogram)
+        ),
+        is_exact_factorization=exact,
+        first_missing=None if exact else first_missing,
+        first_duplicate=None if exact else duplicate,
+    )
+
+
 def materialize_modular_polynomial_residue_assignments(
     request: ModularPolynomialResidueImageRequest,
 ) -> ModularPolynomialResidueImageResult: