ExampleConstruction: AI-generatedVerification: AI-generatedPipeline-generatedprecheck pass

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.

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.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

25 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.4 (standard reference, not scraped)