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.
Dedekind-complete ordered real field
Definition
A Dedekind-complete ordered field is a commutative field with identity , a total order compatible with addition and multiplication, and the least-upper-bound axiom: every nonempty subset of that is bounded above has a least upper bound in . Throughout this batch, all real variables, intervals, limits, derivatives and integrals are taken in such a field. The integers and rationals are interpreted in their usual embedded copies. For , define when and when .
Used by
- Shared formal perturbation for declared determinant tie-breaking Algorithm
- Continuity and derivative on a real interval Definition
- Dyadic floating-point format and directed rounding Definition
- Dyadic orientation and lifted sphere determinants Definition
- Finite complex-array norms used by the NUFFT certificates Definition
- Real intervals, complex rectangles and ball enclosures Definition
- A nondegenerate dyadic simplex determines a unique sphere Lemma
- A nonzero 2-by-2 or 3-by-3 dyadic determinant gives a unique real solution Lemma
- Cauchy products of absolutely convergent series multiply their sums Lemma
- Closed real intervals are compact by completeness Lemma
- Continuous functions have an oriented Riemann integral Lemma
- Continuous functions on a closed interval attain their extrema Lemma
- Dedekind completeness implies the Archimedean property Lemma
- Elementary factorial and geometric series converge uniformly Lemma
- Mean value theorem on a closed real interval Lemma
- Nonnegative real square roots exist uniquely Lemma
- Power series may be differentiated term by term inside their radius Lemma
- Real and complex modulus product and triangle inequalities Lemma
- The orientation-normalized lifted determinant records the side of a sphere Lemma
- Triangle inequality for the finite NUFFT Euclidean norm Lemma
- Outward-rounded operations are inclusion-isotone and enclose DAG evaluations Theorem
- The formal determinant tie-break is nondegenerate and consistent Theorem
Dependency tree · 0 levels
Nothing. This result depends on no other item in the library.
Sources
- Steven G. Krantz, Foundations of Analysis, §1.1, Theorems 1.7 and 1.10 (standard reference, not scraped)