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.
Null times divergent has no rule: with gives product limit , and with gives divergence
Statement refuted
That the product , left undefined by The extended real line , its order, and the arithmetic that is left undefined, could be given a value compatible with limits: that there is such that for all sequences of reals with (Limits and Cauchy sequences of reals) and (Divergence to and to ) the products have the single limiting behaviour named by .
Equivalently: that knowing a factor is null and the other diverges to determines anything at all about the product. It does not, and the two undefined entries in the arithmetic of are undefined for exactly this reason.
Facts & Assumptions
Given: The canonical naturals ; the sequence ; for a real the sequence ; and the sequence .
Canonical naturals: and invertible for , is strictly increasing, and for (Canonical naturals are positive and strictly increasing, Order on the natural numbers, is a linear order on ).
Archimedean facts: for every real there is a natural with , and for every real there is a natural with ; and gives (For every in a complete ordered field there is a natural with , Every complete ordered field is Archimedean, Inverses of positives are positive, and reciprocation reverses order).
Convergence to a real and divergence to ; to establish convergence it suffices to produce a threshold for every real ; a constant sequence converges to its value (Limits and Cauchy sequences of reals, Sequences of reals: bounded, eventually, frequently, tails, subsequences, Divergence to and to ).
A sequence diverging to is unbounded and therefore does not converge to any real (Divergence to and to , Every convergent sequence is bounded); a limit, when it exists, is unique (A sequence has at most one limit).
Order and field arithmetic: multiplying an inequality by a positive element preserves it; and ; for ; and the algebra of limits (Sign rules for products and monotonicity of multiplication, Order is preserved by adding a constant and by adding inequalities, The multiplicative identity is positive, Algebra of limits: sums, scalar multiples, products and quotients, Integer powers , Ordered field, Complete ordered field (least-upper-bound property)).
The product is left undefined in (The extended real line , its order, and the arithmetic that is left undefined).
Counterexample
The sequence is well defined, positive, and converges to : given a real , take a natural with ; for we have , hence .
For every real the sequence diverges to : given a real , the quotient is real, so there is a natural with , and for we get , hence after multiplying by .
The sequence diverges to : given a real , take a natural with ; for we have and , so .
For every real the product sequence is constant: for every , so it converges to .
The product with is , which diverges to by the argument of step 1.3 with the single factor, and therefore converges to no real number.
Now take the three pairs , and . In each, the first sequence is null and the second diverges to , so each pair satisfies the hypotheses of the refuted claim; but the three products converge to , converge to , and converge to in the extended sense. Since and limits are unique, no single describes all three, and the claim is false.
Remarks
-
This is why the entry is blank in the table. The extended real line , its order, and the arithmetic that is left undefined leaves undefined not out of caution but because any value assigned to it would make some instance of a product rule false, and the three pairs above already realise three different behaviours.
-
The same phenomenon rules out . Taking and gives a sum that is constantly , while and gives a sum diverging to ; both pairs have and .
-
Measure theory's convention is not a counterexample to this. Texts that set are fixing the value of a formula in a context where the factor is the measure of a null set, not asserting a limit rule; the distinction is spelled out in Which extended-real operations this library leaves undefined, and where each statement needs the hypothesis.
-
Index range. The classical statement writes and , which requires . Written on , which contains (Sequences of reals: bounded, eventually, frequently, tails, subsequences), the same sequences are and , as above.
Depends on
- The extended real line $\overline{\mathbb{R}} = \mathbb{R} \cup \{-\infty, +\infty\}$, its order, and the arithmetic that is left undefined
- Divergence to $+\infty$ and to $-\infty$
- Algebra of limits: sums, scalar multiples, products and quotients
- For every $\varepsilon > 0$ in a complete ordered field there is a natural $n \ge 1$ with $1/n < \varepsilon$
- Every complete ordered field is Archimedean
- Inverses of positives are positive, and reciprocation reverses order
- Canonical naturals are positive and strictly increasing
- A sequence has at most one limit
- Every convergent sequence is bounded
- Limits and Cauchy sequences of reals
- Sequences of reals: bounded, eventually, frequently, tails, subsequences
- Integer powers $a^m$
- Sign rules for products and monotonicity of multiplication
- Order is preserved by adding a constant and by adding inequalities
- The multiplicative identity is positive
- Order on the natural numbers
- $\le$ is a linear order on $\mathbb{N}$
- Ordered field
- Complete ordered field (least-upper-bound property)
Used by
Nothing in the library uses this result yet.
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 78 results over 25 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.
Sources
- Indeterminate form (Wikipedia) (standard reference, not scraped)
- Extended real number line (Wikipedia) (standard reference, not scraped)
- T. Tao, Analysis I, 3rd ed., §6.1 (standard reference, not scraped)