Pipeline-generated

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.

✓ 3 results · all verified · 1 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 2 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Certified geometric predicates — Examples

1 · Prerequisites

2 · Summary

Examples

The examples show an exact sign after a near-degenerate floating filter, a nearly cocircular lifted determinant certified at higher precision, and an interval input whose possible coordinates give both orientation signs.

\begin{tikzpicture}[scale=0.85]
  \draw[gray,dashed] (0,0) -- (3,3);
  \fill (0,0) circle (2pt) node[below left] {$A$};
  \fill (1.5,1.5) circle (2pt) node[below left] {$B$};
  \fill (3,3.35) circle (2pt) node[above right] {$C$};
  \node at (1.5,-0.7) {nearly collinear (vertical gap exaggerated)};

  \begin{scope}[xshift=5.2cm]
    \draw[gray] (5,1) circle (1.414);
    \fill (4,0) circle (2pt) node[below left] {$A$};
    \fill (6,0) circle (2pt) node[below right] {$B$};
    \fill (4,2) circle (2pt) node[above left] {$C$};
    \fill (6,2.25) circle (2pt) node[above right] {$D$};
    \node at (5,-0.7) {nearly cocircular (gap exaggerated)};
  \end{scope}
\end{tikzpicture}

The drawings are schematic: the displayed gaps are enlarged for visibility. Exact coordinates and all sign calculations are given in the example items; no proof relies on a measured diagram distance.

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-6-luna)Open item page →

An uncertain coordinate interval does not decide orientation

Example

Take $A = (0, 0)$ , $B = (1, 0)$ , and $C = (2, Y)$ where $Y \in [- 1 / 8, 1 / 8]$ . Use an outward-rounding format that represents $0, 1, 2,$ and $\pm 1 / 8$ exactly. The exact orientation determinant is $Y$ . Outward interval evaluation returns $[- 1 / 8, 1 / 8]$ , which contains zero and both signs; the certified result is indeterminate.

Facts & Assumptions

Given: The first two points are exact, and the third point has exact coordinate intervals $C_{x} = [2, 2]$ and $C_{y} = [- 1 / 8, 1 / 8]$ .

[F1]

Dyadic orientation and lifted sphere determinants: orientation is the determinant of ordered rows $(p_{i}, 1)$ .

[F2]

Outward-rounded operations are inclusion-isotone and enclose DAG evaluations: a finite outward arithmetic DAG encloses the exact determinant for every admissible coordinate assignment.

[F3]

Certified geometric predicate for interval-valued coordinates: the interval procedure returns indeterminate when its finite determinant interval contains zero.

[F4]

The interval geometric filter certifies only uniform signs: positive or negative is returned only when that sign holds for every tuple in the box.

[A1]

The selected outward-rounding format represents $0, 1, 2,$ and $\pm 1 / 8$ exactly.

Verification

1.1givenF1algebra

The orientation matrix is $(\begin{array}{ccc} 0 & 0 & 1 \\ 1 & 0 & 1 \\ 2 & Y & 1 \end{array})$ , whose determinant is $Y$ . Since $Y$ ranges over $[- 1 / 8, 1 / 8]$ , admissible inputs realize a negative value, zero, and a positive value.

1.2givenF1F2A1algebra

The Leibniz interval expression has only one nonzero term, namely the interval $C_{y} = [- 1 / 8, 1 / 8]$ ; all other terms contain an exact zero factor. Every intermediate endpoint is among $0, 1, 2, \pm 1 / 8$ , so [A1] makes every outward rounding exact. The returned interval is therefore $[- 1 / 8, 1 / 8]$ , and its inclusion is guaranteed by [F2].

2.1F3F4step 1.1step 1.2∎

The returned interval contains zero, so [F3] requires indeterminate; by [F4] neither positive nor negative could certify all admissible inputs.

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passOpen item page →

A nearly cocircular quadruple has a certified lifted sign

Example

Let $A = (0, 0)$ , $B = (1, 0)$ , $C = (0, 1)$ , and $D = (1, 1 + δ)$ with $δ = 2^{- 52}$ . Their raw lifted determinant with rows $(x, y, x^{2} + y^{2}, 1)$ is $- (δ + δ^{2})$ . In a 113-bit filter format with $u = 2^{- 113}$ and a normal range covering the displayed operations, every lifted entry is exactly representable. The filter error radius is less than $δ / 4$ , so it certifies the negative lifted sign; since the base orientation is positive, the last site is outside the circle through $A, B, C$ .

Facts & Assumptions

Given: The four dyadic sites, the ordered lifted-matrix convention, a 113-bit filter system with unit roundoff $u = 2^{- 113}$ , and normal-range operation results.

[F1]

Dyadic orientation and lifted sphere determinants: the base orientation uses rows $(p_{i}, 1)$ and the lifted determinant uses rows $(p_{i}, \sum_{j} p_{i, j}^{2}, 1)$ .

[F2]

The orientation-normalized lifted determinant records the side of a sphere: for a nondegenerate base simplex, $L_{d} = - O_{d} (∥ q - c ∥^{2} - r^{2})$ , so positive $O_{d} L_{d}$ means inside and negative means outside.

[F3]

The standard relative floating-point model and unit roundoff: the relative model bounds every allowed operation error by the stated unit roundoff and requires normal-range exact results.

[F4]

A left-to-right Leibniz determinant has an explicit forward error bound: for size $s$ , the computed determinant error is at most $γ_{s + s! - 2} S$ under the model hypotheses.

[F5]

Outward-bounded floating determinant filter: the error radius is rounded upward and the filter returns a sign only when its error interval excludes zero.

[F6]

Outward-rounded operations are inclusion-isotone and enclose DAG evaluations: outward interval evaluation encloses the exact absolute-term sum when finite.

[F7]

Dyadic floating-point format and directed rounding: binary formats have a finite normal range and represent dyadic values by the stated precision and exponent parameters.

[F8]

The filtered exact dyadic predicate is sound and terminates: the top-level predicate returns the exact raw determinant sign.

[F9]

Directed dyadic rounding encloses with explicit underflow and overflow bounds: upward directed rounding returns the least representable value not below a finite exact input.

[A1]

The selected 113-bit format represents all displayed matrix entries and has normal range containing every exact intermediate and the final error radius.

Verification

1.1givenF1algebra

The orientation determinant of $A, B, C$ is $\det (\begin{array}{ccc} 0 & 0 & 1 \\ 1 & 0 & 1 \\ 0 & 1 & 1 \end{array}) = 1$ . The lifted matrix has rows $(0, 0, 0, 1)$ , $(1, 0, 1, 1)$ , $(0, 1, 1, 1)$ , and $(1, 1 + δ, 2 + 2 δ + δ^{2}, 1)$ . Expanding its determinant leaves $- (δ + δ^{2})$ .

1.2F6F7algebra

The largest lifted entry $2 + 2 δ + δ^{2}$ has no nonzero binary place below $2^{- 104}$ , so it needs at most 107 significant bits; the 113-bit format represents it and all other matrix entries exactly. The absolute-term sum is $S = 4 + 3 δ + δ^{2} < 5$ , also exactly representable. By [F6] its outward upper endpoint is $U = S$ .

2.1F1F2step 1.1algebra

The base circle has center $(1 / 2, 1 / 2)$ and squared radius $1 / 2$ . The last point's squared distance is $1 / 4 + (1 / 2 + δ)^{2} = 1 / 2 + δ + δ^{2}$ , so it is outside; [F2] agrees with the negative product of the positive orientation and negative lifted determinant.

2.2F3F4F9step 1.2algebra

Here $s = 4$ , $q = 26$ , and $26 u < 1 / 2$ , so $γ_{26} < 52 u$ . Hence $γ_{26} U < 260 \cdot 2^{- 113} < 2^{- 104}$ . Since $2^{- 104}$ is representable, upward rounding gives $E \leq 2^{- 104} < δ / 4$ by [F9], and the exact determinant bound [F4] gives $∣ \hat{D} - L_{2} ∣ \leq E$ .

3.1F1F5F8step 1.1step 2.2algebra∎

Since $L_{2} = - (δ + δ^{2}) < - δ$ and $E < δ / 4$ , $\hat{D} + E \leq L_{2} + 2 E < 0$ . The filter therefore returns negative by [F5]; the exactness of this sign also follows from [F8]. The positive base orientation makes the normalized side sign negative, so $D$ is outside.

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passOpen item page →

A nearly collinear dyadic triangle falls through to the exact sign

Example

Let $A = (0, 0)$ , $B = (1, 1)$ , and $C = (2, 2 + δ)$ with $δ = 2^{- 51}$ , using binary64 inputs. The exact orientation determinant is $δ > 0$ . In the 53-bit filter system with $u = 2^{- 53}$ , the outward error interval includes zero, so the certified predicate uses its exact integer fallback and returns positive.

Facts & Assumptions

Given: The three listed points, the row convention for orientation, a 53-bit binary64 filter, and the standard relative model with every nonzero operation result normal-range.

[F1]

Dyadic orientation and lifted sphere determinants: orientation is the sign of the determinant with ordered rows $(p_{i}, 1)$ .

[F2]

The standard relative floating-point model and unit roundoff: the binary64 unit roundoff is $u = 2^{- 53}$ , and its relative error model excludes underflow and overflow.

[F3]

A left-to-right Leibniz determinant has an explicit forward error bound: for an $s \times s$ matrix, $q = s + s! - 2$ and $∣ \hat{D} - \det M ∣ \leq γ_{q} S$ when the stated operation hypotheses hold.

[F4]

Dyadic floating-point format and directed rounding: the representable spacing in $[2^{e}, 2^{e + 1})$ is $2^{e - p + 1}$ .

[F5]

Directed dyadic rounding encloses with explicit underflow and overflow bounds: downward and upward rounding bracket every finite exact endpoint.

[F6]

Outward-rounded operations are inclusion-isotone and enclose DAG evaluations: every exact value of a finite DAG with finite operation results belongs to its computed interval enclosure.

[F7]

Outward-bounded floating determinant filter: the filter returns a sign only if $[\hat{D} - E, \hat{D} + E]$ excludes zero.

[F8]

Certified predicate for exact dyadic geometric inputs: an inconclusive filter falls through to the exact integer-clearance determinant sign.

[F9]

A certified floating determinant filter returns only the exact sign: a nonzero filter sign equals the exact determinant sign.

[F10]

The filtered exact dyadic predicate is sound and terminates: the certified dyadic procedure returns the exact determinant sign.

[A1]

The selected 53-bit filter rounds every exactly representable normal result exactly and has no underflow or overflow on this calculation.

Verification

1.1givenF1algebra

With rows $(A, 1), (B, 1), (C, 1)$ , the determinant is $\det (\begin{array}{ccc} 0 & 0 & 1 \\ 1 & 1 & 1 \\ 2 & 2 + δ & 1 \end{array}) = δ$ by expansion along the first row. Thus the exact sign is positive.

1.2givenF2A1algebra

In lexicographic Leibniz order the only nonzero signed terms are $+ (2 + δ)$ and $- 2$ . They and their sum $δ$ are exactly representable normal binary64 values, so by [A1] the filter's approximation is $\hat{D} = δ$ .

1.3F4F5F6algebra

The absolute-term sum is $S = (2 + δ) + 2 = 4 + 2^{- 51}$ . Since $4 \leq S < 8$ , [F4] gives spacing $2^{- 50}$ ; $S$ is halfway between $4$ and $4 + 2^{- 50}$ . Outward upward rounding therefore gives $U = 4 + 2^{- 50}$ by [F5], and the outward DAG is sound by [F6].

2.1F2F3F7step 1.3algebra

Here $s = 3$ , so $q = 7$ and $γ_{7} > 7 u$ . Therefore $E \geq γ_{7} U > 28 \cdot 2^{- 53} = 7 δ > δ = \hat{D}$ . The filter interval contains zero and [F7] forces inconclusive.

3.1F8F9F10step 1.1step 2.1∎

By [F8] the top-level procedure now uses its exact integer fallback; the determinant in [step 1.1] is $δ > 0$ . Its returned sign is positive, as also guaranteed by [F9]–[F10].

Certified geometric predicates — Examples

1 · Prerequisites

2 · Summary

Examples

3 · Logical flowchart

4 · Definitions, theorems and proofs

5 · Examples, counterexamples and false statements

An uncertain coordinate interval does not decide orientation

Example

Facts & Assumptions

Verification

A nearly cocircular quadruple has a certified lifted sign

Example

Facts & Assumptions

Verification

A nearly collinear dyadic triangle falls through to the exact sign

Example

Facts & Assumptions

Verification

Sources