LemmaStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-02

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.

Polygonal functions with sufficiently steep nonvertex slopes are dense in $C([0,1])$

Statement

For every $f\in C([0,1],\mathbb R)$ , every $\varepsilon>0$ , and every $M>0$ , there is a piecewise-affine $h$ with finitely many vertices such that $\lVert f-h\rVert_\infty<\varepsilon$ and every slope on a nonvertex affine piece has absolute value greater than $M$ .

Facts & Assumptions

Given: $f\in C([0,1],\mathbb R)$ , $\varepsilon>0$ , and $M>0$ .

[L1]

The function $f$ is uniformly continuous on $[0,1]$ (Heine-Cantor: a continuous map from a compact metric space to any metric space is uniformly continuous).

[L2]

Positive lengths admit arbitrarily fine equal subdivisions (For every $\varepsilon > 0$ in a complete ordered field there is a natural $n \ge 1$ with $1/n < \varepsilon$ ).

Proof

technique · constructive

1.1

By [L1], choose a finite partition $0=x_0<\cdots<x_r=1$ so that $|f(s)-f(t)|<\varepsilon/4$ whenever $s,t$ are in one partition interval. Let $g$ be the affine interpolant through $(x_i,f(x_i))$ .

L1construct

2.1

The affine-interpolation formula makes $|g(t)-f(t)|<\varepsilon/4$ on every partition interval. Let $S$ be the maximum of the finitely many absolute slopes of $g$ .

step 1.1algebra

3.1

Choose $0<\eta<\varepsilon/4$ . By [L2], subdivide every partition interval evenly enough to support a continuous triangular sawtooth $w$ , zero at the old vertices, with $\lVert w\rVert_\infty\le\eta$ and every nonvertex slope of absolute value greater than $S+M$ .

L2step 2.1construct

4.1

Put $h=g+w$ . On each new affine piece, the reverse triangle inequality gives $|h'|\ge|w'|-|g'|>M$ , while $\lVert h-f\rVert_\infty<\varepsilon/2<\varepsilon$ .

step 2.1step 3.1algebra

5.1

This $h$ has the required finite polygonal structure, approximation, and slope bound.

step 4.1discharge-construct∎

Depends on

Used by

Under Dependent Choice, continuous nowhere differentiable functions form a dense subset of C([0,1],ℝ) Theorem

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 52 results over 16 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

A generic continuous function is nowhere differentiable (standard reference, not scraped)

Polygonal functions with sufficiently steep nonvertex slopes are dense in C([0,1])C([0,1])C([0,1])