CounterexampleConstruction: AI-adaptedVerification: 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.

A twice-traversed circle has the same trace but twice the path length

Statement refuted

Two $C^{1}$ paths with the same trace must have the same length.

Facts & Assumptions

Given: The paths $γ (t) = (\cos t, \sin t), β (t) = (\cos (2 t), \sin (2 t)), 0 \leq t \leq 2 π .$

[L1]

The path $t \mapsto (\cos t, \sin t)$ on $[0, 2 π]$ is the once-around parametrization used to define unit-circle circumference (Circular arcs, circumference as arc length, and diameter).

[L2]

Vector differentiation is componentwise, $(\sin t)^{'} = \cos t$ , $(\cos t)^{'} = - \sin t$ , and $\sin^{2} t + \cos^{2} t = 1$ (The derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral, The derivatives of sine and cosine are cosine and minus sine, Parity and the Pythagorean identity for sine and cosine).

[L3]

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

[L4]

A $C^{1}$ path has length equal to the integral of its speed (If $γ : [a, b] \to R^{n}$ is continuous, differentiable on $(a, b)$ , and $γ^{'}$ extends continuously to $[a, b]$ , then $L (γ) = \int_{a}^{b} ∥ γ^{'} (t) ∥_{2} d t$ ).

[L5]

The integral of a constant $q$ on $[a, b]$ is $q (b - a)$ (If $m \leq f \leq M$ on $[a, b]$ then $m (b - a) \leq L (f, P) \leq \underline{\int_{a}^{b}} f \leq \overline{\int_{a}^{b}} f \leq U (f, P) \leq M (b - a)$ for every partition $P$ ; in particular every constant function is integrable, with $\int_{a}^{b} c = c (b - a)$ ).

Counterexample

technique · constructive

1.1

Each point $γ (s)$ , $0 \leq s \leq 2 π$ , equals $β (s / 2)$ , while periodicity in [L3] reduces every $β (t) = γ (2 t)$ to a parameter in $[0, 2 π]$ . Thus $γ$ and $β$ have the same unit-circle trace.

givenL1L3construct

1.2

By [L2], $∥ γ^{'} (t) ∥_{2} = 1$ and $∥ β^{'} (t) ∥_{2} = 2$ throughout the interval.

givenL2algebra

2.1

By [L4] and [L5], $L (γ) = \int_{0}^{2 π} 1 d t = 2 π, L (β) = \int_{0}^{2 π} 2 d t = 4 π .$

step 1.2L4L5

3.1

The traces coincide by step 1.1 but the lengths differ by step 2.1, so the statement is false. The once-around qualification in the definition of circumference prevents this multiplicity ambiguity.

step 1.1step 2.1L1discharge-construct∎

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: 187 results over 29 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

J. Lebl, Basic Analysis II, section 11.4.3 (standard reference, not scraped)