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.
Omitting the absolute value from the Jacobian gives negative length under the reflection
Statement refuted
False claim. In the unoriented change-of-variables formula, one may replace by .
Facts & Assumptions
Given: The reflection on and the constant function on its image.
The one-dimensional unoriented formula uses the absolute derivative (In one dimension the compact-Jordan formula is substitution over the unoriented image interval with the absolute derivative).
Oriented substitution records orientation through the order of its endpoint limits (Substitution: if is differentiable on with integrable and is continuous on an interval containing , then ).
Counterexample
The image is , so its unoriented length integral is .
Since , the proposed un-absolute right side is , not .
With the required absolute value, [L1] gives . The negative value in step 2.1 instead belongs to the oriented formula [L2], whose image endpoints occur in reverse order. Hence the claim is false.
Depends on
- In one dimension the compact-Jordan formula is substitution over the unoriented image interval with the absolute derivative
- Substitution: if $\varphi$ is differentiable on $[c,d]$ with $\varphi'$ integrable and $f$ is continuous on an interval containing $\varphi([c,d])$, then $\int_{\varphi(c)}^{\varphi(d)} f = \int_c^d (f\circ\varphi)\,\varphi'$
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: 85 results over 18 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.