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.
Free tail ultrafilters and bounded real ultralimit calculus
Statement
Assuming AC, there is a free ultrafilter on . For any supplied ultrafilter on , every bounded real sequence has a unique ultralimit. For bounded sequences , limits , and ,
An inequality holding on a large set passes to the limits. Altering a sequence off a large set preserves its limit. For a free ultrafilter, an ordinary convergent bounded sequence has the same ultralimit. The supplied-ultrafilter assertions require no new choice.
Facts & Assumptions
Given: A supplied ultrafilter when discussing calculus; bounded real sequences; AC only for free-filter existence.
A non-null rational Cauchy sequence is eventually bounded away from zero. (A non-null Cauchy sequence is eventually bounded away from zero, with constant sign).
Rational ordered-field arithmetic holds. (The rationals form a totally ordered field).
Absolute value is multiplicative and satisfies the triangle and reverse triangle inequalities, also in any ordered field. (Absolute value and the triangle inequality).
Rational Cauchy sequences form a ring under termwise operations. (Cauchy sequences form a commutative ring).
Null sequences form an ideal of that ring. (Null sequences form an ideal).
A rational sequence is null when every positive rational tolerance eventually bounds its absolute value. (Null sequence).
The Cauchy reals have least upper bounds for nonempty bounded-above sets. (The Cauchy-sequence reals have the least-upper-bound property).
Under AC every proper filter extends to an ultrafilter. (The ultrafilter lemma, from the Axiom of Choice: every filter extends to an ultrafilter).
An ultrafilter contains exactly one of any set and its complement. (Characterisation of ultrafilters: every set or its complement).
AC supplies choice functions for families of nonempty sets. (The Axiom of Choice).
Proof
We first discharge the reciprocal input underlying the real-field/completeness interface. If , choose rational and with for . Set for and otherwise; all denominators used are nonzero.
The sets containing a tail of form a proper filter: intersections contain the later tail, supersets preserve containment, and no tail is empty. AC and [F8] extend it to an ultrafilter. No finite set belongs to the extension because a disjoint tail belongs; in particular it is not principal.
Least-upper-bound completeness implies that the natural multiples of are unbounded: if their supremum were , then would not be an upper bound, giving a natural and . Consequently for , since .
For a sequence , repeatedly bisect the current interval , retaining its left half if that half's preimage under is large, otherwise its right half. The right half is large in the latter case: intersect the large preimage of with the large complement of the left-half preimage. Thus each has large preimage, the intervals nest, and . This is a deterministic recursion.
For rational , take also beyond a Cauchy index of at tolerance . For , . The nonstrict comparison includes . Thus .
Set . All : for fixed , every later left endpoint lies below , and earlier ones lie below . For any , a sufficiently late has length less than , so its large preimage lies in . Thus is an ultralimit, also when .
The sequence is eventually zero, hence null. The ideal is proper since the constant fails the null test with tolerance . Every ideal containing and contains , hence all of . This proves its maximality and the reciprocal interface directly, without the erroneous strict intermediate comparison in the older maximality proof. The real completeness conclusion of [F7] is used with this corrected input.
If , their neighbourhoods of radius are disjoint by the triangle inequality. Their preimages cannot both belong to a proper filter. Hence the limit is unique. Equality of two sequences on a large set lets every neighbourhood test for one pass to the other by intersection; their limits therefore agree. A free ultrafilter contains no finite set: if a finite set were large but none of its singletons were large, intersecting their large complements from [F9] would contradict its largeness. A large singleton would make the ultrafilter principal by upward closure and the filter intersection axiom. Hence the complement of every finite set is large by [F9], so an ordinary convergent bounded sequence satisfies the same tests.
Intersect the two large error sets for and , each at tolerance . There . For use tolerance to obtain ; for the sequence is constant zero. Uniqueness identifies the stated limits.
If , intersect the large sets where both errors are less than . Then . Also , so absolute values converge to . These arguments apply to zero and unit constants as well.
If on a large set but , intersect that set with the two error sets of radius . It would give , impossible. Thus . All calculus constructions used only deterministic interval bisection and finite intersections once the ultrafilter was supplied; AC was spent only in the free-filter existence step.
Depends on
- Rescaled ultralimits and asymptotic cones
- The ultrafilter lemma, from the Axiom of Choice: every filter extends to an ultrafilter
- Characterisation of ultrafilters: every set or its complement
- Complete ordered field (least-upper-bound property)
- The Axiom of Choice
- The Cauchy-sequence reals have the least-upper-bound property
- A non-null Cauchy sequence is eventually bounded away from zero, with constant sign
- Cauchy sequences form a commutative ring
- Null sequences form an ideal
- Absolute value and the triangle inequality
- Null sequence
- The rationals form a totally ordered field
Used by
- Cones of a line and of real trees Example
- Scaling distinguishes sublinear minsize from a fixed perimeter cutoff Example
- Limits of geodesic segments, rays and lines Lemma
- Sublinear minsize identifies every cone segment with a limit segment Lemma
- The rescaled ultradistance defines a metric Lemma
- Sublinear triangle minsize implies hyperbolicity Theorem
Cited to discharge well-definedness by Rescaled ultralimits and asymptotic cones.
Dependency tree · two levels
38 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
- Drutu–Kapovich, Geometric Group Theory — §10.1 Lemma 10.25 and real ultralimit calculus; local rational reciprocal supplement (standard reference, not scraped)