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.

Low-frequency bound for the Weierstrass difference quotient

Statement

Use the parameters and probe points of Nearest-integer probe points for the Weierstrass function, and suppose $a b > 1$ . Put

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

Then $A_{0} = 0$ and, for every $m \in N$ ,

$∣ A_{m} ∣ \leq π (x_{m} - x_{0}) \frac{(a b)^{m} - 1}{a b - 1} .$

In particular, for every $m \geq 1$ ,

$∣ A_{m} ∣ < π (a b)^{m} (x_{m} - x_{0}) / (a b - 1) .$

Facts & Assumptions

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

[L1]

$∣ \cos u - \cos v ∣ \leq ∣ u - v ∣$ for all real $u, v$ (Sine and cosine are $1$ -Lipschitz on $R$ ).

[L2]

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

[L3]

Finite sums satisfy $\sum_{n < 0} c_{n} = 0$ and $\sum_{n < m + 1} c_{n} = \sum_{n < m} c_{n} + c_{m}$ (Finite sums and finite products, by recursion).

[L4]

Finite sums preserve termwise inequalities and commute with scalar multiplication (Laws of finite sums and finite products, claims 2 and 4).

[L5]

For reals $x, y$ , $∣ x + y ∣ \leq ∣ x ∣ + ∣ y ∣$ (The triangle inequality).

[L6]

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

The displayed finite sum defines $A_{m}$ , and [L3] gives $A_{0} = 0$ .

givenL2L3construct

1.2

Multiplying the finite sum $\sum_{n < m} (a b)^{n}$ by $a b - 1$ and telescoping gives $(a b - 1) \sum_{n < m} (a b)^{n} = (a b)^{m} - 1$ , including at $m = 0$ ; since $a b - 1 > 0$ , $\sum_{n < m} (a b)^{n} = \frac{(a b)^{m} - 1}{a b - 1} .$

givenL3algebra

2.1

Repeated use of [L5], followed by [L1] on each summand and [L4], gives $∣ A_{m} ∣ \leq \sum_{n < m} a^{n} b^{n} π ∣ x_{m} - x_{0} ∣ = π (x_{m} - x_{0}) \sum_{n < m} (a b)^{n},$ where [L2] supplies $x_{m} - x_{0} > 0$ and [L6] supplies $π > 0$ .

step 1.1L1L2L4L5L6algebra

3.1

Substitute step 1.2 into step 2.1. For $m \geq 1$ , one has $(a b)^{m} - 1 < (a b)^{m}$ and the other factors are positive, so the strict displayed bound follows; at $m = 0$ , the non-strict formula already gives $A_{0} = 0$ .

step 1.2step 2.1algebra∎

Depends on

Used by

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

Dependency tree · two levels

34 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 1 (standard reference, not scraped)