Alphabeta MathHow 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.
Dropping injectivity double-counts under on two disjoint intervals
Statement refuted
False claim. The injectivity hypothesis may be removed from compact-Jordan change of variables when the derivative is nonzero everywhere on the domain.
Facts & Assumptions
Given: The open set , the compact Jordan set , the map given by , and on .
Compact-Jordan change of variables assumes injectivity (Change of variables for an injective map on a compact Jordan set).
The power rule gives (For a natural the function is differentiable everywhere with derivative ; for it is the constant , with derivative ; for a natural the function is differentiable at every with derivative ; consequently every polynomial function is differentiable at every real, with the derivative computed term by term), and the fundamental theorem evaluates its absolute-value integral (The second fundamental theorem: if is differentiable on with and is integrable, then ).
Counterexample
The derivative never vanishes anywhere on , but , so every point of has one preimage in each component of .
The image integral is its length, , while the proposed source integral is
The mismatch is exact double counting. Thus nonvanishing derivative does not replace injectivity, and [L1]'s hypothesis is essential.
Depends on
- Change of variables for an injective $C^1$ map on a compact Jordan set
- The second fundamental theorem: if $G$ is differentiable on $[a,b]$ with $G' = f$ and $f$ is integrable, then $\int_a^b f = G(b)-G(a)$
- For a natural $n \ge 1$ the function $x \mapsto x^{n}$ is differentiable everywhere with derivative $\iota(n)\,x^{\,n-1}$; for $n = 0$ it is the constant $1$, with derivative $0$; for a natural $n \ge 1$ the function $x \mapsto x^{-n}$ is differentiable at every $x \ne 0$ with derivative $-\iota(n)\,x^{-n-1}$; consequently every polynomial function is differentiable at every real, with the derivative computed term by term
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: 145 results over 25 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.