Skip to content

Add modular polynomial identity verification - #915

Closed
yuelgrace1810-ops wants to merge 15 commits into
mainfrom
agent/modular-polynomial-identity
Closed

Add modular polynomial identity verification#915
yuelgrace1810-ops wants to merge 15 commits into
mainfrom
agent/modular-polynomial-identity

Conversation

@yuelgrace1810-ops

Copy link
Copy Markdown
Collaborator

Summary

  • add a typed modular.polynomial_identity.compute capability for formal coefficientwise equality in (Z/mZ)[x_1,...,x_n]
  • canonicalize duplicate monomials, negative coefficients, and zero residues while exposing the exact residual and comparison scope
  • add an operator-authorized independent Python-FLINT replay checker as modular.polynomial_identity.verify
  • explicitly distinguish formal polynomial identity from equality of induced functions on residue assignments

Why

A held-out audit of Conant's mod-4 Kawauchi example required certifying

P(z²) ≡ f(z)f(-z) in (Z/4Z)[z].

The existing polynomial.identity.verify operates over QQ, while modular.polynomial_residue_image.* verifies bounded value images. Neither establishes coefficientwise identity over a composite residue ring. This closes #912 without changing either existing operation's semantics.

Validation

  • make check: 869 unit tests, Ruff, formatting, complexity, and mypy passed
  • make test-domain: 189 passed
  • focused number-theory domain + exact-verification suite: 33 passed
  • focused checker installation + portfolio suite: 43 passed

Tests cover the original modulus-4 reproduction, a forged result, coefficient perturbation, negative coefficients, duplicate monomials, multivariate exponent vectors, prime modulus 7, and composite moduli 4 and 8.

Closes #912

@morluto
morluto marked this pull request as ready for review August 9, 2026 08:37

@devin-ai-integration devin-ai-integration Bot left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Devin Review found 3 potential issues.

View 1 additional finding in Devin Review.

Open in Devin Review

Comment thread src/jacobian_checkers/exact_domain_operations.py Outdated
Comment thread src/jacobian_checkers/exact_domain_operations.py
Comment thread src/jacobian_checkers/exact_domain_operations.py Outdated

@chatgpt-codex-connector chatgpt-codex-connector Bot left a comment

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 08b40b875f

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

  • Open a pull request for review
  • Mark a draft as ready
  • Comment "@codex review".

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".

Comment thread src/jacobian/domains/number_theory/operations.py Outdated
@morluto
morluto marked this pull request as draft August 9, 2026 08:43
@morluto
morluto marked this pull request as ready for review August 9, 2026 17:38

@chatgpt-codex-connector chatgpt-codex-connector Bot left a comment

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 08b40b875f

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

  • Open a pull request for review
  • Mark a draft as ready
  • Comment "@codex review".

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".

Comment thread src/jacobian_checkers/exact_domain_operations.py Outdated

@chatgpt-codex-connector chatgpt-codex-connector Bot left a comment

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: fc06831828

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

  • Open a pull request for review
  • Mark a draft as ready
  • Comment "@codex review".

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".

Comment thread src/jacobian_checkers/exact_domain_operations.py Outdated

@chatgpt-codex-connector chatgpt-codex-connector Bot left a comment

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 0a572c5151

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

  • Open a pull request for review
  • Mark a draft as ready
  • Comment "@codex review".

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".

Comment thread src/jacobian/domains/number_theory/operations.py Outdated

@chatgpt-codex-connector chatgpt-codex-connector Bot left a comment

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 1e07d8d6bb

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

  • Open a pull request for review
  • Mark a draft as ready
  • Comment "@codex review".

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".

Comment thread src/jacobian/contracts/number_theory.py

@chatgpt-codex-connector chatgpt-codex-connector Bot left a comment

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 4a06c234db

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

  • Open a pull request for review
  • Mark a draft as ready
  • Comment "@codex review".

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".

Comment thread src/jacobian/contracts/number_theory.py

morluto commented Aug 10, 2026

Copy link
Copy Markdown
Owner

Second-pass review: needs one more trust-boundary pass before merge. Most implementation defects have been repaired, but two concerns remain: (1) the new checker is still missing from the shared exact-domain generic attack-case table, so binding/digest/tamper coverage is incomplete; and (2) successful coefficientwise identity replay currently returns the generic exhaustive-integer evidence shape (EXHAUSTIVE_FINITE / EXHAUSTIVE). Please make the evidence semantics intentional and scoped to formal coefficient comparison—not residue-assignment exhaustiveness—and add the checker to the shared attack suite.

@chatgpt-codex-connector chatgpt-codex-connector Bot left a comment

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: e349a4ccc6

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

  • Open a pull request for review
  • Mark a draft as ready
  • Comment "@codex review".

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".

Comment thread src/jacobian/contracts/number_theory.py

Copy link
Copy Markdown
Collaborator Author

Addressed in e349a4c: check_modular_polynomial_identity is now included in the shared exact-domain binding/digest/tamper attack table, and accepted replay uses CHECKED_CERTIFICATE / NOT_APPLICABLE evidence explicitly scoped to formal coefficientwise comparison rather than residue-assignment exhaustiveness. Focused checker suites pass (148 passed).

# Conflicts:
#	src/jacobian/domains/number_theory/operations.py
#	src/jacobian_checkers/exact_domain_operations.py

Copy link
Copy Markdown
Collaborator Author

Follow-up: current main is now merged in 0bae5ba. The number-theory refactor conflict was resolved by moving the modular-identity producer into the new modular_operations kernel. GitHub now reports the PR mergeable; post-merge focused validation passed (129 tests).

Copy link
Copy Markdown
Collaborator Author

Addressed the latest review finding in 60814e9/1c1420b4: ModularPolynomialIdentityResult now recomputes the modular difference from both normalized operands and requires it to equal residual. Added direct model coverage and kept the independent-checker forgery regression contract-valid; focused modular identity tests pass.

# Conflicts:
#	tests/composition/portfolio/test_domain_bundles.py
#	tests/domain/number_theory/test_number_theory_verification.py

@morluto morluto left a comment

Copy link
Copy Markdown
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Post-cutover architecture audit

Disposition: retain the capability, rewrite on current main.

Formal coefficientwise identity in (Z/mZ)[x_1,…,x_n] is a real missing mathematical boundary and is distinct from both QQ identity and equality of induced residue functions. Model the residue ring/variable order and canonical sparse polynomials as parent-bound domain values so cross-modulus or cross-variable comparisons are impossible.

Canonicalize duplicate monomials/negative coefficients once at the request boundary, expose a domain-owned residual/decision result, and install a thin producer plus separate independent checker. Remove old number-theory bundles, generic assurance/completeness/relationships, and central dispatcher wiring. Keep composite-modulus, forged-result, duplicate, and multivariate regressions.

morluto commented Aug 12, 2026

Copy link
Copy Markdown
Owner

Post-#1256/#1265 review: keep the modular-polynomial identity operation, but revise/rebase it to the current math ownership model. The capability is still absent from current main.

The core semantics are good: normalize sparse coefficients in (Z/mZ)[x_1,…,x_n], compare formal coefficients, return the exact residual, and keep verification independent. That is a clean atomic tool.

On rebase, move the provider-independent polynomial/value semantics toward the current jacobian.math number-theory/polynomial owner rather than growing another implementation inside the capability/domain adapter. Use one canonical semantic input, explicit modular normalization, one OperationSpec, and a separate checker declaration. The result's identical/residual/comparison-scope facts are domain-owned; do not recreate generic conclusion/assurance/relationship fields around them.

Recommendation: revise rather than close; preserve the tests and exact checker, but make the new operation conform to the post-#1256 operation budget.

morluto commented Aug 12, 2026

Copy link
Copy Markdown
Owner

Superseded by #1286. The replacement owns formal coefficientwise modular-polynomial semantics in jacobian.math.modular_polynomials, exposes one thin number-theory operation, and independently normalizes both sides in a dedicated checker. It explicitly excludes induced-function equality and relationship/workflow machinery.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Add coefficientwise polynomial identity verification over Z/mZ

2 participants