Skip to content

Commit 7198240

Browse files
Extend exact determinant bound to order 64
1 parent 7d277e1 commit 7198240

8 files changed

Lines changed: 191 additions & 24 deletions

File tree

docs/reference/capabilities/matrix/matrix-rational-determinant.md

Lines changed: 8 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -7,17 +7,19 @@ separate trust boundaries.
77

88
## Input and result contracts
99

10-
The producer accepts one [`RationalMatrix`](../index.md#shared-matrix-values)
11-
from `jacobian.contracts.matrices`: a nonempty square matrix with at most 32
12-
rows and columns. Every entry is a canonical reduced rational:
10+
The producer accepts one determinant-owned exact rational matrix: a nonempty
11+
square matrix with at most 64 rows and columns. This operation-specific bound
12+
does not widen the shared 32-row and 32-column [`RationalMatrix`](../index.md#shared-matrix-values)
13+
used by rank, RREF, multiplication, and other matrix operations. Every entry is
14+
a canonical reduced rational:
1315

1416
```json
1517
{"num": "-3", "den": "7"}
1618
```
1719

18-
The shared `RationalMatrix` model permits up to 32,768 canonical digits per
19-
scalar component; the determinant request model tightens this to 256 decimal
20-
digits via its own `require_matrix_scalar_digits` validator.
20+
The determinant input value has the same canonical `QQ` matrix semantics. The
21+
determinant request model limits every scalar component to 256 decimal digits
22+
via its own `require_matrix_scalar_digits` validator.
2123

2224
`matrix.determinant.compute` uses SymPy's exact matrix determinant API with the
2325
fraction-free Bareiss method. It returns the bounded canonical determinant

src/jacobian/contracts/matrix_operations.py

Lines changed: 25 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -19,6 +19,7 @@
1919
from jacobian.contracts.results import ContractModel
2020

2121
MAX_INPUT_SCALAR_DIGITS = 256
22+
MAX_DETERMINANT_MATRIX_DIMENSION = 64
2223

2324

2425
def _check_integer_digits(
@@ -74,10 +75,32 @@ def require_square(self) -> Self:
7475
return self
7576

7677

78+
class DeterminantRationalMatrix(ContractModel):
79+
"""One determinant-owned exact rational matrix bounded independently."""
80+
81+
matrix_schema_version: Literal["1"] = "1"
82+
domain: Literal["QQ"] = "QQ"
83+
entries: tuple[tuple[CanonicalRational, ...], ...] = Field(
84+
min_length=1,
85+
max_length=MAX_DETERMINANT_MATRIX_DIMENSION,
86+
)
87+
88+
@model_validator(mode="after")
89+
def require_rectangular_nonempty_rows(self) -> Self:
90+
column_count = len(self.entries[0])
91+
if not 1 <= column_count <= MAX_DETERMINANT_MATRIX_DIMENSION:
92+
raise ValueError(
93+
"determinant matrix rows must contain between 1 and 64 entries"
94+
)
95+
if any(len(row) != column_count for row in self.entries):
96+
raise ValueError("determinant matrix rows must all have the same length")
97+
return self
98+
99+
77100
class MatrixDeterminantRequest(ContractModel):
78-
"""One bounded square matrix whose exact determinant is requested."""
101+
"""One square matrix of order at most 64 whose determinant is requested."""
79102

80-
matrix: RationalMatrix
103+
matrix: DeterminantRationalMatrix
81104

82105
@model_validator(mode="after")
83106
def require_square(self) -> Self:

src/jacobian/domains/matrix_lattice/capabilities.py

Lines changed: 5 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -115,7 +115,10 @@ def implementation(request: RequestT) -> ComputedOutcome[ResultT]:
115115
matrix_operation(
116116
"matrix.determinant.compute",
117117
"Compute an exact rational matrix determinant",
118-
"Compute the determinant of one square matrix over QQ with SymPy's exact Bareiss algorithm.",
118+
(
119+
"Compute the determinant of one square matrix over QQ through order 64 "
120+
"with SymPy's exact Bareiss algorithm."
121+
),
119122
MatrixDeterminantRequest,
120123
MatrixDeterminantResult,
121124
compute_determinant,
@@ -143,7 +146,7 @@ def implementation(request: RequestT) -> ComputedOutcome[ResultT]:
143146
},
144147
),
145148
),
146-
version="2",
149+
version="3",
147150
),
148151
matrix_operation(
149152
"matrix.rank.compute",

src/jacobian/domains/matrix_lattice/conversions.py

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,7 @@
77
from jacobian.canonical import format_canonical_integer, parse_canonical_integer
88
from jacobian.contracts.exact import CanonicalRational
99
from jacobian.contracts.matrices import IntegerMatrix, RationalMatrix
10+
from jacobian.contracts.matrix_operations import DeterminantRationalMatrix
1011

1112
__all__ = [
1213
"integer_matrix_from_sympy",
@@ -30,7 +31,9 @@ def rational_from_sympy(value: Any) -> CanonicalRational:
3031
)
3132

3233

33-
def rational_matrix_to_sympy(matrix: RationalMatrix) -> Any:
34+
def rational_matrix_to_sympy(
35+
matrix: RationalMatrix | DeterminantRationalMatrix,
36+
) -> Any:
3437
import sympy
3538

3639
return sympy.Matrix(

src/jacobian/domains/matrix_lattice/kernels.py

Lines changed: 18 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -22,11 +22,22 @@
2222
]
2323

2424

25-
def _exact_matrix(value: MatrixBase) -> MatrixBase:
25+
_DEFAULT_MAX_MATRIX_DIMENSION = 32
26+
_DETERMINANT_MAX_MATRIX_DIMENSION = 64
27+
28+
29+
def _exact_matrix(
30+
value: MatrixBase,
31+
*,
32+
maximum_dimension: int = _DEFAULT_MAX_MATRIX_DIMENSION,
33+
) -> MatrixBase:
2634
if not isinstance(value, MatrixBase):
2735
raise TypeError("matrix must be a SymPy MatrixBase")
28-
if not 1 <= value.rows <= 32 or not 1 <= value.cols <= 32:
29-
raise ValueError("matrix dimensions must be between 1 and 32")
36+
if (
37+
not 1 <= value.rows <= maximum_dimension
38+
or not 1 <= value.cols <= maximum_dimension
39+
):
40+
raise ValueError(f"matrix dimensions must be between 1 and {maximum_dimension}")
3041
if any(not entry.is_number or entry.is_finite is not True for entry in value):
3142
raise ValueError("matrix entries must be finite exact numbers")
3243
if any(entry.has(sympy.Float) for entry in value):
@@ -67,7 +78,10 @@ def characteristic_polynomial(matrix: MatrixBase, variable: str) -> Any:
6778

6879

6980
def determinant(matrix: MatrixBase) -> Any:
70-
source = _exact_matrix(matrix)
81+
source = _exact_matrix(
82+
matrix,
83+
maximum_dimension=_DETERMINANT_MAX_MATRIX_DIMENSION,
84+
)
7185
if source.rows != source.cols:
7286
raise ValueError("determinant requires a square matrix")
7387
return source.det(method="bareiss")

src/jacobian_checkers/exact_domain_operations.py

Lines changed: 32 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -27,6 +27,7 @@
2727
_MAX_RESIDUE_ASSIGNMENTS = 4_096
2828
_MAX_RESIDUE_MODULUS = 1_000_000
2929
_MAX_MATRIX_DIMENSION = 32
30+
_MAX_DETERMINANT_MATRIX_DIMENSION = 64
3031
_MAX_MATRIX_INPUT_DIGITS = 256
3132
_MAX_MATRIX_OUTPUT_DIGITS = 32_768
3233

@@ -213,15 +214,32 @@ def _integer_matrix(value: object) -> fmpz_mat:
213214
return fmpz_mat([[_integer(item) for item in row] for row in entries])
214215

215216

216-
def _bounded_rational_matrix(value: object, *, maximum_digits: int) -> fmpq_mat:
217+
def _bounded_q(value: object, *, maximum_digits: int) -> fmpq:
218+
if not isinstance(value, dict) or set(value) != {"num", "den"}:
219+
raise ValueError("rational is malformed")
220+
for component in (value["num"], value["den"]):
221+
if (
222+
not isinstance(component, str)
223+
or len(component.lstrip("-")) > maximum_digits
224+
):
225+
raise ValueError("rational scalar exceeds the checker bound")
226+
return _q(value)
227+
228+
229+
def _bounded_rational_matrix(
230+
value: object,
231+
*,
232+
maximum_digits: int,
233+
maximum_dimension: int = _MAX_MATRIX_DIMENSION,
234+
) -> fmpq_mat:
217235
if not isinstance(value, dict):
218236
raise ValueError("rational matrix is malformed")
219237
entries = value.get("entries")
220238
if (
221239
not isinstance(entries, list)
222-
or not 1 <= len(entries) <= _MAX_MATRIX_DIMENSION
240+
or not 1 <= len(entries) <= maximum_dimension
223241
or not isinstance(entries[0], list)
224-
or not 1 <= len(entries[0]) <= _MAX_MATRIX_DIMENSION
242+
or not 1 <= len(entries[0]) <= maximum_dimension
225243
):
226244
raise ValueError("rational matrix exceeds the checker dimension bound")
227245
for row in entries:
@@ -950,10 +968,19 @@ def _matrix_determinant(source: dict[str, Any], result: dict[str, Any]) -> bool:
950968
"FRACTION_FREE_BAREISS"
951969
):
952970
return False
953-
matrix = _matrix_source(source)
971+
if set(source) != {"matrix"}:
972+
return False
973+
matrix = _bounded_rational_matrix(
974+
source["matrix"],
975+
maximum_digits=_MAX_MATRIX_INPUT_DIGITS,
976+
maximum_dimension=_MAX_DETERMINANT_MATRIX_DIMENSION,
977+
)
954978
if matrix.nrows() != matrix.ncols():
955979
return False
956-
return bool(_q(result["determinant"]) == matrix.det())
980+
declared = _bounded_q(
981+
result["determinant"], maximum_digits=_MAX_MATRIX_OUTPUT_DIGITS
982+
)
983+
return bool(declared == matrix.det())
957984

958985

959986
def check_matrix_determinant(request: dict[str, Any]) -> dict[str, Any]:

tests/component/checkers/test_exact_domain_checker_attacks.py

Lines changed: 33 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -32,7 +32,7 @@ def test_exact_domain_checker_accepts_independent_replay(
3232
assert checker(checker_request)["accepted"] is True
3333

3434

35-
def test_matrix_determinant_checker_accepts_supported_large_canonical_result() -> None:
35+
def test_matrix_determinant_checker_accepts_order_64_large_canonical_result() -> None:
3636
diagonal_entry = "1" + "0" * 255
3737
zero = {"num": "0", "den": "1"}
3838
source = {
@@ -42,9 +42,9 @@ def test_matrix_determinant_checker_accepts_supported_large_canonical_result() -
4242
"entries": [
4343
[
4444
({"num": diagonal_entry, "den": "1"} if row == column else zero)
45-
for column in range(32)
45+
for column in range(64)
4646
]
47-
for row in range(32)
47+
for row in range(64)
4848
],
4949
}
5050
}
@@ -53,14 +53,43 @@ def test_matrix_determinant_checker_accepts_supported_large_canonical_result() -
5353
"matrix.determinant.flint-replay",
5454
source,
5555
{
56-
"determinant": {"num": "1" + "0" * (255 * 32), "den": "1"},
56+
"determinant": {"num": "1" + "0" * (255 * 64), "den": "1"},
5757
"method": "FRACTION_FREE_BAREISS",
5858
},
5959
)
6060

6161
assert check_matrix_determinant(request)["accepted"] is True
6262

6363

64+
def test_matrix_determinant_checker_rejects_order_above_64() -> None:
65+
zero = {"num": "0", "den": "1"}
66+
one = {"num": "1", "den": "1"}
67+
source = {
68+
"matrix": {
69+
"matrix_schema_version": "1",
70+
"domain": "QQ",
71+
"entries": [
72+
[one if row == column else zero for column in range(65)]
73+
for row in range(65)
74+
],
75+
}
76+
}
77+
request = _request(
78+
"matrix.determinant.compute",
79+
"matrix.determinant.flint-replay",
80+
source,
81+
{
82+
"determinant": one,
83+
"method": "FRACTION_FREE_BAREISS",
84+
},
85+
)
86+
87+
decision = check_matrix_determinant(request)
88+
89+
assert decision["accepted"] is False
90+
assert decision["conclusion"] == "UNKNOWN"
91+
92+
6493
@pytest.mark.parametrize(("checker", "checker_request"), _CASES)
6594
def test_exact_domain_checker_rejects_candidate_mutation(
6695
checker: Callable[[dict[str, Any]], dict[str, Any]],

tests/component/providers/matrix/test_matrix_capabilities.py

Lines changed: 66 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -43,6 +43,23 @@ def _matrix(rows: list[list[int | Fraction]]) -> dict[str, Any]:
4343
}
4444

4545

46+
def _truncated_legendre_matrix(prime: int) -> dict[str, Any]:
47+
order = (prime - 5) // 2
48+
49+
def entry(row: int, column: int) -> int:
50+
residue = (row - column) % prime
51+
character = (
52+
0
53+
if residue == 0
54+
else (1 if pow(residue, (prime - 1) // 2, prime) == 1 else -1)
55+
)
56+
return 1 + character
57+
58+
return _matrix(
59+
[[entry(row, column) for column in range(order)] for row in range(order)]
60+
)
61+
62+
4663
def _reference_determinant(rows: list[list[Fraction]]) -> Fraction:
4764
total = Fraction(0)
4865
for permutation in permutations(range(len(rows))):
@@ -183,6 +200,55 @@ def test_matrix_determinant_verify_independently_recomputes_exact_value(
183200
assert verified.assurance.level is CapabilityAssuranceLevel.VERIFIED
184201

185202

203+
def test_matrix_determinant_computes_and_verifies_order_33_sun_conjecture_case(
204+
matrix_checker_services: _MatrixRuntime,
205+
) -> None:
206+
"""Reproduce Yang--Yang--Zhang, arXiv:2606.22548, Theorem 1.1 at p=71."""
207+
208+
matrix = _truncated_legendre_matrix(71)
209+
computed = matrix_checker_services.core.capabilities.invoke(
210+
CapabilityRequest(
211+
capability_id="matrix.determinant.compute",
212+
input={"matrix": matrix},
213+
)
214+
)
215+
verified = matrix_checker_services.core.capabilities.invoke(
216+
CapabilityRequest(
217+
capability_id="matrix.determinant.verify",
218+
mode=CapabilityMode.VERIFY,
219+
input={
220+
"input": {"matrix": matrix},
221+
"candidate": computed.output["result"],
222+
},
223+
)
224+
)
225+
226+
assert computed.output["result"]["determinant"] == _rational(529)
227+
assert computed.assurance.level is CapabilityAssuranceLevel.COMPUTED
228+
assert verified.execution.status is ExecutionStatus.COMPLETED
229+
assert verified.output["status"] == "VERIFIED"
230+
assert verified.output["conclusion"] == "TRUE"
231+
assert verified.assurance.level is CapabilityAssuranceLevel.VERIFIED
232+
233+
234+
def test_matrix_determinant_rejects_order_above_64(
235+
matrix_services: _MatrixRuntime,
236+
) -> None:
237+
matrix = _matrix(
238+
[[1 if row == column else 0 for column in range(65)] for row in range(65)]
239+
)
240+
241+
result = matrix_services.core.capabilities.invoke(
242+
CapabilityRequest(
243+
capability_id="matrix.determinant.compute",
244+
input={"matrix": matrix},
245+
)
246+
)
247+
248+
assert result.execution.status is ExecutionStatus.ERROR
249+
assert result.diagnostics[0].code == "INVALID_REQUEST"
250+
251+
186252
def test_matrix_determinant_verify_rejects_wrong_bound_value(
187253
matrix_checker_services: _MatrixRuntime,
188254
) -> None:

0 commit comments

Comments
 (0)