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.
Square roots exist: a unique with ; the positives are
Statement
Let be a complete ordered field (Complete ordered field (least-upper-bound property)). Then every with has a unique with and ; we write . Consequently the positive elements of are exactly the nonzero squares: if and only if for some .
Facts & Assumptions
Given: A complete ordered field (Complete ordered field (least-upper-bound property)), that is, an ordered field (Ordered field) with the least-upper-bound property, and an element with .
Every nonempty subset of that is bounded above has a least upper bound in (Complete ordered field (least-upper-bound property)).
Sign and scaling rules: a product of positives is positive, and for one has (Sign rules for products and monotonicity of multiplication).
Squaring is strictly monotone on the nonnegatives: if then ; in particular squaring is injective on (Squaring is monotone on the nonnegatives).
A nonzero square is positive: if then (Squares of nonzero elements are positive).
Multiplying inequalities of positives: if and then (Multiplying inequalities of positives).
Proof
If , then satisfies and , so existence holds; assume henceforth .
Uniqueness holds once a root exists: if satisfy , then strict monotonicity of squaring on nonnegatives [L3] rules out both and , forcing ; so at most one has .
Define ; then because and , so .
The element is an upper bound of : since we have , so any has and , whence , giving .
By completeness [L1], exists in ; and since we have .
Assume, for contradiction, that ; by trichotomy either or .
(Case .) Choose with and , possible since and ; then and , so , whence with , contradicting that is an upper bound of .
(Case .) Here since ; choose with and , so and , hence every has with and , so by [L3]; thus is an upper bound of with , contradicting that is the least upper bound.
Both cases of the disjunction in step 3.1 give a contradiction, so the assumption fails and : a unique (by step 1.2) with exists, and applying this to any writes with while conversely any nonzero square is positive by [L4], so the positive elements of are exactly the nonzero squares.
Depends on
Used by
- Every a cos x+b sin x has the amplitude-phase form R cos(x-φ) Corollary
- For n ≥ 1 every bounded sequence in ℝⁿ has a convergent subsequence Corollary
- If f is continuous on [a,b], differentiable on (a,b), and f' extends continuously to [a,b], then the graph of f has length ∫ₐᵇ√1+f'(t)² dt Corollary
- The central binomial coefficient is asymptotic to 4ⁿ divided by the square root of pi n Corollary
- {q ∈ ℚ : q ≥ 0, q² < 2} is closed and bounded in ℚ and is not compact Counterexample
- ‖·‖₁ on ℝ² violates the parallelogram law, so no symmetric bilinear form induces it Counterexample
- ∏_j ≥ 0 (1 + (-1)ʲ/√j+2) has partial products tending to 0 although ∑_j ≥ 0 (-1)ʲ/√j+2 converges Counterexample
- A curve for which the mean value inequality is an equality, showing the constant cannot be improved Counterexample
- A field homomorphism of ordered fields need not preserve order Counterexample
- An annihilating polynomial need not be minimal: √2 is a root of both x²-2 and x⁴-4 Counterexample
- f(t) = (t², t³) on [0,1]: no ξ satisfies f(1)-f(0) = f'(ξ) Counterexample
- g(x,y) = xy/(x²+y²), extended by g(0,0)=0, is continuous in each variable separately and not continuous at the origin Counterexample
- On a closed interval of ℚ there is a continuous unbounded function, a bounded one with no maximum, and one without the intermediate value property Counterexample
- Over ℚ there is a nonconstant differentiable function with identically zero derivative, so Rolle and the mean value theorem both fail Counterexample
- ℚ ∩ [0,2] is bounded and disconnected, so being an interval of ℚ is not enough Counterexample
- The Cauchy product of ∑_k ≥ 0 (-1)ᵏ/√k+1 with itself has |cₙ| ≥ 1 for every n, so it diverges Counterexample
- The Koch curve is a uniform limit of polygonal paths of lengths (4/3)ⁿ but is not rectifiable Counterexample
- The real complex-squaring map is locally but not globally invertible off the origin Counterexample
- The truncated decimal approximations of √2 form a Cauchy sequence of rationals with no rational limit Counterexample
- With aⱼ = (-1)ʲ/√j+1 convergent and bⱼ = (-1)ʲ bounded but not monotone, ∑ aⱼ bⱼ = ∑ 1/√j+1 diverges Counterexample
- x ↦ √x is a uniformly continuous bijection of [0,∞) onto itself whose inverse x ↦ x² is not uniformly continuous Counterexample
- xₖ = √k has xₖ₊₁ - xₖ → 0 and is not Cauchy Counterexample
- Algebraically constructible real numbers as the smallest real subfield closed under positive square roots Definition
- Real and imaginary parts, complex conjugation, and modulus Definition
- Riemann area between two continuous graphs and the disc as a vertically simple region Definition
- Square-summable families on an arbitrary index set and the space ℓ²(I) Definition
- The Euclidean inner product ⟨ x,y⟩ = ∑_k<n xₖ yₖ on ℝⁿ Definition
- The p-norms ‖ x‖ₚ for rational p ≥ 1, and ‖ x‖_∞ Definition
- Variance, standard deviation, and covariance on a finite probability space Definition
- √· on [0,∞) is uniformly continuous and exactly 1/2-Hölder, and is not Lipschitz Example
- √2 and (1+√5)/2 are algebraic integers, while 1/2 is not Example
- √2 exists in every complete ordered field, and is irrational Example
- A convergent sequence in ℝ³ and the integral ∫₀¹ (1, t, t²), computed componentwise Example
- A convergent series in ℝ² with Γ a line and Γ^⊥ a line, computed from the definition Example
- A Euclidean right triangle has minsize proportional to its scale Example
- Exact sine and cosine values at π/10, π/5, and 2π/5 Example
- Hilbert spaces are uniformly convex Example
- ℚ(√2,√3) has degree four and equals ℚ(√2+√3) Example
- ℚ(√2) carries exactly two distinct field orders, exchanged by the conjugation √2 ↦ -√2 Example
- ℚ(√2)/ℚ has degree two Example
…and 67 more results.
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
- W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 1 (Thm 1.21) (standard reference, not scraped)
- M. Spivak, Calculus, 4th ed., Ch. 8 (standard reference, not scraped)
- University of Colorado analysis notes: The real numbers (standard reference, not scraped)