Checked exact results¶
Use dense.gcd_checked, sparse.divide_checked, and the other checked producers
when you need both a polynomial answer and evidence for an independent check.
They accept the same coefficient sequences and sparse terms as ordinary
operations. Domains are inferred, and integer division and interpolation promote
to rational coefficients.
Import exact from poly to inspect and verify a result. exact.value(result)
returns a GCD, resultant, or interpolant. Division has quotient, quotients,
and remainder; factorization has unit and factors. Every polynomial
accessor returns independent storage in the original dense or sparse shape.
A dense resultant is a constant array, with the canonical empty array for zero.
resultant_certified retains the determinant transcript for a stronger check;
resultant_checked retains the existing ideal identity. Sparse checked GCDs
accept method="modular"; checked division accepts order= and axes=.
factor_checked supports integers, rationals, Gaussian rationals and prime-field
coefficients, including repeated factors. It also supports univariate and
multivariate AA and QQbar inputs. squarefree_checked
supports all these domains, promoting integers to rationals. Dense inputs are univariate;
sparse inputs can have any number of axes. One-axis sparse squarefree results
retain the existing dense evidence format; multiaxis results retain sparse
blocks. Functional extraction and checking work the same way for both.
What a successful check establishes¶
| Producer | Claim verified by exact.check |
|---|---|
gcd_checked |
A common divisor with coprime cofactors, hence a GCD up to a unit; also handles two zero inputs |
coprimality |
The two inputs have no common nonunit factor |
Dense divide_checked |
The quotient/remainder identity and degree bound |
Sparse divide_checked, divide_many_checked |
The ordered quotient/remainder identity; no claim of a unique or reduced remainder |
resultant_checked |
An identity expressing the returned polynomial as a combination of the inputs; not the determinant definition of the resultant |
resultant_certified |
The full Sylvester determinant, over QQ, QQi, GF(p), AA, and QQbar; integer inputs promote to QQ |
factor_checked over AA or QQbar |
Complete normalized irreducible factorization, including positive multiplicities and strict factor ordering |
factor_checked over other domains |
Unit times the powered factors equals the input; no irreducibility claim |
squarefree_checked |
The same product identity; no squarefreeness claim |
interpolate_checked, hermite_interpolate_checked |
Distinct nodes, the degree bound, and every supplied value or derivative constraint |
coprimality returns None when the inputs have a common factor. A returned
certificate still needs checking. algebraic.compare_checked and
algebraic.sign_checked use algebraic.check for their exact ordering evidence.
For algebraic factorization, the facade checker validates coefficient witnesses,
monicity, and reconstruction. Univariate irreducibility follows from degree and
negative real quadratic discriminants. Multivariate results retain auxiliary
image factorizations, which the checker validates before exhausting candidate
proper divisors. It never calls the factorization producer, but the exhaustive
check can require exponential work. Keep the complete Result for this claim:
evidence() exposes the core product certificate. The underlying core
check_factorization and check_multivariate_factorization keep their
product-only contracts.
Results retain their original operands and share storage when copied.
evidence() borrows an immutable core witness. An explicit certificate copy is
useful for interoperability; its allocation is outside the facade's work budget.
Result construction, functional accessors, and checks accept either a shared
Budget or max_steps=. A limit raises an error, never an unchecked answer.
See the walkthrough for a complete example.
Result¶
@fieldwise_init
struct Result[k: Int, P: Copyable & Deinitable, is_sparse: Bool, E: Copyable & Deinitable](_Archive, Copyable, Movable)
An exact result retaining its original operands and immutable evidence.
Use the functional value, quotient, remainder, factors and check helpers. The checker’s claim depends on the operation that produced the result. Multivariate algebraic factorization also retains image certificates internally; keep the complete Result for its irreducibility check.
Parameters.
k: The inferred exact coefficient kind.P: The original sparse power shape, or Int for dense arrays.is_sparse: Whether output polynomials use sparse arrays.E: The retained core evidence type.
Defined in src/poly/exact.mojo.
Result.evidence¶
def evidence(self) -> ref[ImmOrigin(origin_of(self._data[].proof))] Self.E
Borrow the evidence for an independent core checker.
This is the core product certificate for sparse algebraic factorization. Auxiliary irreducibility certificates remain in the complete Result consumed by exact.check.
Returns. Immutable evidence; copy it explicitly for mutable interoperability.
check¶
def check[k: Int, P: Copyable & Deinitable, is_sparse: Bool, E: Copyable & Deinitable](result: Result[k, P, is_sparse, E], mut budget: Budget) raises PolyError -> Bool
Verify the exact relation claimed by a retained algebra result.
GCD checks establish maximality up to a unit. Resultant checks establish an ideal-membership identity or the full determinant when produced by resultant_certified. Factorization checks over AA and QQbar also establish normalized irreducible factors with exact multiplicities. Other factorization checks establish product identities only; squarefree checks do not establish squarefreeness.
Parameters.
k: Inferred from the input types unless explicitly supplied.P: Inferred from the input types unless explicitly supplied.is_sparse: Inferred from the input types unless explicitly supplied.E: Inferred from the input types unless explicitly supplied.
Arguments.
result: The result retaining its original inputs and evidence.budget: The shared work allowance, including preparation and output storage.
Returns. Whether the retained evidence establishes the documented relation.
Raises.
PolyError: DOMAIN for incompatible input, UNSUPPORTED for an unavailable coefficient domain, or LIMIT/CAPACITY on resource limits.
Defined in src/poly/exact.mojo.
value¶
def value[k: Int, P: Copyable & Deinitable, is_sparse: Bool, E: Copyable & Deinitable](result: Result[k, P, is_sparse, E], mut budget: Budget) raises PolyError -> _Array[k, P, is_sparse]
Copy the polynomial value of a GCD, resultant, or interpolation result.
Parameters.
k: Inferred from the input types unless explicitly supplied.P: Inferred from the input types unless explicitly supplied.is_sparse: Inferred from the input types unless explicitly supplied.E: Inferred from the input types unless explicitly supplied.
Arguments.
result: The result retaining its original inputs and evidence.budget: The shared work allowance, including preparation and output storage.
Returns. An independent array in the original dense or sparse representation.
Raises.
PolyError: DOMAIN for incompatible input, UNSUPPORTED for an unavailable coefficient domain, or LIMIT/CAPACITY on resource limits.
Defined in src/poly/exact.mojo.
quotient¶
def quotient[k: Int, P: Copyable & Deinitable, is_sparse: Bool, E: Copyable & Deinitable](result: Result[k, P, is_sparse, E], mut budget: Budget) raises PolyError -> _Array[k, P, is_sparse]
Copy the quotient of a checked division.
Parameters.
k: Inferred from the input types unless explicitly supplied.P: Inferred from the input types unless explicitly supplied.is_sparse: Inferred from the input types unless explicitly supplied.E: Inferred from the input types unless explicitly supplied.
Arguments.
result: The result retaining its original inputs and evidence.budget: The shared work allowance, including preparation and output storage.
Returns. An independent coefficient array.
Raises.
PolyError: DOMAIN for incompatible input, UNSUPPORTED for an unavailable coefficient domain, or LIMIT/CAPACITY on resource limits.
Defined in src/poly/exact.mojo.
quotients¶
def quotients[k: Int, P: Copyable & Deinitable, is_sparse: Bool, E: Copyable & Deinitable](result: Result[k, P, is_sparse, E], mut budget: Budget) raises PolyError -> List[_Array[k, P, is_sparse]]
Copy all quotients in the original divisor order.
Parameters.
k: Inferred from the input types unless explicitly supplied.P: Inferred from the input types unless explicitly supplied.is_sparse: Inferred from the input types unless explicitly supplied.E: Inferred from the input types unless explicitly supplied.
Arguments.
result: The result retaining its original inputs and evidence.budget: The shared work allowance, including preparation and output storage.
Returns. Independent quotient arrays in divisor order.
Raises.
PolyError: DOMAIN for incompatible input, UNSUPPORTED for an unavailable coefficient domain, or LIMIT/CAPACITY on resource limits.
Defined in src/poly/exact.mojo.
remainder¶
def remainder[k: Int, P: Copyable & Deinitable, is_sparse: Bool, E: Copyable & Deinitable](result: Result[k, P, is_sparse, E], mut budget: Budget) raises PolyError -> _Array[k, P, is_sparse]
Copy the remainder of a checked division.
Parameters.
k: Inferred from the input types unless explicitly supplied.P: Inferred from the input types unless explicitly supplied.is_sparse: Inferred from the input types unless explicitly supplied.E: Inferred from the input types unless explicitly supplied.
Arguments.
result: The result retaining its original inputs and evidence.budget: The shared work allowance, including preparation and output storage.
Returns. An independent coefficient array.
Raises.
PolyError: DOMAIN for incompatible input, UNSUPPORTED for an unavailable coefficient domain, or LIMIT/CAPACITY on resource limits.
Defined in src/poly/exact.mojo.
cofactors¶
def cofactors[k: Int, P: Copyable & Deinitable, is_sparse: Bool, E: Copyable & Deinitable](result: Result[k, P, is_sparse, E], mut budget: Budget) raises PolyError -> Tuple[_Array[k, P, is_sparse], _Array[k, P, is_sparse]]
Copy GCD cofactors or resultant identity multipliers.
Parameters.
k: Inferred from the input types unless explicitly supplied.P: Inferred from the input types unless explicitly supplied.is_sparse: Inferred from the input types unless explicitly supplied.E: Inferred from the input types unless explicitly supplied.
Arguments.
result: The result retaining its original inputs and evidence.budget: The shared work allowance, including preparation and output storage.
Returns. The GCD input quotients, or the multipliers u and v in ua + vb = resultant.
Raises.
PolyError: DOMAIN for incompatible input, UNSUPPORTED for an unavailable coefficient domain, or LIMIT/CAPACITY on resource limits.
Defined in src/poly/exact.mojo.
unit¶
def unit[k: Int, P: Copyable & Deinitable, is_sparse: Bool, E: Copyable & Deinitable](result: Result[k, P, is_sparse, E], mut budget: Budget) raises PolyError -> _Scalar[k]
Copy the factorization scalar.
Parameters.
k: Inferred from the input types unless explicitly supplied.P: Inferred from the input types unless explicitly supplied.is_sparse: Inferred from the input types unless explicitly supplied.E: Inferred from the input types unless explicitly supplied.
Arguments.
result: The result retaining its original inputs and evidence.budget: The shared work allowance, including preparation and output storage.
Returns. The scalar multiplier.
Raises.
PolyError: DOMAIN for incompatible input, UNSUPPORTED for an unavailable coefficient domain, or LIMIT/CAPACITY on resource limits.
Defined in src/poly/exact.mojo.
factors¶
def factors[k: Int, P: Copyable & Deinitable, is_sparse: Bool, E: Copyable & Deinitable](result: Result[k, P, is_sparse, E], mut budget: Budget) raises PolyError -> List[Tuple[_Array[k, P, is_sparse], Int]]
Copy factor polynomials and their positive multiplicities.
Parameters.
k: Inferred from the input types unless explicitly supplied.P: Inferred from the input types unless explicitly supplied.is_sparse: Inferred from the input types unless explicitly supplied.E: Inferred from the input types unless explicitly supplied.
Arguments.
result: The result retaining its original inputs and evidence.budget: The shared work allowance, including preparation and output storage.
Returns. Independent factor arrays in deterministic core order.
Raises.
PolyError: DOMAIN for incompatible input, UNSUPPORTED for an unavailable coefficient domain, or LIMIT/CAPACITY on resource limits.
Defined in src/poly/exact.mojo.
Save a complete result with io.dumps(result) and restore it with
io.loads[type_of(result)](text). Loading verifies the retained operands and
certificate before returning. See checked archives.
Certificate¶
@fieldwise_init
struct Certificate[C: CoefficientRing](Copyable, Movable, Writable)
A Sylvester determinant value with every exact elimination identity.
Defined in src/poly/_determinant.mojo.
| Field | Type | |
|---|---|---|
variable |
Int64 |
The eliminated variable. |
resultant |
SparsePoly[Self.C] |
The exact determinant, including its sign. |
steps |
List[Step[Self.C]] |
The fraction-free elimination transcript in forward order. |
Step¶
@fieldwise_init
struct Step[C: CoefficientRing](Copyable, Movable, Writable)
One exact fraction-free elimination step on the current trailing matrix.
Defined in src/poly/_determinant.mojo.
| Field | Type | |
|---|---|---|
pivot_row |
Int |
The row swapped into position zero, or minus one for an all-zero first column. |
trailing |
List[List[SparsePoly[Self.C]]] |
The next trailing matrix, empty for a singular termination. |