feat(number-theory): add verified finite abelian factorizations - #1301
Conversation
6a97690 to
2b4f61d
Compare
AttributionThe bounded exact finite-abelian-group factorization producer and verifier originated in #910, authored by @yuelgrace1810-ops. This PR ports that work into the provider-independent math layer and declaration-owned checker model while preserving the original credit. |
Synchronize #1301 with the final lazy, migration-compatible declaration runtime boundary.
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.
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.
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.
b33a9ff to
3d9e943
Compare
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.
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.
89fe8b7 to
1a77dce
Compare
|
Bugbot is not enabled for your account, so this pull request was not reviewed. Enable Bugbot in the Cursor dashboard to get automatic reviews on future PRs. |
💡 Codex Reviewjacobian/src/jacobian/checker_operations.py Line 213 in 1868087 Do not cache the realized runtime on the module-global declaration: after any earlier access or runtime construction, subsequent authorizations reuse this stale probe instead of remeasuring the current checker source. If the checker package changes or becomes available within the same process, the registry can authorize using the old provider digest, and the worker then rejects the newly authorized checker as changed; the test suite already needs manual cache clearing around monkeypatched factories. Keep caching bounded to one installation batch rather than the declaration lifetime. AGENTS.md reference: AGENTS.md:L137-L140 Move these request/result/value models into AGENTS.md reference: AGENTS.md:L76-L83 Register AGENTS.md reference: AGENTS.md:L65-L68 ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
If Codex has suggestions, it will comment; otherwise it will react with 👍. Codex can also answer questions or update the PR. Try commenting "@codex address that feedback". |
|
Reconciled this branch with current main and pushed merge commit 2d0ba83. The resolution keeps main's checker/runtime installer semantics, then reapplies the finite-Abelian-group declaration and preserves the required optional-provider installation expectation. Focused validation: 61 tests passed. |
Coverage ReportTotal coverage: 77% (threshold: 50%) |
Summary
Supersedes #910 with a current-ownership port of bounded finite abelian group factorization.
jacobian.math.finite_abelian_groups;OperationSpecforfinite_abelian_group.exact_factorization.compute;Ownership and validation
The result model validates structural invariants only; exhaustive mathematical replay lives in the semantic function and the separate checker, not in a Pydantic validator or capability adapter. The operation returns an inline typed value and creates no artifacts. The checker alone may produce a verification record after operator authorization.
This PR is stacked on #1299 so the number-theory declaration owns its clean-process runtime instead of adding another central checker-runtime mapping.
Bounds
Validation
Focused coverage uses a noncanonical eight-element transversal of
Z/2 x Z/4, verifies the complete factorization independently, checks deterministic duplicate witnesses on a negative case, and rejects a forged decision. Hosted CI is authoritative for the full matrix.Credit
This is a current-ownership port of the original implementation in #910 by @yuelgrace1810-ops. Their original investigation, reproduction, and implementation work are the basis for this replacement.