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 continuous path on , with , is not rectifiable
Counterexample
Define by and for . Then is continuous, but the graph path is not rectifiable.
Facts & Assumptions
Given: The function and graph path .
The number is positive, and the shift formulas give for integers (Pi as twice the smallest positive zero of cosine, Quarter-turn values and shifts by pi/2 and pi).
The harmonic series diverges, the case of the rational -series theorem (For rational , converges iff ); a nonnegative series converges exactly when its partial sums are bounded above (A series of nonnegative terms converges iff its partial sums are bounded, and then the sum is their supremum).
Bounded variation means that all partition variation sums are bounded above (Bounded variation and total variation on an interval).
A path is rectifiable exactly when all of its coordinate functions have bounded variation (A path in is rectifiable exactly when every coordinate has bounded variation).
Reciprocals of positive naturals tend below every positive bound (For every in a complete ordered field there is a natural with ).
for every real (Parity and the Pythagorean identity for sine and cosine).
Verification
Since for , as ; away from zero it is continuous. Thus is a path.
Put . Positivity of and [L5] give , so choose with ; and [L1] gives .
For , take the partition whose points are , omitting a repeated endpoint if . Its variation contribution from consecutive is .
Since , [L2] says the tails are unbounded. Hence the variation sums in step 2.1 are unbounded and is not of bounded variation.
The first coordinate has bounded variation, but the second does not by step 3.1. Therefore [L4] says the graph path is not rectifiable.
Depends on
- A path in $\mathbb{R}^n$ is rectifiable exactly when every coordinate has bounded variation
- For rational $p > 0$, $\sum 1/k^p$ converges iff $p > 1$
- A series of nonnegative terms converges iff its partial sums are bounded, and then the sum is their supremum
- Pi as twice the smallest positive zero of cosine
- Quarter-turn values and shifts by pi/2 and pi
- Parity and the Pythagorean identity for sine and cosine
- For every $\varepsilon > 0$ in a complete ordered field there is a natural $n \ge 1$ with $1/n < \varepsilon$
- Bounded variation and total variation on an interval
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: 136 results over 24 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. R. Shastri, Metric Spaces, Section 6 (standard reference, not scraped)