LemmaStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 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.

The Weierstrass tail has one sign and dominates at the probe points

Statement

Use the parameters and probe points of Nearest-integer probe points for the Weierstrass function. Put

$B_{m} : = \sum_{n = m}^{\infty} a^{n} (\cos (b^{n} π x_{m}) - \cos (b^{n} π x_{0})) .$

This tail converges absolutely, all of its summands have the same weak sign, and

$∣ B_{m} ∣ \geq (2 / 3) (a b)^{m} (x_{m} - x_{0}) .$

Facts & Assumptions

Given: Parameters $0 < a < 1$ , an odd integer $b > 1$ , a real $x_{0}$ , and the associated $k_{m}, z_{m}, x_{m}$ .

[L1]

The series defining $W_{a, b}$ converges absolutely at every real point (The classical Weierstrass series converges uniformly to a continuous function).

[L2]

For every $n \geq m$ , $\cos (b^{n} π x_{m}) = - (- 1)^{k_{m}}$ and $\cos (b^{n} π x_{0}) = (- 1)^{k_{m}} \cos (b^{n - m} z_{m} π)$ (Nearest-integer probe points for the Weierstrass function).

[L3]

The probes satisfy $- 1 / 2 \leq z_{m} < 1 / 2$ and $0 < x_{m} - x_{0} \leq 3 / (2 b^{m})$ (Nearest-integer probe points for the Weierstrass function).

[L4]

Cosine is strictly decreasing on $[0, π]$ , strictly increasing on $[- π, 0]$ by parity, and has range $[- 1, 1]$ (Signs, monotonicity intervals, and ranges of sine and cosine, Parity and the Pythagorean identity for sine and cosine).

[L5]

$\cos (π / 2) = 0$ (Quarter-turn values and shifts by pi/2 and pi).

[L6]

If a convergent real sequence is eventually nonnegative, then its limit is nonnegative; more generally, eventual non-strict inequalities pass to limits (Limits preserve non-strict inequalities).

[L7]

The number $π = 2 γ$ is positive because the smallest positive zero of cosine satisfies $γ \in (0, 2)$ (Pi as twice the smallest positive zero of cosine, Cosine has a smallest positive zero, lying strictly between zero and two).

Proof

technique · direct

1.1

Absolute convergence in [L1] licenses subtraction of the two convergent series and defines the displayed tail $B_{m}$ .

L1construct

1.2

Since $∣ z_{m} ∣ \leq 1 / 2$ and $π > 0$ by [L7], parity and monotonicity in [L4], together with [L5], give $\cos (z_{m} π) = \cos (∣ z_{m} ∣ π) \geq \cos (π / 2) = 0$ .

L3L4L5L7

2.1

By [L2], every summand of $B_{m}$ is $- (- 1)^{k_{m}} a^{n} (1 + \cos (b^{n - m} z_{m} π)) .$ The parenthesized factor is nonnegative by the range clause of [L4], so the partial sums share one weak sign. Their absolute values therefore converge to $∣ B_{m} ∣$ and dominate the absolute value of the $n = m$ term by [L6]; step 1.2 makes that term at least $a^{m}$ . Hence $∣ B_{m} ∣ \geq a^{m}$ .

step 1.1step 1.2L2L4L6algebra

3.1

The upper bound in [L3] gives $1 \geq (2 b^{m} / 3) (x_{m} - x_{0})$ . Multiplying step 2.1 by this nonnegative bound yields $∣ B_{m} ∣ \geq (2 / 3) (a b)^{m} (x_{m} - x_{0})$ .

step 2.1L3algebra∎

Depends on

Used by

Under ab>1+3π/2, the classical Weierstrass function is continuous everywhere and differentiable nowhere Theorem

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

Jeff Calder, Weierstrass's Non-Differentiable Function, proof of Theorem 1, step 2 (standard reference, not scraped)