CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-13

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 Koch curve is a uniform limit of polygonal paths of lengths $(4 / 3)^{n}$ but is not rectifiable

Counterexample

There are polygonal paths $κ_{n} : [0, 1] \to R^{2}$ that converge uniformly to a path $κ$ and satisfy

$L (κ_{n}) = {(\frac{4}{3})}^{n},$

yet the limit path is not rectifiable: $L (κ) = + \infty$ . The path $κ$ is one side of the Koch snowflake, so the closed snowflake boundary is nonrectifiable as well.

Facts & Assumptions

Given: The Euclidean plane and the unit interval.

[L1]

The recursion theorem produces a sequence once its initial value and update rule are specified (The recursion theorem).

[L2]

The real numbers are a complete ordered field (The Cauchy-sequence reals have the least-upper-bound property), so the nonnegative real $3$ has a square root (Square roots exist: a unique $\sqrt{a} \geq 0$ with $(\sqrt{a})^{2} = a$ ; the positives are ${x^{2} : x \neq 0}$ ); the standard basis gives the coordinate decomposition of vectors in $R^{2}$ (The standard list $e : n \to F^{n}$ with $e_{i} (i) = 1_{F}$ and $e_{i} (j) = 0_{F}$ for $j \neq i$ is an ordered basis of $F^{n}$ ; hence $\dim_{F} F^{n} = n$ , and $F^{0}$ is the zero space with basis $\emptyset$ and dimension $0$ ); and the Euclidean norm is homogeneous and satisfies the triangle inequality (Cauchy-Schwarz $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥_{2} ∥ y ∥_{2}$ with its equality case, the triangle inequality for $∥ \cdot ∥_{2}$ , the parallelogram law and polarisation).

[L3]

A uniformly Cauchy sequence of real-valued functions has a uniform limit; a uniform limit of continuous real-valued functions is continuous; and a vector-valued map is continuous exactly when its coordinates are continuous (A sequence of real-valued functions converges uniformly if and only if it is uniformly Cauchy, The uniform limit of continuous real-valued functions on a metric space is continuous, A vector-valued function has a limit, or is continuous, if and only if each of its components does; with the algebra of continuous vector-valued functions).

[L4]

The sequence $3^{- n}$ tends to zero, while $(4 / 3)^{n}$ tends to $+ \infty$ (For $∣ r ∣ < 1$ the sequence $r^{k}$ is null, and for $∣ r ∣ > 1$ the sequence $∣ r ∣^{k}$ diverges to $+ \infty$ ).

[L5]

Arc length is the supremum of inscribed polygonal sums, and a piecewise- $C^{1}$ polygonal path has length equal to the sum of its edge lengths (Paths in $R^{n}$ , inscribed polygonal sums, arc length as their supremum, and rectifiability, A continuous piecewise- $C^{1}$ path is rectifiable and its length is the sum of the speed integrals over its pieces).

[L6]

Uniform convergence gives only $L (κ) \leq {lim inf}_{n} L (κ_{n})$ (Arc length is lower semicontinuous under uniform convergence of paths).

[L7]

Euclidean isometries preserve length, and length is additive across subdivision points (A $C$ -Lipschitz map multiplies path length by at most $C$ ; isometries preserve length and scalar dilation multiplies it by the absolute scale, Arc length is additive across every subdivision point and decreases under restriction).

Verification

technique · construction

1.1

Define $R (x, y) : = (x / 2 - \sqrt{3} y / 2, \sqrt{3} x / 2 + y / 2)$ . Since $(\sqrt{3})^{2} = 3$ , direct expansion gives $∥ R v ∥_{2} = ∥ v ∥_{2}$ and $∥ v - R v ∥_{2} = ∥ v ∥_{2}$ for every $v \in R^{2}$ .

L2algebra

2.1

Put $κ_{0} (t) = (t, 0)$ . Recursively, suppose $κ_{n}$ is affine between consecutive points of $σ_{n} : = {j / 4^{n} : 0 \leq j \leq 4^{n}}$ . For an old edge from $A = κ_{n} (j / 4^{n})$ to $A + v = κ_{n} ((j + 1) / 4^{n})$ , prescribe the five successive values of $κ_{n + 1}$ at parameters $(4 j + r) / 4^{n + 1}$ , $0 \leq r \leq 4$ , to be $A$ , $A + v / 3$ , $A + v / 3 + R v / 3$ , $A + 2 v / 3$ , and $A + v$ , and make $κ_{n + 1}$ affine between them. The endpoint prescriptions agree on adjacent old edges, so [L1] gives the sequence.

step 1.1L1construct

3.1

Every old vertex is retained. By step 1.1, each old edge of length $ℓ$ is replaced by four edges of length $ℓ / 3$ . Induction therefore gives $4^{n}$ edges of length $3^{- n}$ in $κ_{n}$ , and [L5] gives $L (κ_{n}) = 4^{n} 3^{- n} = (4 / 3)^{n}$ .

step 1.1step 2.1L5algebra

4.1

On an old edge of length $3^{- n}$ , compare $κ_{n + 1}$ with the affine chord $κ_{n}$ . At the five subdivision parameters their differences have norms at most $0, 3^{- n} / 12, 3^{- n} / 2, 3^{- n} / 12, 0$ . On each intervening interval the difference is affine, so the triangle inequality gives $\sup_{t} ∥ κ_{n + 1} (t) - κ_{n} (t) ∥_{2} \leq 1 / (2 \cdot 3^{n})$ . Consequently, for $m > n$ , telescoping and the finite geometric-sum identity give $\sup_{t} ∥ κ_{m} (t) - κ_{n} (t) ∥_{2} < 3 / (4 \cdot 3^{n})$ .

step 1.1step 2.1step 3.1L2algebra

5.1

Each coordinate sequence is uniformly Cauchy by step 4.1, so [L3] supplies uniform coordinate limits. Let $κ$ be the resulting vector-valued limit. The inequality $∥ z ∥_{2} \leq ∣ z_{1} ∣ + ∣ z_{2} ∣$ , obtained from the coordinate decomposition and norm axioms in [L2], makes the convergence $κ_{n} \to κ$ uniform. Each $κ_{n}$ is continuous, and [L3] makes $κ$ continuous, hence a path.

step 4.1L2L3construct

6.1

Fix $n$ . Every vertex of $σ_{n}$ remains unchanged in every later path, so uniform convergence gives $κ (j / 4^{n}) = κ_{n} (j / 4^{n})$ for all $0 \leq j \leq 4^{n}$ . Thus the inscribed polygonal sum of $κ$ on $σ_{n}$ is $ℓ_{σ_{n}} (κ) = 4^{n} 3^{- n} = (4 / 3)^{n}$ . These sums are unbounded by [L4]. The defining supremum in [L5] is therefore $+ \infty$ , so $κ$ is not rectifiable.

step 3.1step 5.1L4L5

7.1

The classical Koch snowflake boundary is the concatenation of three isometric copies of $κ$ . By [L7], each copy is nonrectifiable, and a rectifiable concatenation would have rectifiable restrictions. Hence the snowflake boundary is nonrectifiable.

step 6.1L7

8.1

Lower semicontinuity is consistent with the result but cannot prove it: [L6] yields only $L (κ) \leq {lim inf}_{n} (4 / 3)^{n} = + \infty$ , a vacuous upper bound. The retained-vertex partitions in step 6.1 supply the necessary lower bounds.

step 3.1step 5.1step 6.1L4L6∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 196 results over 36 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

M. Ghomi, Curves and Surfaces, Lecture Notes 1, Exercise 9 (standard reference, not scraped)

The Koch curve is a uniform limit of polygonal paths of lengths (4/3)n(4/3)n but is not rectifiable