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.
The extended real line , its order, and the arithmetic that is left undefined
Definition
Fix two objects and , distinct from one another and neither of them a real number (The real numbers), and set
This is a new object, introduced here explicitly with its own order and its own partial arithmetic. It is not an enlargement of the field , and no operation of (Complete ordered field (least-upper-bound property)) is redefined by anything below.
The order. For declare
with ordered as in Order on the reals, and write for " and " as usual (Partial order and partially ordered set).
is a totally ordered set, and the inclusion of preserves and reflects the order. All four checks are immediate from the displayed clauses.
- Reflexive. For one of the first two clauses applies; for the third does, since in .
- Antisymmetric. Suppose and . If then forces , since the clause fails and are not both real. Symmetrically forces , and or forces the other to be . In the one remaining situation and are both real and antisymmetry is that of .
- Transitive. Let . If or the conclusion is one of the first two clauses. Otherwise forces, in , either or ; and forces, in , either or . The value is incompatible with the second alternative pair, so is real, hence so are and , and transitivity is that of .
- Total. If or then ; if or then ; otherwise both are real and the order of is total.
- Preserved and reflected. For the first two clauses fail, so in says exactly in .
In particular is the least and the greatest element of , and for every .
Reflection. Extend negation by
keeping the field negative on . The resulting map , , satisfies and
For and real this is the elementwise order reversal in : translation invariance (Order is preserved by adding a constant and by adding inequalities) applied with the constant turns into and, applied with the constant , turns it back, while holds exactly when . In every other case both sides are decided by the first two clauses of the order: makes both sides true, as does , and if , and are not both real then one of , holds and both sides are false.
Partial addition. For the sum is defined by
- = the field sum, when ;
- when and , or and ;
- when and , or and ;
and the two sums and are left undefined. Addition is commutative where defined, and
each side being defined exactly when the other is: the excluded pairs are exchanged by , and the three clauses above are exchanged accordingly.
Partial multiplication. For the product is defined by
- = the field product, when ;
- when one of is , the other is , and both are or both are ;
- when one of is , the other is , and one is and the other ;
and every product with one factor and the other is left undefined. The comparisons and here are taken in the order above, under which .
Nothing else is defined. There is no subtraction, no division, no exponentiation and no absolute value on in this library; where such an expression is wanted it is written out in the two defined operations, and where a case falls in the undefined list the statement carries an explicit hypothesis saying so.
Definition references
Remarks
-
is not a field, and not an ordered field. It has no additive inverse for : is whenever it is defined and is never . So none of the field axioms (Complete ordered field (least-upper-bound property)) is available here, and no algebraic manipulation valid in may be transported to without a separate justification.
-
Why the excluded cases are excluded. The three defined clauses of each operation are exactly the cases in which the value is forced by the limiting behaviour of the sequences involved, and the excluded cases are exactly the ones in which it is not. For the product this is proved on the companion page: Null times divergent has no rule: with gives product limit , and with gives divergence ↗ exhibits a null sequence and two sequences diverging to whose products behave differently, so no value assigned to could be compatible with products of limits. The same phenomenon rules out a value for : with and the sum is constantly , while with it diverges to . Leaving them undefined is not squeamishness, it is the only option that keeps every later statement about limits true without a side condition hidden inside the arithmetic.
-
This is the separate introduction that Conventions: , unbounded sets, and the extended reals points to. That remark refuses the conventions and inside , and records that the extended real line is introduced explicitly here, with its own order and its own partial arithmetic kept separate from rather than quietly extending it. This is that introduction. The suprema and infima of Complete ordered field (least-upper-bound property), Greatest lower bound (infimum) and the whole suprema page remain real numbers with their nonempty and bounded hypotheses intact; what is new is a separate supremum operation, taken in and named as such, supplied by Every subset of has a least upper bound and a greatest lower bound in , agreeing with the real supremum and infimum on nonempty sets bounded in .
-
The symbols were already in circulation, and this definition does not change what they meant. Divergence to and to defines the single phrase "" as an abbreviation for a condition on , and says in as many words that it does not define an object named . That reading is still correct: nothing in Divergence to and to is restated or reinterpreted here, and Convergence in and the extended subsequential limit set: is an extended subsequential limit when some subsequence converges to , or diverges to is where the two are related, by a definition that quotes the old one rather than replacing it. Likewise the interval notation of Intervals of : the nine order-convex forms, nondegeneracy, and length is notation for a condition on one side, not an endpoint, and stays that way.
-
Why the order is defined by three clauses rather than by a picture. The clauses are what the verifications above actually use, and they make the two facts that later proofs lean on immediate: every element is and every element is , with no case analysis at the point of use.