How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
Certified predicate for exact dyadic geometric inputs
Definition
Input: an ordered tuple of exact dyadic points in dimension or
, with exactly points for an orientation request and exactly
points for a raw incircle/insphere or orientation-normalized sphere-side
request, and optionally a filter configuration
containing a floating format, its exact dyadic unit-roundoff bound, and a
verifiable finite range certificate. Output: the requested sign, including
zero; for a sphere-side request with zero base orientation, output
degenerate-base together with the raw lifted sign. For each required
determinant, construct its matrix in
Dyadic orientation and lifted sphere determinants exactly using dyadic
integer arithmetic.
- Attempt Outward-bounded floating determinant filter only when the optional filter configuration is present and its format, standard relative model, and finite normal-range certificate satisfy that algorithm's inputs. If it is absent or invalid, skip directly to the exact fallback.
- If the filter returns a nonzero sign, use that sign. If the filter is unavailable or inconclusive, use Exact dyadic determinant sign by integer clearance. For an orientation or raw lifted request, return this sign.
- For a requested incircle/insphere side, compute the base orientation and
lifted determinant signs by the preceding steps. If the base orientation is
zero, return the status
degenerate-basetogether with the raw lifted sign. Otherwise return the sign of their product: positive inside, zero on, negative outside, by The orientation-normalized lifted determinant records the side of a sphere.
Remarks
The exact fallback is justified by The integer-clearance determinant-sign algorithm is correct and terminates. The exact predicates retain zero. A caller may separately opt into the symbolic tie-break algorithm; it does not alter this procedure.
Depends on
Used by
- Exact certified clipping of convex rational polygons Algorithm
- Finite exact 3D Delaunay and regular lower-hull cavity repair Algorithm
- Incremental planar Delaunay insertion with exact edge flips Algorithm
- A nearly cocircular quadruple has a certified lifted sign Example
- A nearly collinear dyadic triangle falls through to the exact sign Example
- Certified clipping returns the exact convex polygon overlap Theorem
- The filtered exact dyadic predicate is sound and terminates Theorem
Dependency tree · two levels
16 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- Jonathan R. Shewchuk, Adaptive Precision Floating-Point Arithmetic and Fast Robust Geometric Predicates, §§4.2–4.4 (standard reference, not scraped)
- CGAL Developer Manual, Robustness Issues, §11.1 (standard reference, not scraped)