CounterexampleConstruction: Literature-sourcedVerification: 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.

The vector field (y,0) gives different integrals along two paths with the same endpoints

Statement refuted

The field $F (x, y) = (y, 0)$ has the same vector line integral along every path from $(0, 0)$ to $(1, 0)$ .

Facts & Assumptions

Given: The paths $α (t) = (t, 0)$ and $β (t) = (t, t (1 - t))$ on $[0, 1]$ .

[L1]

A vector line integral is the integral of $⟨ F (γ (t)), γ^{'} (t) ⟩$ on a $C^{1}$ path (Scalar line integrals with respect to arc length and vector-field line integrals).

[L2]

Vector line integrals add under concatenation and negate under reversal (Line integrals under reversal and concatenation).

[L3]

Path independence is equivalent to zero integral around every closed piecewise- $C^{1}$ path on a piecewise- $C^{1}$ path-connected domain (Path independence is equivalent to zero integral around every closed piecewise-C1 path).

[L4]

The power rule (For a natural $n \geq 1$ the function $x \mapsto x^{n}$ is differentiable everywhere with derivative $ι (n) x^{n - 1}$ ; for $n = 0$ it is the constant $1$ , with derivative $0$ ; for a natural $n \geq 1$ the function $x \mapsto x^{- n}$ is differentiable at every $x \neq 0$ with derivative $- ι (n) x^{- n - 1}$ ; consequently every polynomial function is differentiable at every real, with the derivative computed term by term), together with Newton-Leibniz for a continuous function whose interior derivative admits an integrable extension (Newton–Leibniz needs only continuity on $[a, b]$ , differentiability on $(a, b)$ , and a Riemann-integrable extension of the interior derivative), evaluates polynomial integrals by endpoint increments.

Counterexample

technique · constructive

1.1

Both paths run from $(0, 0)$ to $(1, 0)$ . Along $α$ , the first component $y$ is zero, so [L1] gives $\int_{α} F \cdot d r = 0$ .

givenL1algebraconstruct

1.2

Along $β$ , one has $F (β (t)) = (t (1 - t), 0)$ and $β^{'} (t) = (1, 1 - 2 t)$ . Hence [L1] and [L4] give $\int_{β} F \cdot d r = \int_{0}^{1} (t - t^{2}) d t = \frac{1}{6} .$

givenL1L4algebra

2.1

The two values differ, so the field is not path-independent.

step 1.1step 1.2

3.1

The concatenation $α * β^{-}$ is closed, and [L2] gives its integral as $0 - 1 / 6 = - 1 / 6$ . This is the corresponding nonzero-loop failure in [L3].

step 1.1step 1.2L2L3discharge-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: 96 results over 20 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, Example 9.3.1 (standard reference, not scraped)