ExampleConstruction: AI-generatedVerification: AI-generatedPipeline-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.

Division of [1,2] by [-1,1] has no finite hull

Example

Take numerator interval $X = [1, 2]$ and divisor interval $Y = [- 1, 1]$ . The exact quotient set over $y \neq 0$ is unbounded above and below. Therefore no finite interval is a sound hull; the permitted results are a sign split or an entire status.

Facts & Assumptions

Given: $X = [1, 2]$ , $Y = [- 1, 1]$ , and the quotient set ${x / y : x \in X, y \in Y ∖ {0}}$ .

[L1]

Outward-rounded interval, rectangle and ball operations: division with a denominator interval containing zero returns split-domain or a non-finite status, never a finite quotient interval.

[L2]

Outward-rounded operations are inclusion-isotone and enclose DAG evaluations: a finite interval result must contain every exact quotient in its domain.

Verification

1.1givenchooseconstructalgebra

For any $M > 0$ , choose a real $t > M + 1$ , set $x = 1$ and $y = 1 / t$ . Then $x \in [1, 2]$ , $y \in (0, 1] \subset Y$ , and $x / y = t > M$ . Replacing $y$ by $- 1 / t$ gives a quotient $- t < - M$ . Thus the quotient set is unbounded in both directions.

2.1step 1.1L1L2algebra∎

A finite interval has finite lower and upper endpoints, so choose $M$ larger than their absolute values in step 1.1; the resulting exact quotient lies outside that interval, contradicting the required inclusion [L2]. The branch in [L1] avoids that contradiction by declining a finite hull.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

10 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

Kearfott, Interval Computations: Introduction, Uses, and Resources, §1 (standard reference, not scraped)
Rump, Verification methods: Rigorous results using floating-point arithmetic, §§5.1 and 5.4 (standard reference, not scraped)