Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-21
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.

Weissinger's fixed-point criterion for summably contracting iterates

Statement

Let (X,d) be a nonempty complete metric space and let T:X→X. Suppose nonnegative reals (am)m≥1 satisfy ∑m≥1am<∞ and

d(Tmx,Tmy)≤amd(x,y)(x,y∈X,m≥1).

Summably contracting iterates have a unique fixed point and the iteration tail bounds its error. Explicitly, for xk+1=Txk and the fixed point x∗,

d(xn,x∗)≤d(x1,x0)∑m≥nam(n≥1).

Facts & Assumptions

Given: The complete metric space, map, constants, and starting point in the Statement.

[L1]

Absolute convergence implies convergence for a real series (If ∑∣ak∣ converges then ∑ak converges).

[L2]

In a complete metric space every Cauchy sequence converges to a point of the space (Complete metric space: every Cauchy sequence converges in the space).

Proof

technique · direct
1.1givenL1algebra

For p>n, telescoping and the iterate estimate give d(xp,xn)≤d(x1,x0)∑m=np−1am; by [L1] the tails tend to zero, so (xn) is Cauchy.

2.1step 1.1L2algebra∎

By [L2], xn→x∗∈X; letting p→∞ in step 1.1 gives the stated tail bound. The m=1 estimate makes T continuous, hence Tx∗=x∗, and since summability gives some am<1, two fixed points u,v satisfy d(u,v)=d(Tmu,Tmv)≤amd(u,v) and are equal.

Depends on

Used by

Dependency tree · two levels

32 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