Alphabeta Math
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 vortex field is closed but not exact on the punctured plane

Statement refuted

Every closed C1 vector field on a piecewise-C1 path-connected open set is exact.

Facts & Assumptions

Given: On U=R2∖{(0,0)}, let F(x,y)=(−yx2+y2,xx2+y2).

[L1]

With coordinates indexed from 0, so that F=(F0,F1) and ∂0,∂1 are ∂x,∂y, closedness requires ∂yF0=∂xF1, while exactness requires a C2 potential whose gradient is F (Exact and closed C1 vector fields).

[L2]

A gradient line integral is its potential's endpoint increment and is therefore zero on a closed path (The gradient theorem: the line integral of a gradient is the endpoint increment).

[L3]

On a nonempty open piecewise-C1 path-connected domain, conservativity, path independence, and zero closed-loop integrals are equivalent (Conservative, path-independent, and zero-closed-loop conditions are equivalent).

[L4]

Vector line integrals use the integrand ⟨F(γ(t)),γ′(t)⟩ (Scalar line integrals with respect to arc length and vector-field line integrals).

[L5]

Sine and cosine have derivatives cos⁡t and −sin⁡t and satisfy sin⁡2t+cos⁡2t=1 (The derivatives of sine and cosine are cosine and minus sine, Parity and the Pythagorean identity for sine and cosine).

[L6]

The integral of the constant 1 on [0,2π] is 2π, and π>0 (If m≤f≤M on [a,b] then m(b−a)≤L(f,P)≤∫ab‾f≤∫ab‾f≤U(f,P)≤M(b−a) for every partition P; in particular every constant function is integrable, with ∫abc=c(b−a), Pi as twice the smallest positive zero of cosine).

Counterexample

technique · constructive
1.1

The rational formulas defining F are C1 on U. Direct differentiation gives ∂yF0=y2−x2(x2+y2)2=∂xF1, so F is closed by [L1].

givenL1algebraconstruct
1.2

The punctured plane is piecewise-C1 path-connected: choose a positive radius at least as large as the radii of two given points, join each point outward along its own ray to that circle, and join the resulting points by a circular arc. None of these pieces meets the origin.

given
1.3

On the counterclockwise unit circle γ(t)=(cos⁡t,sin⁡t), 0≤t≤2π, [L5] gives F(γ(t))=(−sin⁡t,cos⁡t)=γ′(t).

givenL5algebra
2.1

By [L4], [L5], and [L6], ∫γF⋅dr=∫02π(sin⁡2t+cos⁡2t) dt=2π≠0.

step 1.3L4L5L6
3.1

If F were exact, [L1] would give a potential and [L2] would make the closed-circle integral zero, contradicting step 2.1. Thus F is closed but not exact. By [L3] and step 1.2, it is also neither conservative nor path-independent.

step 1.1step 1.2step 2.1L1L2L3
4.1

The domain is not star-shaped: for any proposed centre a≠0, the segment from a to −a passes through the omitted origin.

givenstep 3.1algebradischarge-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: 128 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