Core API

Cylindrical algebraic decomposition¶

For the array workflow, see inequalities and CAD.

Final-data construction¶

cad_final builds a complete CAD and independently verifies its final data before returning. Its default combines Brown–McCallum projection reductions with Lazard lifting, one algebraic field per base sample, relative sections and bounded interval-first root isolation. The verifier checks projection, specialization, root completeness, geometry and original-input signs; it does not replay intermediate construction proofs. Checked exact SIMD batches accelerate eligible rational sign evaluations, with scalar and arbitrary-precision fallbacks.

CADFinalCertificate is the evidence returned by poly.cad.decompose and poly.cad.cover. It exposes metadata methods and explicit cells(budget) and sample(budget) materialization. check_cad_final binds inputs, order, fixed prefix and conjunction independently. Explicit McCallum requests and fixed prefixes retain the compatible legacy backend and undergo its complete check.

`CADFinalCell`¶

@fieldwise_init
struct CADFinalCell(Copyable, Movable)

An absolute cell coordinate and labels, without intermediate proofs.

The enclosing CADFinalCertificate proves geometry and completeness. This output value is not a replacement for that certificate.

Defined in src/polynomials/cad_final_types.mojo.

Field	Type
`parent`	`Int`	Parent index in the materialized breadth-first list; -1 at its root.
`level`	`Int`	Zero-based coordinate level; -1 for the root placeholder.
`position`	`Int`	Alternating stack position: sectors are even and sections are odd.
`sample`	`RealAlgebraic`	The absolute last coordinate, computed only on an output request.
`signs`	`List[Int]`	Original-input signs on terminal cells; empty on other levels.

`CADFinalCertificate`¶

@fieldwise_init
struct CADFinalCertificate(Copyable, Movable)

Immutable retained evidence for a complete decomposition or conjunction.

Inspect geometry through cells(), and metadata through variables(), factor_counts(), cell_count() and stack_count(). Compact evidence keeps relative roots until cells() requests absolute coordinates. A legacy payload supports explicit McCallum, fixed prefixes and old archives. Independent acceptance always binds the original inputs, variable order, fixed prefix and query through check_cad_final.

Defined in src/polynomials/cad_final.mojo.

`CADFinalCertificate.is_compact`¶

def is_compact(self) -> Bool

Report whether the retained representation uses relative sections.

Returns. True for compact final evidence, False for compatible legacy evidence.

`CADFinalCertificate.is_covering`¶

def is_covering(self) -> Bool

Report whether the claim includes a sign conjunction.

Returns. True for a full-CAD conjunction claim.

`CADFinalCertificate.variables`¶

def variables(self, mut budget: Budget) raises PolyError -> List[Int64]

Copy the cylindrical variable order.

Arguments.

budget: Shared storage and work allowance.

Returns. Variables in base-to-top order.

Raises.

PolyError: DOMAIN for missing evidence, LIMIT/CAPACITY on resource limits.

`CADFinalCertificate.factor_counts`¶

def factor_counts(self, mut budget: Budget) raises PolyError -> List[Int]

Count the retained projection factors at each level.

Arguments.

budget: Shared storage and work allowance.

Returns. Factor counts in cylindrical order.

Raises.

PolyError: DOMAIN for missing evidence, LIMIT/CAPACITY on resource limits.

`CADFinalCertificate.cell_count`¶

def cell_count(self, mut budget: Budget) raises PolyError -> Int

Count all cells, including the root, without materializing samples.

Arguments.

budget: Shared traversal allowance.

Returns. The number of retained cells at all levels.

Raises.

PolyError: DOMAIN for missing evidence, LIMIT/CAPACITY on resource limits.

`CADFinalCertificate.stack_count`¶

def stack_count(self) -> Int

Count retained stacks without constructing output coordinates.

Returns. The number of stacks, or zero for an empty invalid representation.

`CADFinalCertificate.satisfiable`¶

def satisfiable(self) -> Bool

Read the retained conjunction truth value.

Returns. True when the retained covering contains a witness; False for a decomposition-only claim.

`CADFinalCertificate.cells`¶

def cells(self, mut budget: Budget) raises PolyError -> List[CADFinalCell]

Materialize absolute coordinates once per retained cell.

Arguments.

budget: Shared allowance including absolute root construction.

Returns. Breadth-first geometry, beginning with a root placeholder. Its signs belong to the bound original inputs.

Raises.

PolyError: DOMAIN for missing evidence, LIMIT/CAPACITY on resource limits.

`CADFinalCertificate.legacy_decomposition`¶

def legacy_decomposition(self) -> ref[ImmOrigin(origin_of(self._data[].legacy))] Optional[CADCertificate]

Borrow a retained legacy decomposition for compatible archive transport.

Returns. The optional legacy payload; absent for compact evidence and coverings.

`CADFinalCertificate.sample`¶

def sample(self, mut budget: Budget) raises PolyError -> Optional[List[RealAlgebraic]]

Materialize a satisfying path without converting the other cells.

Arguments.

budget: Shared coordinate construction and storage allowance.

Returns. Absolute coordinates in cylindrical order, or None without a satisfying conjunction.

Raises.

PolyError: DOMAIN for malformed evidence, LIMIT/CAPACITY on resource limits.

`CADFinalCertificate.legacy_covering`¶

def legacy_covering(self) -> ref[ImmOrigin(origin_of(self._data[].covering))] Optional[CADCoveringCertificate]

Borrow a retained legacy covering for compatible archive transport.

Returns. The optional legacy payload; absent for compact evidence and decompositions.

`CADFinalCertificate.compact_bytes`¶

def compact_bytes(self, mut budget: Budget) raises PolyError -> List[UInt8]

Encode compact final data in the version-one QCF payload.

Arguments.

budget: Shared encoding and output storage allowance.

Returns. Exact final-data bytes, excluding producer search counters. The enclosing archive must bind and verify the claim.

Raises.

PolyError: DOMAIN for a legacy representation, LIMIT/CAPACITY on resource limits.

`CADFinalCertificate.from_compact_bytes`¶

@staticmethod
def from_compact_bytes(data: Span[UInt8, _], inputs: List[SparsePoly[QQ]], variables: List[Int64], masks: List[UInt8], query: Bool, mut budget: Budget) raises PolyError -> Self

Decode and independently accept a compact full-space claim.

Arguments.

data: Exact QCF payload with no trailing bytes.
inputs: Original polynomials supplied by the caller.
variables: Expected cylindrical order.
masks: Expected conjunction masks, or empty for a decomposition.
query: Whether the caller requests a conjunction claim.
budget: Shared decoding and complete verification allowance.

Returns. Accepted compact evidence; no producer assertions are trusted.

Raises.

PolyError: ENCODING for rejected evidence, LIMIT/CAPACITY on resource limits.

`CADFinalCertificate.from_legacy`¶

@staticmethod
def from_legacy(var proof: CADCertificate, inputs: List[SparsePoly[QQ]], fixed: List[RealAlgebraic], mut budget: Budget) raises PolyError -> Self

Accept and retain an old decomposition without regenerating it.

Arguments.

proof: Owned historical decomposition evidence.
inputs: Original polynomial family.
fixed: Expected fixed coordinate prefix.
budget: Shared complete verification and storage allowance.

Returns. Accepted legacy evidence in the new result interface.

Raises.

PolyError: ENCODING for rejected evidence, LIMIT/CAPACITY on resource limits.

`CADFinalCertificate.from_legacy_covering`¶

@staticmethod
def from_legacy_covering(var proof: CADCoveringCertificate, inputs: List[SparsePoly[QQ]], masks: List[UInt8], fixed: List[RealAlgebraic], mut budget: Budget) raises PolyError -> Self

Accept and retain an old full covering without regenerating it.

Arguments.

proof: Owned historical covering evidence.
inputs: Original polynomial family.
masks: Expected conjunction masks.
fixed: Expected fixed coordinate prefix.
budget: Shared complete verification and storage allowance.

Returns. Accepted legacy covering in the new result interface.

Raises.

PolyError: ENCODING for rejected evidence, LIMIT/CAPACITY on resource limits.

`cad_final`¶

def cad_final(inputs: List[SparsePoly[QQ]], variables: List[Int64], mut budget: Budget, *, fixed: List[RealAlgebraic] = List[RealAlgebraic](), masks: List[UInt8] = List[UInt8](), query: Bool = False, lazard: Optional[Bool] = None) raises PolyError -> CADFinalCertificate

Construct a full CAD and accept its final evidence before returning.

Arguments.

inputs: Original polynomial family.
variables: All variables in base-to-top order.
budget: Complete allowance, including construction retries and final verification.
fixed: Section prefix; a nonempty prefix uses the checked legacy backend.
masks: Allowed sign masks for a conjunction; empty for decomposition only.
query: Request a full-decomposition conjunction result.
lazard: None selects Revision 15 with interval lifting; True selects plain Lazard with interval lifting; False selects checked legacy McCallum.

Returns. Only independently accepted evidence. Relative terminal sections remain unmaterialized on the compact backend.

Raises.

PolyError: DOMAIN for invalid input, UNSUPPORTED for legacy nullification, LIMIT/CAPACITY on resource limits.

Defined in src/polynomials/cad_final.mojo.

`check_cad_final`¶

def check_cad_final(inputs: List[SparsePoly[QQ]], variables: List[Int64], masks: List[UInt8], certificate: CADFinalCertificate, mut budget: Budget, *, fixed: List[RealAlgebraic] = List[RealAlgebraic](), query: Bool = False, vectorized: Bool = True) raises PolyError -> Bool

Independently verify a complete retained CAD against the requested scope.

Arguments.

inputs: Original polynomial family.
variables: Expected cylindrical variable order.
masks: Conjunction masks, or empty for decomposition only.
certificate: Retained compact or compatible legacy evidence.
budget: Shared complete verification allowance.
fixed: Expected section prefix; empty means all real space.
query: Whether the claim includes the conjunction's truth.
vectorized: Use checked exact rational SIMD batches; False selects the scalar reference.

Returns. Whether the whole certificate proves this exact requested claim.

Raises.

PolyError: LIMIT/CAPACITY on resource limits; neither permits acceptance.

Defined in src/polynomials/cad_final.mojo.

Legacy certificates¶

cad constructs a complete sign-invariant decomposition of real coordinate space. Variables are supplied in base-to-top order; every input variable must occur in that list. Extra variables are allowed. Inputs may share factors, contain repeated factors, be constant, or be zero. The producer builds primitive squarefree pairwise coprime projection bases before lifting.

McCallum projection includes each member's coefficients from the leading one down to the first nonzero constant (every coefficient when none is constant), discriminants and pairwise resultants. check_cad_projection also accepts the full coefficient set in older certificates. Lazard projection includes leading and trailing coefficients, discriminants and pairwise resultants. Both use Res(f,f') in place of the discriminant: the extra leading-coefficient factor is already projected. Projection certificates prove the Sylvester determinants, not merely membership in the input ideal. Their checkers verify fraction-free multiplication identities without repeating exact elimination division.

Lazard lifting removes vanishing factors before each successive substitution. The implementation uses the first nonzero Taylor derivative at each prefix; the result differs from division by linear factors only by a positive factorial scalar. All earlier zero derivatives and the first nonzero derivative are certified. This handles algebraic coordinates and nullification exactly.

McCallum mode fails with UNSUPPORTED on nullification except at the final lifting level over a point base. In particular, it does not claim order invariance for a nullified intermediate projection polynomial. Use lazard=True for such inputs.

Fix leading algebraic coordinates¶

CADFiber(fixed, budget) binds an exact prefix in the supplied variable order. Its decompose, cover, solve, and decompose_to methods follow only those sections, then cover or search the remaining coordinates. Include each fixed coordinate's defining polynomial in the input family: a prefix coordinate must be a projection section, not a point inside a sector. Invalid witnesses, excess coordinates, and a nonsection prefix raise DOMAIN when encountered. Valid witnesses for the same value may use different defining polynomials or isolating intervals; their equality is checked independently.

Use the same CADFiber with check or checker to verify its results. These methods retain the ordinary certificate and stream layouts, but their claim is coverage over the bound prefix. Ordinary check_cad still requires full-space coverage. An empty prefix recovers the ordinary traversal. All preparation, copying, computation, and checking share the supplied budget.

The coefficient-array interface prepares and checks this prefix automatically for AA coefficients and user-supplied fixed= coordinates. Most callers can use poly.cad directly; the workflow tutorial shows how to select a slice without constructing core witnesses.

`CADFiber`¶

struct CADFiber(Copyable, Movable)

Bind a zero-dimensional section prefix for CAD generation and checking.

Each coordinate must be a section of its projection stack. Include a defining polynomial for each value among the inputs. Equivalent witnesses may use different defining polynomials or isolating intervals. Coordinates follow the leading variables in base-to-top order; an empty prefix covers all real space.

Defined in src/polynomials/cad_fiber.mojo.

`CADFiber.init`¶

def __init__(out self, fixed: List[RealAlgebraic], mut budget: Budget) raises PolyError

Validate and copy the requested algebraic coordinate prefix.

Arguments.

fixed: Exact coordinates for the leading cylindrical variables.
budget: The shared validation and storage allowance.

Raises.

PolyError: DOMAIN for invalid witnesses, LIMIT or CAPACITY on work limits.

`CADFiber.decompose`¶

def decompose(self, inputs: List[SparsePoly[QQ]], variables: List[Int64], mut budget: Budget, lazard: Bool = False) raises PolyError -> CADCertificate

Decompose all remaining coordinates over the fixed section prefix.

Arguments.

inputs: Rational polynomials, including defining polynomials for the prefix.
variables: All variables in base-to-top order, with fixed coordinates first.
budget: The shared work and storage allowance.
lazard: Whether to use Lazard projection and lifting.

Returns. Evidence covering the specified fiber; check it with this CADFiber.

Raises.

PolyError: DOMAIN for invalid inputs or a prefix outside projection sections, UNSUPPORTED for McCallum nullification, LIMIT or CAPACITY on work limits.

`CADFiber.cover`¶

def cover(self, inputs: List[SparsePoly[QQ]], masks: List[UInt8], variables: List[Int64], mut budget: Budget, lazard: Bool = False) raises PolyError -> CADCoveringCertificate

Decide a conjunction with a full decomposition of the requested fiber.

Arguments.

inputs: Rational polynomials, including defining polynomials for the prefix.
masks: Allowed sign bits per input: 1 for negative, 2 for zero, 4 for positive.
variables: All variables in base-to-top order, with fixed coordinates first.
budget: The shared work and storage allowance.
lazard: Whether to use Lazard projection and lifting.

Returns. Evidence covering the specified fiber; check it with this CADFiber.

Raises.

PolyError: DOMAIN for invalid inputs or a prefix outside projection sections, UNSUPPORTED for McCallum nullification, LIMIT or CAPACITY on work limits.

`CADFiber.solve`¶

def solve(self, inputs: List[SparsePoly[QQ]], masks: List[UInt8], variables: List[Int64], mut budget: Budget, lazard: Bool = False) raises PolyError -> CylindricalCoveringCertificate

Search only the requested fiber for a witness or conflict covering.

Arguments.

inputs: Rational polynomials, including defining polynomials for the prefix.
masks: Allowed sign bits per input: 1 for negative, 2 for zero, 4 for positive.
variables: All variables in base-to-top order, with fixed coordinates first.
budget: The shared work and storage allowance.
lazard: Whether to use Lazard projection and lifting.

Returns. Evidence covering the specified fiber; check it with this CADFiber.

Raises.

PolyError: DOMAIN for invalid inputs or a prefix outside projection sections, UNSUPPORTED for McCallum nullification, LIMIT or CAPACITY on work limits.

`CADFiber.search`¶

def search(self, inputs: List[SparsePoly[QQ]], masks: List[UInt8], variables: List[Int64], mut budget: Budget, lazard: Bool = False) raises PolyError -> CADCoveringsCertificate

Decide the conjunction on the fiber by a conflict-driven search over cylindrical coverings.

Arguments.

inputs: Rational polynomials over all variables.
masks: Allowed sign bits per input: 1 for negative, 2 for zero, 4 for positive.
variables: All variables in base-to-top order, with fixed coordinates first.
budget: The shared work and storage allowance.
lazard: Whether to use Lazard characterizations; False selects McCallum's.

Returns. A witness on the fiber or a covering of it; check it with this CADFiber.

Raises.

PolyError: DOMAIN for invalid inputs, UNSUPPORTED for McCallum nullification, LIMIT or CAPACITY on work limits.

`CADFiber.check`¶

def check(self, inputs: List[SparsePoly[QQ]], masks: List[UInt8], certificate: CADCoveringsCertificate, mut budget: Budget) raises PolyError -> Bool

Verify a coverings witness or covering on exactly the bound prefix.

Arguments.

inputs: The original rational polynomial family.
masks: The original allowed-sign masks.
certificate: The proposed witness or covering.
budget: The shared verification allowance.

Returns. Whether the certificate proves its verdict on the fiber.

Raises.

PolyError: LIMIT or CAPACITY on work limits, DOMAIN for invalid masks.

`CADFiber.check`¶

def check(self, inputs: List[SparsePoly[QQ]], certificate: CADCertificate, mut budget: Budget) raises PolyError -> Bool

Verify the geometric claim on exactly the bound section prefix.

Arguments.

inputs: The original rational polynomial family.
certificate: The proposed decomposition or feasibility evidence.
budget: The shared verification allowance.

Returns. Whether local witnesses, prefix binding, and required coverage are valid.

Raises.

PolyError: LIMIT or CAPACITY on work limits.

`CADFiber.check`¶

def check(self, inputs: List[SparsePoly[QQ]], masks: List[UInt8], certificate: CADCoveringCertificate, mut budget: Budget) raises PolyError -> Bool

Verify the geometric claim on exactly the bound section prefix.

Arguments.

inputs: The original rational polynomial family.
masks: The original allowed-sign masks.
certificate: The proposed decomposition or feasibility evidence.
budget: The shared verification allowance.

Returns. Whether local witnesses, prefix binding, and required coverage are valid.

Raises.

PolyError: LIMIT or CAPACITY on work limits, DOMAIN for invalid masks.

`CADFiber.check`¶

def check(self, inputs: List[SparsePoly[QQ]], masks: List[UInt8], certificate: CylindricalCoveringCertificate, mut budget: Budget) raises PolyError -> Bool

Verify the geometric claim on exactly the bound section prefix.

Arguments.

inputs: The original rational polynomial family.
masks: The original allowed-sign masks.
certificate: The proposed decomposition or feasibility evidence.
budget: The shared verification allowance.

Returns. Whether local witnesses, prefix binding, and required coverage are valid.

Raises.

PolyError: LIMIT or CAPACITY on work limits, DOMAIN for invalid masks.

`CADFiber.decompose_to`¶

def decompose_to[S: CADSink](self, inputs: List[SparsePoly[QQ]], variables: List[Int64], mut sink: S, mut budget: Budget, lazard: Bool = False) raises PolyError -> CADStreamReceipt

Stream complete local stacks and terminal signs for the requested fiber.

Parameters.

S: The witness destination type.

Arguments.

inputs: Rational polynomials including the prefix's defining polynomials.
variables: All variables in base-to-top order, fixed coordinates first.
sink: The consumer of the projection header and depth-first events.
budget: The shared computation and transport allowance.
lazard: Whether to use Lazard projection and lifting.

Returns. Counts of visited stacks and terminal cells, requiring a matching fiber checker.

Raises.

PolyError: DOMAIN for invalid inputs or a nonsection prefix, UNSUPPORTED for McCallum nullification, LIMIT or CAPACITY on work limits; failure may leave an incomplete destination.

`CADFiber.checker`¶

def checker(self, inputs: List[SparsePoly[QQ]], mut budget: Budget) raises PolyError -> CADStreamChecker

Prepare incremental verification bound to the requested section prefix.

Arguments.

inputs: The original rational polynomial family.
budget: The shared preparation allowance.

Returns. A checker requiring every branch after the fixed prefix, and no other prefix branch.

Raises.

PolyError: DOMAIN for invalid input, LIMIT or CAPACITY on work limits.

Reading cells and certificates¶

The decomposition's root cell has index 0, level -1 and no coordinate. Other cells have a parent, coordinate level and alternating stack position: even positions are open sectors and odd positions are sections. Each stack lists all distinct roots at the base sample. Its sources pair identifies the basis polynomial and its root index: boundaries denote those root functions over the whole base cell, not fixed numerical sample values. In Lazard mode the root functions are those of the certified Lazard evaluation.

Following parent indices recovers a sample tuple. The geometric dimension is the number of sector positions on that path. Terminal cells contain certified evaluations and signs for the original input family. Projection theorems, complete root lists, order/equality proofs and stack coverage establish that these signs hold throughout each cell. Sample-point signs alone are insufficient.

cad_cell lifts only the path containing an exact query point. It uses the same global projection closure and complete local stacks; it does not build unrelated branches. Its checker also verifies point containment at every coordinate.

cad_covering decides a conjunction of polynomial sign conditions. Masks use bit 1 for negative, 2 for zero and 4 for positive; unions express non-strict inequalities or disequality. A nonnegative witness_cell identifies a satisfying terminal cell. Otherwise every terminal cell names a violated constraint, and the certified decomposition covers all real space. This implementation uses a complete CAD for coverings.

cylindrical_covering provides the selective alternative. It retains a global projection closure, samples uncovered intervals (zero first, then exterior sectors and gaps), and stops at a satisfying assignment. A violated constraint excludes the interval between its own factor roots, crossing boundaries of unrelated polynomials. Such intervals may overlap. Constraints decided at an earlier coordinate exclude entire cylinders, avoiding later lifting.

CylindricalCoveringCertificate stores only visited cells and local stacks. Conflict intervals refer to inclusive ranges of alternating stack positions; their parity encodes open or closed finite endpoints. Input-factor identities and root mappings justify crossing irrelevant boundaries. For infeasibility, the checker combines intervals and completed children from leaves to root and requires every parent stack position to be covered. For feasibility, it checks the complete assignment and all constraint signs. Constant contradictions need no stack. No producer or search is invoked by this checker.

coverings_solve decides a conjunction without any global projection, by the conflict-driven search over cylindrical algebraic coverings of Ábrahám, Davenport, England and Kremer (2021). It assigns one coordinate at a time and stops at the first satisfying point. A constraint is delineated only once it fails at a candidate sample; a level whose samples all fail returns intervals, each with the polynomials characterizing it. Their Lazard projection (leading and trailing coefficients, discriminants, and resultants with interval bounds on the sides where a polynomial has roots, and of adjacent bounds) gives the interval excluded one level down. With lazard=False the characterization uses every coefficient and McCallum nullification raises UNSUPPORTED.

CADCoveringsCertificate holds either a witness, with exact evaluations and signs of every input, or a covering tree. Each CoveringNode covers one coordinate's line above the prefix formed by its ancestors' samples, by CoveringIntervals in increasing order. A CoveringBound names a root of a listed polynomial at that prefix by its index. An interval is a single section or an open interval; it is excluded either by a constraint whose sign at the interval sample fails, or by a child covering above the sample. Supplied factorizations of the inputs and of the projection polynomials are checked by product. check_coverings recomputes every bound, requires the intervals to cover the line, finds no characterization root inside an open interval, checks conflict signs exactly, and for every child recomputes its Lazard projection (requiring nonzero discriminants) and requires each factor in the parent interval's characterization. It reuses the producer's exact root and sign routines but none of its choices. CADFiber.search and its check overload start the search and the check at the fiber's fixed prefix. poly.cad.solve returns this evidence.

All traversals use explicit worklists and budgets. Invalid certificates return false or a documented typed error; exhausted checking raises LIMIT.

cad.mojo Download

"""Construct a complete certified cylindrical decomposition of the unit circle."""
from std.testing import assert_true
from polynomials import Budget, QQ, NoContext, SparsePoly, MonomialOrder, cad, check_cad, cylindrical_covering, check_cylindrical_covering


def main() raises:
    var budget = Budget()
    var order = MonomialOrder()
    var x = SparsePoly[QQ].variable(0, order, NoContext(), budget)
    var y = SparsePoly[QQ].variable(1, order, NoContext(), budget)
    var one = SparsePoly[QQ].constant(QQ.one(NoContext()), order, budget)
    var circle = x.pow(2, budget).add(y.pow(2, budget), budget).sub(one, budget)
    var inputs: List[SparsePoly[QQ]] = [circle.copy()]
    var result = cad(inputs, [Int64(0), Int64(1)], budget, lazard=True)
    assert_true(check_cad(inputs, result, budget))
    var plane_cells = 0
    for cell in result.cells:
        if cell.level == 1:
            plane_cells += 1
    assert_true(plane_cells == 13)
    var interior = cylindrical_covering(inputs, [UInt8(1)], [Int64(0), Int64(1)], budget, lazard=True)
    assert_true(interior.witness_cell >= 0 and check_cylindrical_covering(inputs, [UInt8(1)], interior, budget))
    assert_true(len(interior.stacks) == 2)
    print("Unit-circle plane cells:", plane_cells)
    print("Projection, lifting and coverage checked")
    print("Disk interior found with two selective stacks")

Run from the repository root pixi run mojo run -I build docs/examples/cad.mojo

Output

Unit-circle plane cells: 13
Projection, lifting and coverage checked
Disk interior found with two selective stacks

`CADCell`¶

@fieldwise_init
struct CADCell(Copyable, Movable, Writable)

A cylindrical cell located by its parent and section or sector position.

Defined in src/polynomials/cad_types.mojo.

Field	Type
`parent`	`Int`	The parent cell index; minus one for the zero-dimensional root cell.
`level`	`Int`	The final coordinate level; minus one for the root cell.
`position`	`Int`	The alternating stack position; even positions are sectors, odd positions sections.
`sample`	`RealAlgebraic`	The exact last sample coordinate, with rational zero as the root-cell placeholder.
`evaluations`	`List[AlgebraicPolynomialEvaluation]`	Certified input-polynomial values at a full-dimensional coordinate tuple.
`signs`	`List[AlgebraicComparisonCertificate]`	Comparisons of those values with zero, giving signs constant on the entire cell.
`witnesses`	`List[CADSignWitness]`	One sign proof per input, or empty when every sign has an exact evaluation.

`CADCellCertificate`¶

@fieldwise_init
struct CADCellCertificate(Copyable, Movable, Writable)

A certified single sign-invariant cell containing an exact query point.

Defined in src/polynomials/cad_types.mojo.

Field	Type
`projection`	`CADProjectionCertificate`	The projection closure for the input family.
`stacks`	`List[CADStackCertificate]`	One certified stack along the query-point path at each level.
`positions`	`List[Int]`	The chosen section or sector at each level.
`evaluations`	`List[AlgebraicPolynomialEvaluation]`	The input-polynomial values at the query point.
`signs`	`List[AlgebraicComparisonCertificate]`	The constant input signs on the selected cylindrical cell.

`CADCertificate`¶

@fieldwise_init
struct CADCertificate(Copyable, Movable, Writable)

A sign-invariant cylindrical tree with exact witnesses for its checking scope.

Defined in src/polynomials/cad_types.mojo.

Field	Type
`projection`	`CADProjectionCertificate`	The complete projection closure and basis certificates.
`cells`	`List[CADCell]`	The root and retained cylindrical cells in breadth-first order.
`stacks`	`List[CADStackCertificate]`	One complete stack for every nonterminal cell, in cell order.

`CADCoveringCertificate`¶

@fieldwise_init
struct CADCoveringCertificate(Copyable, Movable, Writable)

A feasibility witness or a complete covering by cells violating a conjunction.

Defined in src/polynomials/cad_types.mojo.

Field	Type
`decomposition`	`CADCertificate`	The sign-invariant decomposition for the producer's coordinate scope.
`witness_cell`	`Int`	A satisfying terminal cell, or minus one when the conjunction is infeasible.
`violations`	`List[Int]`	For infeasibility, one violated constraint index per terminal cell in traversal order.

`CADPolynomialLift`¶

@fieldwise_init
struct CADPolynomialLift(Copyable, Movable, Writable)

A certified specialization and complete real roots of one projection basis member.

Defined in src/polynomials/cad_types.mojo.

Field	Type
`ordinary`	`Optional[AlgebraicSpecializationCertificate]`	Ordinary specialization in McCallum mode.
`lazard`	`Optional[LazardEvaluationCertificate]`	Vanishing-order evaluation in Lazard mode.
`roots`	`Optional[AlgebraicRootsCertificate]`	All specialized roots, absent only for an allowed McCallum nullification.

`CADProjectionCertificate`¶

@fieldwise_init
struct CADProjectionCertificate(Copyable, Movable, Writable)

Complete projection closure with determinant and basis normalization proofs.

Defined in src/polynomials/cad_projection.mojo.

Field	Type
`variables`	`List[Int64]`	Variables in base-to-top cylindrical order.
`lazard`	`Bool`	Whether to use leading/trailing coefficients rather than every coefficient.
`levels`	`List[List[SparsePoly[QQ]]]`	Primitive squarefree pairwise coprime bases at each main-variable level.
`factorizations`	`List[MultivariateFactorization[QQ]]`	Product identities for inputs and projection polynomials in schedule order.
`resultants`	`List[ProjectionResultantCertificate]`	Discriminant and pairwise resultant determinant transcripts.
`coprimality`	`List[CoprimalityCertificate[QQ]]`	Coprimality of each basis member with its derivative and with earlier members.

`CADSignWitness`¶

@fieldwise_init
struct CADSignWitness(Copyable, Movable, Writable)

The proof of one input's sign at a terminal sample point.

Defined in src/polynomials/cad_types.mojo.

Field	Type
`kind`	`Int`	Zero for the next exact evaluation, one for interval exclusion, two for a representation zero proof, three for a common-divisor zero proof, four for a section of a dividing top-level basis member.
`point`	`List[RealAlgebraic]`	Refined witnesses of every coordinate, for kinds one and two.
`primitive`	`Int`	For kind two, the coordinate whose field contains every other coordinate; for kind four, the index of the top-level basis member.
`representations`	`List[DensePoly[QQ]]`	For kind two, each coordinate as a rational polynomial in the primitive one; for kind three, the monic divisor's coefficients in the primitive coordinate's field, by powers of the other irrational coordinate.

`CADStackCertificate`¶

@fieldwise_init
struct CADStackCertificate(Copyable, Movable, Writable)

A complete ordered stack of sections and sectors above one base cell.

Defined in src/polynomials/cad_types.mojo.

Field	Type
`parent`	`Int`	The parent cell index in a decomposition, or the preceding path index.
`level`	`Int`	The zero-based level of the new coordinate.
`lifts`	`List[CADPolynomialLift]`	One complete specialization and root proof per basis polynomial.
`roots`	`List[RealAlgebraic]`	The distinct stack boundaries at the base sample, in increasing order.
`sources`	`List[Tuple[Int, Int]]`	For each boundary, its basis-polynomial index and specialized root index.
`mapping`	`List[List[Int]]`	The boundary index of each root of each basis polynomial.
`equalities`	`List[AlgebraicComparisonCertificate]`	Equalities binding every specialized root to its merged boundary.
`ordering`	`List[AlgebraicComparisonCertificate]`	Strict comparisons of adjacent boundaries.
`samples`	`List[RealAlgebraic]`	Alternating sector and section samples, with unbounded sectors at both ends.
`separations`	`List[AlgebraicComparisonCertificate]`	Section equalities and sector-bound comparisons in sample traversal order.

`DeterminantStep`¶

@fieldwise_init
struct DeterminantStep(Copyable, Movable, Writable)

One exact fraction-free elimination step on the current trailing matrix.

Defined in src/polynomials/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[QQ]]]`	The next trailing matrix, empty for a singular termination.

`LazardEvaluationCertificate`¶

@fieldwise_init
struct LazardEvaluationCertificate(Copyable, Movable, Writable)

Successive vanishing orders and all zero/nonzero specialization witnesses.

Defined in src/polynomials/lazard.mojo.

Field	Type
`orders`	`List[Int]`	The least nonvanishing derivative order for each assigned variable.
`evaluations`	`List[AlgebraicSpecializationCertificate]`	All tested derivatives in prefix order; the last is the lifting polynomial.

`ProjectionResultantCertificate`¶

@fieldwise_init
struct ProjectionResultantCertificate(Copyable, Movable, Writable)

A Sylvester determinant value with every exact elimination identity.

Defined in src/polynomials/determinant.mojo.

Field	Type
`variable`	`Int64`	The eliminated variable.
`resultant`	`SparsePoly[QQ]`	The exact determinant, including its sign.
`steps`	`List[DeterminantStep]`	The fraction-free elimination transcript in forward order.

`cad`¶

def cad(inputs: List[SparsePoly[QQ]], variables: List[Int64], mut budget: Budget, lazard: Bool = False) raises PolyError -> CADCertificate

Decompose real coordinate space into certified sign-invariant cylindrical cells.

Arguments.

inputs: The rational polynomials whose signs must be invariant.
variables: Distinct variables in base-to-top cylindrical order.
budget: The shared work allowance.
lazard: Whether to use Lazard projection and vanishing-order lifting.

Returns. A complete tree of sections and sectors with projection, lifting, coverage and sign witnesses.

Raises.

PolyError: UNSUPPORTED for McCallum nullification outside a terminal point base, DOMAIN for malformed inputs, LIMIT or CAPACITY on work limits.

Defined in src/polynomials/cad.mojo.

`cad_cell`¶

def cad_cell(inputs: List[SparsePoly[QQ]], variables: List[Int64], point: List[RealAlgebraic], mut budget: Budget, lazard: Bool = False) raises PolyError -> CADCellCertificate

Construct only the cylindrical cell path containing an exact algebraic point.

Arguments.

inputs: The rational polynomials whose signs must be invariant.
variables: Distinct variables in base-to-top order.
point: Exact coordinates aligned with the variable order.
budget: The shared work allowance.
lazard: Whether to use Lazard projection and evaluation.

Returns. A certified cell containing the point, with symbolic root-function boundaries and constant signs.

Raises.

PolyError: UNSUPPORTED for disallowed McCallum nullification, DOMAIN for invalid coordinates, LIMIT or CAPACITY on work limits.

Defined in src/polynomials/cad.mojo.

`cad_covering`¶

def cad_covering(inputs: List[SparsePoly[QQ]], masks: List[UInt8], variables: List[Int64], mut budget: Budget, lazard: Bool = False) raises PolyError -> CADCoveringCertificate

Decide a conjunction using a satisfying cell or a complete violating-cell covering.

Arguments.

inputs: The rational constraint polynomials.
masks: Allowed sign bits per polynomial: one for negative, two for zero, four for positive.
variables: Distinct variables in base-to-top cylindrical order.
budget: The shared work allowance.
lazard: Whether to use Lazard projection and lifting.

Returns. A satisfying terminal cell, or one violated constraint for every cell covering real space.

Raises.

PolyError: UNSUPPORTED for disallowed McCallum nullification, DOMAIN for invalid masks or inputs, LIMIT or CAPACITY on work limits.

Defined in src/polynomials/cad_covering.mojo.

`cad_projection`¶

def cad_projection(inputs: List[SparsePoly[QQ]], variables: List[Int64], mut budget: Budget, lazard: Bool = False) raises PolyError -> CADProjectionCertificate

Construct the complete McCallum or Lazard projection closure.

Arguments.

inputs: The rational polynomial family, including repeated factors and zero inputs.
variables: Distinct variables in base-to-top cylindrical order, covering every input.
budget: The shared work allowance.
lazard: Whether to use Lazard leading/trailing coefficient projection.

Returns. Projection bases with product, coprimality and exact determinant certificates.

Raises.

PolyError: DOMAIN for malformed inputs or variable order, LIMIT or CAPACITY on work limits.

Defined in src/polynomials/cad_projection.mojo.

`check_cad`¶

def check_cad(inputs: List[SparsePoly[QQ]], certificate: CADCertificate, mut budget: Budget) raises PolyError -> Bool

Verify global CAD sign invariance and cylindrical coverage from local witnesses.

Arguments.

inputs: The original polynomial family.
certificate: The complete proposed decomposition.
budget: The shared work allowance.

Returns. Whether projection, every complete stack, the cell tree and all terminal signs are valid.

Raises.

PolyError: LIMIT or CAPACITY on work limits.

Defined in src/polynomials/cad.mojo.

`check_cad_cell`¶

def check_cad_cell(inputs: List[SparsePoly[QQ]], point: List[RealAlgebraic], certificate: CADCellCertificate, mut budget: Budget) raises PolyError -> Bool

Verify a sign-invariant cylindrical cell and exact query-point containment.

Arguments.

inputs: The original polynomial family.
point: The original exact coordinates in the certificate's variable order.
certificate: The proposed single-cell path.
budget: The shared work allowance.

Returns. Whether the certified cell contains the query point and has the stated constant signs.

Raises.

PolyError: LIMIT or CAPACITY on work limits.

Defined in src/polynomials/cad.mojo.

`check_cad_covering`¶

def check_cad_covering(inputs: List[SparsePoly[QQ]], masks: List[UInt8], certificate: CADCoveringCertificate, mut budget: Budget) raises PolyError -> Bool

Check a feasibility witness or a complete sign-conflict covering of real space.

Arguments.

inputs: The original polynomial constraints.
masks: The original allowed-sign masks.
certificate: The proposed satisfying cell or complete violating-cell covering.
budget: The shared work allowance.

Returns. Whether the stated feasibility result follows from the certified decomposition.

Raises.

PolyError: DOMAIN for invalid masks, LIMIT or CAPACITY on work limits.

Defined in src/polynomials/cad_covering.mojo.

`check_cad_projection`¶

def check_cad_projection(inputs: List[SparsePoly[QQ]], certificate: CADProjectionCertificate, mut budget: Budget) raises PolyError -> Bool

Check projection closure and recompute optional Brown reduction hypotheses.

Historical Lazard and McCallum certificates use their retained identities. Brown reductions additionally check the coefficient ideal under a work cap.

Arguments.

inputs: The original rational polynomial family.
certificate: The proposed projection closure and witnesses.
budget: The shared work allowance.

Returns. Whether every projection obligation and basis property is certified.

Raises.

PolyError: LIMIT or CAPACITY on work limits.

Defined in src/polynomials/cad_projection.mojo.

`check_lazard_evaluation`¶

def check_lazard_evaluation(f: SparsePoly[QQ], variable: Int64, point: List[Tuple[Int64, RealAlgebraic]], certificate: LazardEvaluationCertificate, mut budget: Budget) raises PolyError -> Bool

Verify minimal vanishing orders and every Taylor-coefficient specialization.

Arguments.

f: The original nonzero polynomial.
variable: The final unassigned variable.
point: The original ordered assignments.
certificate: The proposed orders and specialization witnesses.
budget: The shared work allowance.

Returns. Whether the final specialization is the nonzero Lazard evaluation up to positive factorials.

Raises.

PolyError: DOMAIN for malformed inputs, LIMIT or CAPACITY on work limits.

Defined in src/polynomials/lazard.mojo.

`check_projection_resultant`¶

def check_projection_resultant(f: SparsePoly[QQ], g: SparsePoly[QQ], certificate: ProjectionResultantCertificate, mut budget: Budget) raises PolyError -> Bool

Check a Sylvester determinant by multiplication identities without division.

Arguments.

f: The original first polynomial.
g: The original second polynomial.
certificate: The proposed determinant and elimination transcript.
budget: The shared work allowance.

Returns. Whether the complete transcript proves the exact resultant.

Raises.

PolyError: DOMAIN for malformed inputs, LIMIT or CAPACITY on work limits.

Defined in src/polynomials/determinant.mojo.

`lazard_evaluate`¶

def lazard_evaluate(f: SparsePoly[QQ], variable: Int64, point: List[Tuple[Int64, RealAlgebraic]], mut budget: Budget) raises PolyError -> LazardEvaluationCertificate

Remove vanishing factors before each algebraic substitution in cylindrical order.

Arguments.

f: The nonzero rational polynomial.
variable: The final unassigned lifting variable.
point: Earlier variable assignments in base-to-top cylindrical order.
budget: The shared work allowance.

Returns. Certified vanishing orders and a nonzero lifting specialization, up to positive factorials.

Raises.

PolyError: DOMAIN for zero input or invalid assignments, LIMIT or CAPACITY on work limits.

Defined in src/polynomials/lazard.mojo.

`projection_resultant`¶

def projection_resultant(f: SparsePoly[QQ], g: SparsePoly[QQ], variable: Int64, mut budget: Budget) raises PolyError -> ProjectionResultantCertificate

Compute a resultant with a complete Sylvester determinant transcript.

Arguments.

f: The first rational polynomial.
g: The second polynomial in the same stored order.
variable: The variable to eliminate.
budget: The shared work allowance.

Returns. The exact resultant and fraction-free elimination steps.

Raises.

PolyError: DOMAIN for incompatible inputs, LIMIT or CAPACITY on work limits.

Defined in src/polynomials/determinant.mojo.

`CADConflict`¶

@fieldwise_init
struct CADConflict(Copyable, Movable, Writable)

A certified violated constraint at an exact partial assignment.

Defined in src/polynomials/cylindrical_covering.mojo.

Field	Type
`constraint`	`Int`	The index of the violated input polynomial.
`evaluation`	`AlgebraicPolynomialEvaluation`	Exact polynomial evaluation at the interval sample or root assignment.
`sign`	`AlgebraicComparisonCertificate`	The value's sign, excluded by the constraint's allowed-sign mask.

`CADConflictInterval`¶

@fieldwise_init
struct CADConflictInterval(Copyable, Movable, Writable)

A conflicting interval spanning consecutive sections and sectors of a stack.

Defined in src/polynomials/cylindrical_covering.mojo.

Field	Type
`parent`	`Int`	The base cell whose stack contains the interval.
`lower`	`Int`	The first included stack position, with zero denoting the lower unbounded sector.
`upper`	`Int`	The last included stack position; section parity determines endpoint inclusion.
`position`	`Int`	The stack sample at which the conflict is certified.
`proof`	`CADConflict`	The violated constraint and its evaluation and sign proofs.

`CylindricalCoveringCertificate`¶

@fieldwise_init
struct CylindricalCoveringCertificate(Copyable, Movable, Writable)

A selective feasibility witness or overlapping cylindrical conflict covering.

Defined in src/polynomials/cylindrical_covering.mojo.

Field	Type
`projection`	`CADProjectionCertificate`	The projection closure proving delineability and sign invariance.
`cells`	`List[CADCell]`	Only visited base cells, with parents preceding children and root at index zero.
`stacks`	`List[CADStackCertificate]`	Complete local root delineations for visited nonterminal cells.
`conflicts`	`List[CADConflictInterval]`	Possibly overlapping intervals excluded by individual constraints.
`root_conflict`	`Optional[CADConflict]`	An optional constant contradiction excluding all coordinates without lifting.
`witness_cell`	`Int`	A fully assigned satisfying cell, or minus one for a complete conflict covering.

`cylindrical_covering`¶

def cylindrical_covering(inputs: List[SparsePoly[QQ]], masks: List[UInt8], variables: List[Int64], mut budget: Budget, lazard: Bool = False) raises PolyError -> CylindricalCoveringCertificate

Decide a sign conjunction by sampling uncovered intervals and pruning cylinders.

Arguments.

inputs: The rational constraint polynomials.
masks: Allowed sign bits per polynomial: one for negative, two for zero, four for positive.
variables: Distinct variables in base-to-top cylindrical order.
budget: The shared work allowance.
lazard: Whether to use Lazard projection and vanishing-order evaluation.

Returns. A satisfying assignment or independently checkable overlapping conflict coverage.

Raises.

PolyError: DOMAIN for invalid inputs, UNSUPPORTED for McCallum nullification, LIMIT or CAPACITY on work limits.

Defined in src/polynomials/cylindrical_covering.mojo.

`check_cylindrical_covering`¶

def check_cylindrical_covering(inputs: List[SparsePoly[QQ]], masks: List[UInt8], certificate: CylindricalCoveringCertificate, mut budget: Budget) raises PolyError -> Bool

Verify selective conflict intervals and cylindrical coverage without searching.

Arguments.

inputs: The original polynomial constraints.
masks: The original allowed-sign masks.
certificate: The proposed selective feasibility or infeasibility certificate.
budget: The shared work allowance.

Returns. Whether exact evaluation, projection, interval expansion and coverage justify the result.

Raises.

PolyError: DOMAIN for invalid masks, LIMIT or CAPACITY on work limits.

Defined in src/polynomials/cylindrical_covering.mojo.

`CoveringBound`¶

@fieldwise_init
struct CoveringBound(Copyable, Movable, Writable)

An interval endpoint: one real root of a characterization polynomial at the node's prefix.

Defined in src/polynomials/cad_coverings_search.mojo.

Field	Type
`polynomial`	`Int`	The index of the polynomial in CADCoveringsCertificate.polynomials.
`root`	`Int`	The root's index, in increasing order, among the real roots of the polynomial's Lazard evaluation at the prefix.

`CoveringInterval`¶

@fieldwise_init
struct CoveringInterval(Copyable, Movable, Writable)

An interval of one coordinate, above a node's prefix, on which the conjunction fails.

Defined in src/polynomials/cad_coverings_search.mojo.

Field	Type
`lower`	`Optional[CoveringBound]`	The lower endpoint, or None for minus infinity.
`upper`	`Optional[CoveringBound]`	The upper endpoint, or None for plus infinity.
`lower_closed`	`Bool`	Whether the lower endpoint belongs to the interval; with upper_closed, a single section.
`upper_closed`	`Bool`	Whether the upper endpoint belongs to the interval.
`sample`	`RealAlgebraic`	A point of the interval at which the conflict or the child covering is established.
`constraint`	`Int`	The input violated on the whole interval, or minus one when a child covering excludes it.
`child`	`Int`	The node covering the next coordinate above the sample, or minus one.
`polynomials`	`List[Int]`	The characterization: same-level polynomials delimiting the interval and lower-level polynomials whose signs it relies on.

`CoveringNode`¶

@fieldwise_init
struct CoveringNode(Copyable, Movable, Writable)

A covering of one coordinate's line above an exact prefix point.

Defined in src/polynomials/cad_coverings_search.mojo.

Field	Type
`parent`	`Int`	The node whose interval sample extends the prefix, or minus one for the root.
`interval`	`Int`	That interval's index in the parent's intervals, or minus one for the root.
`level`	`Int`	The zero-based level of the covered coordinate.
`intervals`	`List[CoveringInterval]`	Intervals covering the whole line, in increasing order.

`CADCoveringsCertificate`¶

@fieldwise_init
struct CADCoveringsCertificate(Copyable, Movable, Writable)

A satisfying point, or a conflict-driven cylindrical covering proving that none exists.

Defined in src/polynomials/cad_coverings_search.mojo.

Field	Type
`variables`	`List[Int64]`	Variables in base-to-top cylindrical order.
`polynomials`	`List[SparsePoly[QQ]]`	Normalized irreducible polynomials named by bounds and characterizations.
`input_factors`	`List[MultivariateFactorization[QQ]]`	One factorization per input, in input order.
`projections`	`List[MultivariateFactorization[QQ]]`	Factorizations of the projection polynomials the checker recomputes, in any order.
`nodes`	`List[CoveringNode]`	The covering tree, root first; empty when satisfiable or for a root conflict.
`root_conflict`	`Int`	An input constant on the whole search space whose sign fails, or minus one.
`witness`	`List[RealAlgebraic]`	A satisfying point in base-to-top order, or empty.
`evaluations`	`List[AlgebraicPolynomialEvaluation]`	Input values at the witness.
`signs`	`List[AlgebraicComparisonCertificate]`	Input signs at the witness.

`CADCoveringsCertificate.satisfiable`¶

def satisfiable(self) -> Bool

Report whether the certificate claims a satisfying point.

Returns. True for a witness, False for a covering or a root conflict.

`coverings_solve`¶

def coverings_solve(inputs: List[SparsePoly[QQ]], masks: List[UInt8], variables: List[Int64], mut budget: Budget, lazard: Bool = True) raises PolyError -> CADCoveringsCertificate

Decide a sign conjunction by a conflict-driven search over cylindrical algebraic coverings.

The search assigns one coordinate at a time and stops at the first satisfying point. Otherwise every failed sample is generalized to an interval through local Lazard (or, with lazard False, McCallum) characterizations, and the result is a checkable covering tree.

Arguments.

inputs: The rational constraint polynomials.
masks: Allowed sign bits per polynomial: one for negative, two for zero, four for positive.
variables: Distinct variables in base-to-top cylindrical order, covering every input.
budget: The shared work allowance.
lazard: Whether to use Lazard characterizations; False selects McCallum's, which refuse nullification.

Returns. A satisfying point with its input signs, or a covering proving that none exists.

Raises.

PolyError: DOMAIN for invalid inputs, UNSUPPORTED for McCallum nullification, LIMIT or CAPACITY on work limits.

Defined in src/polynomials/cad_coverings_search.mojo.

`check_coverings`¶

def check_coverings(inputs: List[SparsePoly[QQ]], masks: List[UInt8], certificate: CADCoveringsCertificate, mut budget: Budget) raises PolyError -> Bool

Verify a coverings certificate without searching or trusting the producer's choices.

A witness is substituted exactly and every sign checked. A covering is replayed node by node: bounds are recomputed as roots at the node's prefix, intervals must contain their samples, cover the line, and hold no characterization root inside; conflicts are exact signs at the samples; and each child's Lazard projection is recomputed, its supplied factorizations checked by product, and every factor required in the parent interval's characterization.

Arguments.

inputs: The original polynomial constraints.
masks: The original allowed-sign masks.
certificate: The proposed witness or covering.
budget: The shared work allowance.

Returns. Whether the certificate proves its verdict.

Raises.

PolyError: DOMAIN for invalid masks, LIMIT or CAPACITY on work limits.

Defined in src/polynomials/cad_coverings_search.mojo.

Cylindrical algebraic decomposition¶

Final-data construction¶

CADFinalCell¶

CADFinalCertificate¶

CADFinalCertificate.is_compact¶

CADFinalCertificate.is_covering¶

CADFinalCertificate.variables¶

CADFinalCertificate.factor_counts¶

CADFinalCertificate.cell_count¶

CADFinalCertificate.stack_count¶

CADFinalCertificate.satisfiable¶

CADFinalCertificate.cells¶

CADFinalCertificate.legacy_decomposition¶

CADFinalCertificate.sample¶

CADFinalCertificate.legacy_covering¶

CADFinalCertificate.compact_bytes¶

CADFinalCertificate.from_compact_bytes¶

CADFinalCertificate.from_legacy¶

CADFinalCertificate.from_legacy_covering¶

cad_final¶

check_cad_final¶

Legacy certificates¶

Fix leading algebraic coordinates¶

CADFiber¶

CADFiber.__init__¶

CADFiber.decompose¶

CADFiber.cover¶

CADFiber.solve¶

CADFiber.search¶

CADFiber.check¶

CADFiber.check¶

CADFiber.check¶

CADFiber.check¶

CADFiber.decompose_to¶

CADFiber.checker¶

Reading cells and certificates¶

CADCell¶

CADCellCertificate¶

CADCertificate¶

CADCoveringCertificate¶

CADPolynomialLift¶

CADProjectionCertificate¶

CADSignWitness¶

CADStackCertificate¶

DeterminantStep¶

LazardEvaluationCertificate¶

ProjectionResultantCertificate¶

cad¶

cad_cell¶

cad_covering¶

cad_projection¶

check_cad¶

check_cad_cell¶

check_cad_covering¶

check_cad_projection¶

check_lazard_evaluation¶

check_projection_resultant¶

lazard_evaluate¶

projection_resultant¶

CADConflict¶

CADConflictInterval¶

CylindricalCoveringCertificate¶

cylindrical_covering¶

check_cylindrical_covering¶

CoveringBound¶

CoveringInterval¶

CoveringNode¶

CADCoveringsCertificate¶

CADCoveringsCertificate.satisfiable¶

coverings_solve¶

check_coverings¶

`CADFinalCell`¶

`CADFinalCertificate`¶

`CADFinalCertificate.is_compact`¶

`CADFinalCertificate.is_covering`¶

`CADFinalCertificate.variables`¶

`CADFinalCertificate.factor_counts`¶

`CADFinalCertificate.cell_count`¶

`CADFinalCertificate.stack_count`¶

`CADFinalCertificate.satisfiable`¶

`CADFinalCertificate.cells`¶

`CADFinalCertificate.legacy_decomposition`¶

`CADFinalCertificate.sample`¶

`CADFinalCertificate.legacy_covering`¶

`CADFinalCertificate.compact_bytes`¶

`CADFinalCertificate.from_compact_bytes`¶

`CADFinalCertificate.from_legacy`¶

`CADFinalCertificate.from_legacy_covering`¶

`cad_final`¶

`check_cad_final`¶

`CADFiber`¶

`CADFiber.init`¶

`CADFiber.decompose`¶

`CADFiber.cover`¶

`CADFiber.solve`¶

`CADFiber.search`¶

`CADFiber.check`¶

`CADFiber.check`¶

`CADFiber.check`¶

`CADFiber.check`¶

`CADFiber.decompose_to`¶

`CADFiber.checker`¶

`CADCell`¶

`CADCellCertificate`¶

`CADCertificate`¶

`CADCoveringCertificate`¶

`CADPolynomialLift`¶

`CADProjectionCertificate`¶

`CADSignWitness`¶

`CADStackCertificate`¶

`DeterminantStep`¶

`LazardEvaluationCertificate`¶

`ProjectionResultantCertificate`¶

`cad`¶

`cad_cell`¶

`cad_covering`¶

`cad_projection`¶

`check_cad`¶

`check_cad_cell`¶

`check_cad_covering`¶

`check_cad_projection`¶

`check_lazard_evaluation`¶

`check_projection_resultant`¶

`lazard_evaluate`¶

`projection_resultant`¶

`CADConflict`¶

`CADConflictInterval`¶

`CylindricalCoveringCertificate`¶

`cylindrical_covering`¶

`check_cylindrical_covering`¶

`CoveringBound`¶

`CoveringInterval`¶

`CoveringNode`¶

`CADCoveringsCertificate`¶

`CADCoveringsCertificate.satisfiable`¶

`coverings_solve`¶

`check_coverings`¶