LemmaStatement: AI-adaptedProof: AI-generatedprecheck passverified 2026-08-02 (claude-opus-5)

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.

For a positive cut $A$ , the reciprocal $A^{- 1}$ satisfies $A \cdot A^{- 1} = 1^{*}$

Statement

For $A > 0^{*}$ , the reciprocal $A^{- 1}$ (Multiplication and reciprocals of Dedekind cuts) is a Dedekind cut with $A^{- 1} > 0^{*}$ , and $A \cdot A^{- 1} = 1^{*}$ .

Facts & Assumptions

Given: A cut $A$ with $A > 0^{*}$ , and the multiplicative identity $1^{*} = {r \in Q : r < 1}$ .

[L1]

Nonnegative product: for $A, B > 0^{*}$ , $A \cdot B = {q \leq 0} \cup {a b : a \in A, b \in B, a > 0, b > 0}$ (Multiplication and reciprocals of Dedekind cuts).

[L2]

Reciprocal: for $A > 0^{*}$ , $A^{- 1} = {p \leq 0} \cup {p > 0 : \exists s \in Q, s > 0, s \notin A, p < 1 / s}$ (Multiplication and reciprocals of Dedekind cuts).

[L3]

$A > 0^{*}$ means $A$ contains a positive rational; and every cut is a proper, downward-closed set of rationals with no greatest element (Order on the Dedekind reals, Dedekind cut).

[L4]

$Q$ is a field: rational addition and multiplication are commutative and associative, multiplication distributes over addition, and every nonzero rational is invertible (The rationals form a field); the order is total, $x \leq y$ implies $x + z \leq y + z$ , and $0 < x$ , $0 < y$ imply $0 < x y$ (The rationals form a totally ordered field).

[L6]

Every nonempty subset $S \subseteq N$ has a least element: there is $ℓ \in S$ with $ℓ \leq s$ for all $s \in S$ (The well-ordering principle).

[L5]

Rational power growth: for a rational $y > 1$ one has $y^{n} \geq 1 + n (y - 1)$ for every natural $n \geq 1$ , by induction from $Q$ arithmetic — at $n = 1$ both sides are $y$ , and if $y^{n} \geq 1 + n (y - 1)$ then, multiplying by $y > 0$ and writing $y = 1 + (y - 1)$ , $y^{n + 1} \geq (1 + (y - 1)) (1 + n (y - 1)) = 1 + (n + 1) (y - 1) + n (y - 1)^{2} \geq 1 + (n + 1) (y - 1)$ because $n (y - 1)^{2} \geq 0$ ; and by the Archimedean property every rational is exceeded by some such power; since a cut is proper it omits a rational upper bound, so for any $a_{0} > 0$ some $a_{0} y^{n} \notin A$ (The rationals are Archimedean, Dedekind cut).

Proof

technique · direct

1.1

$A^{- 1}$ is a cut with $A^{- 1} > 0^{*}$ : since $A > 0^{*}$ contains $0$ and hence, by downward closure, all rationals $\leq 0$ , every $s \notin A$ is positive; fix $a_{0} \in A$ with $a_{0} > 0$ , so any positive $p \in A^{- 1}$ has $p < 1 / s < 1 / a_{0}$ (its witness $s \notin A$ satisfies $s > a_{0}$ ), making $A^{- 1}$ proper; it is nonempty (it contains $0$ ) and downward closed: a $q \leq 0$ lies in the ${p \leq 0}$ clause, and if $0 < q < p$ with $p \in A^{- 1}$ carrying witness $s$ ( $p < 1 / s$ ) then $q < p < 1 / s$ , so $q \in A^{- 1}$ with the same witness $s$ ; it contains a positive $p$ (take any $s \notin A$ and $0 < p < 1 / s$ ), and has no greatest element: a $p \leq 0$ is exceeded by the positive element just exhibited, while any positive $p \in A^{- 1}$ carries a witness $s > 0$ , $s \notin A$ with $p < 1 / s$ , and the rational $p^{'} = (p + 1 / s) / 2$ satisfies $p < p^{'} < 1 / s$ , so $p^{'}$ lies in $A^{- 1}$ with the same witness $s$ yet $p^{'} > p$ .

L2L3L4

1.2

Inclusion $A \cdot A^{- 1} \subseteq 1^{*}$ : any $q \leq 0$ in $A \cdot A^{- 1}$ lies in $1^{*}$ , and if $a \in A$ , $p \in A^{- 1}$ with $a, p > 0$ , choose $s \notin A$ , $s > 0$ , $p < 1 / s$ , so $a < s$ (as $a \in A$ , $s \notin A$ ) and $a p < s \cdot (1 / s) = 1$ , giving $a p \in 1^{*}$ .

L1L2L3L4

1.3

For the reverse inclusion fix a target $x$ with $0 < x < 1$ : pick a rational $t$ with $x < t < 1$ (betweenness in $Q$ ) and set $y : = 1 / t$ , so $y > 1$ ; choose $a_{0} \in A$ with $a_{0} > 0$ (as $A > 0^{*}$ ); by rational power growth some power $a_{0} y^{n} \notin A$ , so ${n \geq 1 : a_{0} y^{n} \notin A}$ is a nonempty set of naturals.

L3L4L5

2.1

Let $n \geq 1$ be the least natural with $a_{0} y^{n} \notin A$ (nonempty by step 1.3; $n \geq 1$ since $a_{0} y^{0} = a_{0} \in A$ ); by minimality $a : = a_{0} y^{n - 1} \in A$ with $a > 0$ , while $s : = a_{0} y^{n} = a \cdot y \notin A$ with $s > 0$ .

L4L6step 1.3choose

3.1

Set $p : = x / a > 0$ ; since $x < t = 1 / y$ gives $1 / x > y$ , we get $1 / p = a / x > a \cdot y = s$ , so $p < 1 / s$ with $s > 0$ , $s \notin A$ , whence $p \in A^{- 1}$ by the reciprocal's definition; then $x = a \cdot p$ with $a \in A$ , $p \in A^{- 1}$ , $a, p > 0$ , so $x \in A \cdot A^{- 1}$ , and with the ${q \leq 0}$ clause this yields $1^{*} \subseteq A \cdot A^{- 1}$ .

L1L2L4step 1.1step 1.3step 2.1algebra

4.1

Combining the two inclusions gives $A \cdot A^{- 1} = 1^{*}$ , and by step 1.1 the reciprocal $A^{- 1}$ is a Dedekind cut with $A^{- 1} > 0^{*}$ .

step 1.1step 1.2step 3.1∎

Depends on

Used by

The Dedekind reals form a field Theorem

Dependency tree · two levels

26 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 (Appendix: construction of ℝ) (standard reference, not scraped)
M. Girotti, Addendum — Construction of $\mathbb{R}$ via Dedekind's method (MATH 317, Advanced Calculus of One Variable) (standard reference, not scraped)
Construction of the real numbers (Wikipedia) (standard reference, not scraped)

For a positive cut AA, the reciprocal A−1A−1 satisfies A⋅A−1=1∗A⋅A−1=1∗