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.
Circular arcs, circumference as arc length, and diameter
Definition
Let and . A circular arc of the circle with centre and radius is a restriction
taken as a parametrized path rather than as its image; its trace is that image. The parameter interval is part of the arc, because a set of points does not determine a length: the same trace is swept by restrictions of different lengths.
The arc's length is the path length of Paths in , inscribed polygonal sums, arc length as their supremum, and rectifiability computed with the Euclidean norm of The -norms for rational , and . The circumference is for the once-around parameter interval , where is the constant of Pi as twice the smallest positive zero of cosine. Translation does not affect the value, so the notation suppresses . The diameter is .
The phrase once around is part of the convention: a parametrized path that repeats the same trace can have a larger length.
Depends on
Used by
- A twice-traversed circle has the same trace but twice the path length Counterexample
- Every circle has circumference 2 pi r and circumference-to-diameter ratio pi Theorem
- Inscribed regular-polygon perimeters increase to 2 pi, while circumscribed perimeters decrease to 2 pi Theorem
- The arc length of a unit semicircle is pi Theorem
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 100 results over 21 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)