Alphabeta MathHow 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.
The filtered exact dyadic predicate is sound and terminates
Statement
For every finite encoded dyadic point tuple and every orientation or lifted determinant request in Certified predicate for exact dyadic geometric inputs, the returned raw sign equals the exact determinant sign, including zero, and the procedure terminates. A nondegenerate incircle/insphere side result agrees with the orientation- normalized convention in The orientation-normalized lifted determinant records the side of a sphere.
Facts & Assumptions
Given: Finite binary coordinates interpreted as exact dyadic rationals, and the procedures and determinant conventions on the certified geometric predicate page.
Dyadic orientation and lifted sphere determinants: orientation uses rows and the lifted determinant uses rows , with the specified point and column order.
A certified floating determinant filter returns only the exact sign: a positive or negative floating filter output is the exact determinant sign; inconclusive outputs make no claim.
Exact dyadic determinant sign by integer clearance: the fallback clears dyadic row denominators and returns the sign of the exact integer Leibniz sum.
Clearing dyadic row denominators preserves determinant sign: positive row scaling preserves determinant sign and zero.
The orientation-normalized lifted determinant records the side of a sphere: when the base orientation is nonzero, the sign of the orientation times lifted determinant gives the exact inside/on/outside classification.
Proof
The point tuple is finite and every coordinate is dyadic. The entries of the orientation matrix and lifted matrix use only finitely many sums and products of dyadics, so each requested matrix is a finite dyadic matrix under [F1].
For each requested matrix, if the floating filter returns a sign, it is exact by [F2]. If the filter is skipped or returns inconclusive, the algorithm invokes the integer fallback; [F3] computes its finite Leibniz sum exactly, and [F4] transfers its sign to the original dyadic determinant. Thus the raw result is correct, including when it is zero.
A matrix has size at most five. Each filter attempt enumerates finitely many products and interval operations, and a failed precondition or nonfinite status branches directly to the fallback. The fallback performs finite row scalings and exactly integer terms, each a finite integer product and sum, so it terminates for every finite encoding.
When a sphere-side result is requested and the base orientation is nonzero, the algorithm returns the sign of the product of the two exact raw signs from [step 1.2]. Its inside/on/outside meaning follows from [F5]. When the base orientation is zero, the algorithm returns degenerate-base and makes no side classification.
The construction and fallback are finite and choose no element from an arbitrary family; no axiom of choice is used.
Depends on
- Certified predicate for exact dyadic geometric inputs
- A certified floating determinant filter returns only the exact sign
- Exact dyadic determinant sign by integer clearance
- Clearing dyadic row denominators preserves determinant sign
- The orientation-normalized lifted determinant records the side of a sphere
- Dyadic orientation and lifted sphere determinants
Used by
- A nearly cocircular quadruple has a certified lifted sign Example
- A nearly collinear dyadic triangle falls through to the exact sign Example
- Exact 3D lower-hull insertion covers the hull and terminates Theorem
- Exact planar insertion terminates with a weak empty-circle triangulation Theorem
Cited to discharge well-definedness by Certified predicate for exact dyadic geometric inputs.
Dependency tree · two levels
15 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)