Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 3 additions & 0 deletions src/jacobian/math/integral_binary_quadratic_forms/__init__.py
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
"""Integral binary quadratic form operations."""

__all__: list[str] = []
40 changes: 40 additions & 0 deletions src/jacobian/math/integral_binary_quadratic_forms/_admission.py
Original file line number Diff line number Diff line change
@@ -0,0 +1,40 @@
"""Owner-local admission decisions for built-in math operations."""

from __future__ import annotations

from jacobian.catalog.admission import (
AdmissionDecision,
OperationAdmission,
OperationRegistration,
)
from jacobian.math.integral_binary_quadratic_forms._tools import TOOLS

ADMISSIONS: tuple[OperationAdmission, ...] = (
OperationAdmission(
"number_theory.binary_quadratic_form.check",
AdmissionDecision.KEEP,
"exact primitive positive-definite form check with discriminant and Gram",
),
OperationAdmission(
"number_theory.binary_quadratic_form.evaluate",
AdmissionDecision.KEEP,
"exact evaluation of a binary quadratic form at an integer pair",
),
OperationAdmission(
"number_theory.binary_quadratic_form.reduce",
AdmissionDecision.KEEP,
"exact Gauss reduction with SL_2(Z) witness and step ledger",
),
OperationAdmission(
"number_theory.binary_quadratic_form.proper_equivalence.decide",
AdmissionDecision.KEEP,
"exact proper equivalence decision via canonical reduced representative",
),
OperationAdmission(
"number_theory.binary_quadratic_form.reduced_classes.compute",
AdmissionDecision.KEEP,
"exact complete enumeration of reduced classes for a negative discriminant",
),
)

REGISTRATION = OperationRegistration(TOOLS, ADMISSIONS)
214 changes: 214 additions & 0 deletions src/jacobian/math/integral_binary_quadratic_forms/_models.py
Original file line number Diff line number Diff line change
@@ -0,0 +1,214 @@
"""Typed wire contracts for integral binary quadratic form operations."""

from __future__ import annotations

from typing import Literal, Self

from pydantic import Field, model_validator

from jacobian._models import StrictModel

MAX_COEFFICIENT = 10**6


class BinaryQuadraticFormCheckRequest(StrictModel):
"""Request to check integer coefficients as a primitive positive-definite form."""

a: int = Field(ge=-MAX_COEFFICIENT, le=MAX_COEFFICIENT)
b: int = Field(ge=-MAX_COEFFICIENT, le=MAX_COEFFICIENT)
c: int = Field(ge=-MAX_COEFFICIENT, le=MAX_COEFFICIENT)


class BinaryQuadraticFormEvaluateRequest(StrictModel):
"""Request to evaluate a checked form at an integer pair (x, y)."""

a: int
b: int
c: int
Comment on lines +25 to +27

Copy link
Copy Markdown

Choose a reason for hiding this comment

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

P2 Badge Use a canonical form value across these operations

The form is represented here as three raw coefficients, again as form1/form2 tuples for equivalence, and as separate original/reduced fields in results. Consequently, even the serialized output of the check operation cannot be passed unchanged to evaluate or reduce because it contains extra status/result fields, forcing callers to reconstruct (a,b,c) manually. Introduce one domain-owned binary-quadratic-form value and use it consistently in producer results and consumer requests.

AGENTS.md reference: AGENTS.md:L95-L97

Useful? React with 👍 / 👎.

Comment on lines +25 to +27

Copy link
Copy Markdown

Choose a reason for hiding this comment

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

P2 Badge Bound evaluation coefficients before computing

Unlike x and y and the other coefficient-bearing requests, these fields accept integers of arbitrary magnitude. A native or successfully decoded request containing a coefficient with millions of digits therefore reaches _evaluate, which performs multiplication and constructs an equally unbounded exact result on the synchronous execution path. Apply an explicit coefficient budget in this request model so accepted inputs, intermediate work, and outputs remain bounded.

AGENTS.md reference: AGENTS.md:L128-L135

Useful? React with 👍 / 👎.

x: int = Field(ge=-MAX_COEFFICIENT, le=MAX_COEFFICIENT)
y: int = Field(ge=-MAX_COEFFICIENT, le=MAX_COEFFICIENT)


class BinaryQuadraticFormReduceRequest(StrictModel):
"""Request Gauss reduction of a primitive positive-definite form."""

a: int = Field(ge=-MAX_COEFFICIENT, le=MAX_COEFFICIENT)
b: int = Field(ge=-MAX_COEFFICIENT, le=MAX_COEFFICIENT)
c: int = Field(ge=-MAX_COEFFICIENT, le=MAX_COEFFICIENT)

@model_validator(mode="after")
def require_valid_form(self) -> Self:
if self.a <= 0:
raise ValueError("a must be positive for positive-definite")
disc = self.b * self.b - 4 * self.a * self.c
if disc >= 0:
raise ValueError("discriminant must be negative")
if disc % 4 not in (0, 1):
raise ValueError("discriminant must be 0 or 1 mod 4")
from math import gcd

if gcd(gcd(self.a, self.b), self.c) != 1:
raise ValueError("form must be primitive")
return self


class BinaryQuadraticFormProperEquivRequest(StrictModel):
"""Request to decide proper (SL_2(Z)) equivalence of two forms."""

form1: tuple[int, int, int]
form2: tuple[int, int, int]
Comment thread
morluto marked this conversation as resolved.


class BinaryQuadraticFormReducedClassesRequest(StrictModel):
"""Request all reduced primitive positive-definite classes of a discriminant."""

discriminant: int = Field(le=-3)
Comment thread
morluto marked this conversation as resolved.
Comment thread
morluto marked this conversation as resolved.


class BinaryQuadraticFormCheckResult(StrictModel):
"""Result of checking a binary quadratic form."""

status: Literal["PRIMITIVE_POSITIVE_DEFINITE", "NOT_IN_INITIAL_DOMAIN"]
obstruction: str | None = None
a: int | None = None
b: int | None = None
c: int | None = None
discriminant: int | None = None
gram: tuple[tuple[int, ...], ...] | None = None

@model_validator(mode="after")
def bind_result(self) -> Self:
if self.status == "PRIMITIVE_POSITIVE_DEFINITE":

Copy link
Copy Markdown

Choose a reason for hiding this comment

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

P2 Badge Bind negative check results to their source form

When the status is NOT_IN_INITIAL_DOMAIN, the result omits the inspected coefficients and this validator performs no consistency check, so a result claiming that the valid form [1,1,1] is outside the domain can revalidate unchanged. Retain the source coefficients on this branch and verify the negative classification so the authoritative decision cannot be detached from its input.

AGENTS.md reference: AGENTS.md:L156-L157

Useful? React with 👍 / 👎.

if self.a is None or self.b is None or self.c is None:
raise ValueError("accepted form must carry coefficients")
if self.discriminant is None:
raise ValueError("accepted form must carry discriminant")
if self.discriminant != self.b**2 - 4 * self.a * self.c:
raise ValueError("discriminant must be b^2 - 4ac")
Comment on lines +81 to +87

Copy link
Copy Markdown

Choose a reason for hiding this comment

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

P2 Badge Validate the claimed positive-definite status

When status is PRIMITIVE_POSITIVE_DEFINITE, this validator checks only that the discriminant matches the coefficients; it never verifies a > 0, a negative discriminant, or primitivity. For example, status="PRIMITIVE_POSITIVE_DEFINITE", a=-1, b=0, c=1, discriminant=4 validates despite being indefinite, allowing an incorrect authoritative classification to revalidate as an exact result. Recheck the defining domain predicates in this branch.

AGENTS.md reference: AGENTS.md:L156-L157

Useful? React with 👍 / 👎.

if self.gram is not None and self.gram != (
(self.a, self.b),
(self.b, self.c),
):
raise ValueError("gram must be [[a,b],[b,c]]")
return self


class BinaryQuadraticFormEvaluateResult(StrictModel):
"""Result of evaluating a form at (x, y)."""

a: int
b: int
c: int
x: int
y: int
value: int
primitive: bool

@model_validator(mode="after")
def bind_value(self) -> Self:
from jacobian.math.integral_binary_quadratic_forms._operations import (
_evaluate,
_gcd,
)

value = _evaluate(self.a, self.b, self.c, self.x, self.y)
if self.value != value:
raise ValueError("value must be a*x^2 + b*x*y + c*y^2")
primitive = _gcd(self.x, self.y) == 1
if self.primitive != primitive:
raise ValueError("primitive must be gcd(x,y)==1")
return self


class ReducedBinaryQuadraticFormResult(StrictModel):
"""Result of Gauss reduction."""

a: int
b: int
c: int
reduced_a: int
reduced_b: int
reduced_c: int
matrix: tuple[tuple[int, int], tuple[int, int]]
steps: tuple[tuple[int, int, int, int, int, int, int, int, int, int], ...]

Copy link
Copy Markdown

Choose a reason for hiding this comment

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

P2 Badge Validate every reduction step in the ledger

The advertised reduction certificate includes this step ledger, but result validation never checks that each tuple transforms its recorded source to its destination, that consecutive steps chain together, or that their product equals matrix. Consequently, replacing a producer's ledger with arbitrary ten-integer tuples still yields a valid exact result; replay these bounded steps and their composition during validation.

AGENTS.md reference: AGENTS.md:L156-L157

Useful? React with 👍 / 👎.


@model_validator(mode="after")
def bind_reduction(self) -> Self:
from jacobian.math.integral_binary_quadratic_forms._operations import (
_check_reduced,
)

if not _check_reduced(self.reduced_a, self.reduced_b, self.reduced_c):
raise ValueError("reduced form must satisfy |b|<=a<=c with tie-breaking")
if (
self.a == self.reduced_a
and self.b == self.reduced_b
and self.c == self.reduced_c
):
return self
Comment on lines +143 to +148

Copy link
Copy Markdown

Choose a reason for hiding this comment

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

P2 Badge Validate the matrix for already-reduced forms

When the input is already reduced, this early return skips both the determinant and transformation checks. For example, a result with identical original/reduced coefficients but matrix=((2, 0), (0, 2)) is accepted even though the advertised SL₂(Z) witness has determinant 4, so corrupted producer output can pass result validation; validate the matrix on this path as well.

AGENTS.md reference: AGENTS.md:L103-L114

Useful? React with 👍 / 👎.

p, q = self.matrix[0]
r, s = self.matrix[1]
if p * s - q * r != 1:
raise ValueError("transformation matrix must have determinant 1")
ra, rb, rc = _transform(self.a, self.b, self.c, p, q, r, s)
if (ra, rb, rc) != (self.reduced_a, self.reduced_b, self.reduced_c):
raise ValueError("transformation must map original to reduced form")
return self


def _transform(
a: int, b: int, c: int, p: int, q: int, r: int, s: int
) -> tuple[int, int, int]:
"""Apply SL_2(Z) transformation U=[[p,q],[r,s]] to form [a,b,c]."""
na = a * p * p + b * p * r + c * r * r
nb = 2 * a * p * q + b * (p * s + q * r) + 2 * c * r * s
nc = a * q * q + b * q * s + c * s * s
return na, nb, nc


class ProperEquivalenceResult(StrictModel):
"""Result of proper equivalence decision."""

form1: tuple[int, int, int]
form2: tuple[int, int, int]
status: Literal["PROPERLY_EQUIVALENT", "NOT_PROPERLY_EQUIVALENT"]
matrix: tuple[tuple[int, int], tuple[int, int]] | None = None

@model_validator(mode="after")
def bind_equivalence(self) -> Self:
if self.status == "PROPERLY_EQUIVALENT" and self.matrix is not None:
p, q = self.matrix[0]
Comment on lines +177 to +180

Copy link
Copy Markdown

Choose a reason for hiding this comment

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

P2 Badge Bind the equivalence status to the forms

When a result carries NOT_PROPERLY_EQUIVALENT, this condition performs no mathematical validation at all; even identical forms such as (1,1,1) and (1,1,1) are accepted with that false status. A producer regression would therefore escape result construction and expose an incorrect exact decision, so recompute or otherwise bind both status branches to the supplied forms.

AGENTS.md reference: AGENTS.md:L74-L77

Useful? React with 👍 / 👎.

r, s = self.matrix[1]
if p * s - q * r != 1:
raise ValueError("witness matrix must have determinant 1")
a1, b1, c1 = self.form1
ta, tb, tc = _transform(a1, b1, c1, p, q, r, s)
if (ta, tb, tc) != self.form2:
raise ValueError("witness must map form1 to form2")
return self


class ReducedClassesResult(StrictModel):
"""Result of enumerating reduced classes of a discriminant."""

discriminant: int
classes: tuple[tuple[int, int, int], ...]
class_number: int

@model_validator(mode="after")
def bind_classes(self) -> Self:
from jacobian.math.integral_binary_quadratic_forms._operations import (
_check_reduced,
)

if self.class_number != len(self.classes):
raise ValueError("class_number must equal the number of classes")
Comment on lines +204 to +205

Copy link
Copy Markdown

Choose a reason for hiding this comment

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

P2 Badge Verify that the reduced class list is complete

This checks only that class_number matches the supplied list length, not that the list is the complete class set promised by the operation. For example, ReducedClassesResult(discriminant=-23, classes=(), class_number=0) validates even though the exact class number is 3, allowing truncated or empty producer output to revalidate as an exact result; bind the tuple against the complete enumeration.

AGENTS.md reference: AGENTS.md:L103-L114

Useful? React with 👍 / 👎.

for a, b, c in self.classes:
if b * b - 4 * a * c != self.discriminant:
raise ValueError("every class must have the requested discriminant")
if not _check_reduced(a, b, c):
raise ValueError("every class must be reduced")
seen = set(self.classes)
if len(seen) != len(self.classes):
raise ValueError("classes must be distinct")
return self
Loading