Skip to content

Commit 7a2074e

Browse files
morlutomorluto
authored
feat(number-theory): add verified finite abelian factorizations (#1301)
* refactor(checkers): let declarations own provider runtimes Compose declaration-owned clean-process runtimes with the latest batched checker-identity path. Existing checker families retain the legacy registry; new declarations may carry one unassigned provider runtime, and the composition root batches identity material across the full declaration set before authorization. * fix(checkers): defer declaration runtime measurement Store passive provider-runtime factories on exact replay declarations and realize each runtime once, at installation. Importing domain declarations no longer identifies or hashes checker source, while the existing installer and authorization boundary keep the same resolved runtime contract. * refactor(checkers): keep direct runtime migration compatibility Retain the existing direct provider_runtime constructor as a temporary compatibility seam while making provider_runtime_factory lazy and cached. Reject dual ownership and preserve pre-authorization invariants for both forms. * fix(checkers): type the lazy runtime accessor Declare the compatibility accessor's dynamic return as Any so mypy accepts the dataclass field interception while the public provider_runtime field retains its precise declared type. * feat(number-theory): add bounded finite abelian factorizations Rebuild the finite-abelian-group port as one domain-owned commit on the corrected declaration-runtime base. Keep exhaustive native semantics, one thin operation binding, a lazy dedicated checker runtime, independent stdlib replay, and focused positive and negative factorization coverage. * test: include check-all in the primary help contract * Fix invalid forged factorization assertion * Align forged factorization diagnostic * Align forged factorization output contract * fix declaration-owned checker runtime compatibility * fix(checkers): satisfy static validation * fix(checkers): handle declaration-owned runtime installation * fix(checkers): require explicit optional provider omission * Merge origin/main into finite abelian factorization PR
1 parent 8809168 commit 7a2074e

8 files changed

Lines changed: 771 additions & 2 deletions

File tree

‎src/jacobian/domains/number_theory/bundle.py‎

Lines changed: 7 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,9 @@
99
from jacobian.domains.number_theory.checkers import NUMBER_THEORY_EXACT_REPLAY_CHECKERS
1010
from jacobian.domains.number_theory.derived import DERIVED_NUMBER_THEORY_CAPABILITIES
1111
from jacobian.domains.number_theory.divisibility import DIVISIBILITY_CAPABILITIES
12+
from jacobian.domains.number_theory.finite_abelian_groups import (
13+
FINITE_ABELIAN_GROUP_FACTORIZATION_CAPABILITY,
14+
)
1215
from jacobian.domains.number_theory.modular import MODULAR_CAPABILITIES
1316
from jacobian.domains.number_theory.modular_identity import (
1417
MODULAR_IDENTITY_CAPABILITIES,
@@ -29,11 +32,12 @@ def build_number_theory_bundle() -> DomainBundle:
2932
schema_namespace="jacobian.number-theory",
3033
semantics=DomainSemantics(
3134
name="jacobian.exact-integer-number-theory",
32-
version="1",
35+
version="2",
3336
definition={
3437
"description": (
3538
"Exact integer divisibility, primes, arithmetic functions, "
36-
"and modular arithmetic over bounded inputs"
39+
"modular arithmetic, and bounded finite abelian group "
40+
"factorization"
3741
),
3842
"integer_encoding": "canonical decimal string",
3943
},
@@ -49,6 +53,7 @@ def build_number_theory_bundle() -> DomainBundle:
4953
*MODULAR_CAPABILITIES,
5054
*MODULAR_IDENTITY_CAPABILITIES,
5155
*DERIVED_NUMBER_THEORY_CAPABILITIES,
56+
FINITE_ABELIAN_GROUP_FACTORIZATION_CAPABILITY,
5257
),
5358
diagnostics=DomainDiagnostics(
5459
invalid_request=CapabilityDiagnostic(

‎src/jacobian/domains/number_theory/checkers.py‎

Lines changed: 48 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -11,12 +11,32 @@
1111
ModularPolynomialResidueImageRequest,
1212
PowerfulNumberRequest,
1313
)
14+
from jacobian.math.finite_abelian_groups import FiniteAbelianGroupFactorizationRequest
1415
from jacobian.provider_runtime import source_provider_runtime
1516
from jacobian.providers import flint_runtime
1617

1718
_EXACT_DOMAIN_ENTRYPOINT = "jacobian_checkers.exact_domain_operations"
1819

1920

21+
def _finite_abelian_group_checker_runtime(
22+
*, checker_ids: tuple[str, ...] = ()
23+
) -> CapabilityProviderRuntime:
24+
"""Measure the exhaustive group checker only when installation requests it."""
25+
26+
return source_provider_runtime(
27+
"jacobian.finite-abelian-group-checker",
28+
version="1",
29+
entrypoint=(
30+
"jacobian_checkers.finite_abelian_groups:"
31+
"check_finite_abelian_group_exact_factorization"
32+
),
33+
install_tier=CapabilityInstallTier.T1,
34+
license_id="MIT",
35+
features=("exhaustive-finite-group-replay", "clean-process-checker"),
36+
checker_ids=checker_ids,
37+
)
38+
39+
2040
def _flint_exact_replay_runtime(
2141
*, checker_ids: tuple[str, ...] = (), refresh: bool = False
2242
) -> CapabilityProviderRuntime:
@@ -41,6 +61,34 @@ def _integer_lcm_runtime(
4161

4262

4363
NUMBER_THEORY_EXACT_REPLAY_CHECKERS = (
64+
ExactReplayCheckerDeclaration(
65+
"finite_abelian_group.exact_factorization.compute",
66+
FiniteAbelianGroupFactorizationRequest,
67+
"check_finite_abelian_group_exact_factorization",
68+
"finite-abelian-group.exact-factorization.stdlib-replay",
69+
entrypoint_module="jacobian_checkers.finite_abelian_groups",
70+
replay_method="standard-library exhaustive finite-group replay",
71+
reason=(
72+
"operator-authorized standard-library checker independently "
73+
"normalizes both factors and replays every group sum"
74+
),
75+
provider_runtime_factory=_finite_abelian_group_checker_runtime,
76+
verification_capability_id="finite_abelian_group.exact_factorization.verify",
77+
verification_title="Verify a finite abelian group factorization",
78+
verification_description=(
79+
"Independently normalize both bounded factors, enumerate every sum "
80+
"in the declared product of cyclic groups, and verify the complete "
81+
"representation histogram, decision, and first failure witnesses."
82+
),
83+
verification_tags=(
84+
"verification",
85+
"exact",
86+
"number-theory",
87+
"finite-abelian-group",
88+
"factorization",
89+
"unique-representation",
90+
),
91+
),
4492
ExactReplayCheckerDeclaration(
4593
"integer.compute.lcm",
4694
IntegerPairRequest,

‎src/jacobian/domains/number_theory/finite_abelian_groups.py‎

Lines changed: 72 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,72 @@
1+
"""Thin operation binding for finite abelian group factorization."""
2+
3+
from __future__ import annotations
4+
5+
from jacobian.contracts.capabilities import CapabilityDiagnostic
6+
from jacobian.domains._examples import example
7+
from jacobian.math.finite_abelian_groups import (
8+
FiniteAbelianGroupFactorizationRequest,
9+
FiniteAbelianGroupFactorizationResult,
10+
finite_abelian_group_factorization,
11+
)
12+
from jacobian.operation_bindings import inline_operation
13+
from jacobian.operations import OperationSpec
14+
15+
FINITE_ABELIAN_GROUP_FACTORIZATION_CAPABILITY = inline_operation(
16+
OperationSpec(
17+
operation_id="finite_abelian_group.exact_factorization.compute",
18+
version="1",
19+
title="Exact finite abelian group factorization",
20+
description=(
21+
"Normalize two bounded integer-vector factors in a declared product "
22+
"of cyclic groups, exhaustively count every sum representation, and "
23+
"decide whether every group element has exactly one representation."
24+
),
25+
request_type=FiniteAbelianGroupFactorizationRequest,
26+
result_type=FiniteAbelianGroupFactorizationResult,
27+
execute=finite_abelian_group_factorization,
28+
tags=(
29+
"number-theory",
30+
"finite-abelian-group",
31+
"cyclic-product",
32+
"factorization",
33+
"unique-representation",
34+
"coset-transversal",
35+
"exact",
36+
),
37+
invalid_request=CapabilityDiagnostic(
38+
code="INVALID_FINITE_ABELIAN_FACTORIZATION_REQUEST",
39+
stage="finite_abelian_group_input_validation",
40+
message=(
41+
"Input does not satisfy the bounded product-of-cyclic-groups "
42+
"factorization contract."
43+
),
44+
hint=(
45+
"Supply rank at most 6, group order and factor product at most "
46+
"4,096, and distinct bounded factor elements after normalization."
47+
),
48+
),
49+
invocation_examples=(
50+
example(
51+
"z2_times_z4_transversal",
52+
"Verify eight representatives form a complete transversal.",
53+
{
54+
"moduli": [2, 4],
55+
"left": [
56+
[0, 0],
57+
[0, 1],
58+
[0, 2],
59+
[0, 3],
60+
[1, 0],
61+
[1, 1],
62+
[1, 2],
63+
[1, 3],
64+
],
65+
"right": [[0, 0]],
66+
},
67+
),
68+
),
69+
)
70+
)
71+
72+
__all__ = ["FINITE_ABELIAN_GROUP_FACTORIZATION_CAPABILITY"]

‎src/jacobian/math/__init__.py‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,7 @@
22

33
from jacobian.math import (
44
arithmetic,
5+
finite_abelian_groups,
56
finite_fields,
67
graphs,
78
matrices,
@@ -12,6 +13,7 @@
1213

1314
__all__ = [
1415
"arithmetic",
16+
"finite_abelian_groups",
1517
"finite_fields",
1618
"graphs",
1719
"matrices",

0 commit comments

Comments
 (0)