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 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].

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

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