LemmaStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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.

Nearest-integer probe points for the Weierstrass function

Statement

Let $0 < a < 1$ , let $b > 1$ be an odd integer, and fix $x_{0} \in R$ . For each $m \in N$ , define

$k_{m} : = ⌊ b^{m} x_{0} + \frac{1}{2} ⌋, z_{m} : = b^{m} x_{0} - k_{m}, x_{m} : = \frac{k_{m} + 1}{b^{m}} .$

Then $k_{m}$ is an integer, $- 1 / 2 \leq z_{m} < 1 / 2$ , and $0 < x_{m} - x_{0} \leq 3 / (2 b^{m})$ and $x_{m} \to x_{0}$ .

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} π)$ .

Facts & Assumptions

Given: Parameters and points as in the Statement.

[L1]

In the classical Weierstrass construction, $0 < a < 1$ and $b > 1$ is an odd integer (The classical Weierstrass function).

[L2]

For every real $x$ there is exactly one integer $k$ with $k \leq x < k + 1$ , namely $k = ⌊ x ⌋$ (Integer part: for every real $x$ there is exactly one integer $m$ with $m \leq x < m + 1$ ).

[L3]

If $∣ r ∣ > 1$ , then $∣ r ∣^{m}$ diverges to $+ \infty$ (For $∣ r ∣ < 1$ the sequence $r^{k}$ is null, and for $∣ r ∣ > 1$ the sequence $∣ r ∣^{k}$ diverges to $+ \infty$ ).

[L4]

For all reals $x, y$ , $\cos (x + y) = \cos x \cos y - \sin x \sin y$ (The addition formulas for sine and cosine).

[L5]

Both sine and cosine have period $2 π$ (The zero sets of sine and cosine and the least positive common period 2 pi).

[L6]

For every real $x$ , $\sin (x + π) = - \sin x$ and $\cos (x + π) = - \cos x$ , with $\sin 0 = 0$ and $\cos 0 = 1$ (Quarter-turn values and shifts by pi/2 and pi, The derivatives of sine and cosine are cosine and minus sine).

Proof

technique · direct

1.1

Apply [L2] to $b^{m} x_{0} + 1 / 2$ . The resulting integer $k_{m}$ satisfies $k_{m} \leq b^{m} x_{0} + 1 / 2 < k_{m} + 1$ , hence $- 1 / 2 \leq z_{m} = b^{m} x_{0} - k_{m} < 1 / 2$ .

L1L2constructalgebra

2.1

Since $x_{m} - x_{0} = (1 - z_{m}) / b^{m}$ , step 1.1 and $b^{m} > 0$ give $0 < x_{m} - x_{0} \leq 3 / (2 b^{m})$ .

step 1.1algebra

3.1

Let $ε > 0$ . By [L3], for all sufficiently large $m$ one has $b^{m} > 3 / (2 ε)$ , hence step 2.1 gives $0 < x_{m} - x_{0} \leq 3 / (2 b^{m}) < ε$ . Thus $x_{m} \to x_{0}$ .

step 2.1L3algebra

4.1

For $n \geq m$ , the integer $b^{n - m}$ is odd. The identities $b^{n} x_{m} = b^{n - m} (k_{m} + 1)$ and $b^{n} x_{0} = b^{n - m} (k_{m} + z_{m})$ , followed by repeated use of [L4] to shift through integer multiples of $π$ , give the two asserted cosine values; oddness preserves the parity of $k_{m}$ and reverses the parity of $k_{m} + 1$ .

step 1.1L1L4L5L6algebra∎

Depends on

Used by

Dependency tree · two levels

47 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, equations (4) to (6) (standard reference, not scraped)