Alphabeta Math
PropositionStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + claude-sonnet-5)audited 2026-08-17
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.

Vanishing integrals around triangles construct a primitive for a continuous function on a star-shaped domain

Statement

Let UC be open and star-shaped with respect to aU in the sense of Complex star-shaped and convex domains are the published Euclidean notions under the identification C=R2, and let f:UC be continuous. Suppose

Δ[u,v,w]f(ζ)dζ=0

for every filled triangle Δ[u,v,w]U in the sense of Filled complex triangles, their oriented three-edge boundary contours, diameter, and perimeter. Then

F(z)=azf(ζ)dζ

is holomorphic on U and satisfies F(z)=f(z) for every zU. Thus F is a primitive of f as defined in A primitive of a complex function on an open set.

Facts & Assumptions

Given: An open set U star-shaped with respect to a, a continuous f:UC, and vanishing boundary integral for every filled triangle contained in U.

[L1]

Reversal negates a contour integral and concatenation adds contour integrals (Complex line integrals change sign under reversal and add under concatenation).

[L2]

On a piecewise-C1 contour, the complex line integral agrees with the usual parametric integral (For piecewise-C1 contours the Riemann–Stieltjes integral agrees with the parametric complex integral and the published real line integrals).

[L3]

Complex line integrals are linear in the integrand, and the ML estimate bounds their modulus by a uniform integrand bound times contour length (Complex line integrals are linear in the integrand, ML estimate: a contour integral is bounded by a supremum bound times path length).

[L4]

A primitive of f on an open set is a holomorphic function whose derivative equals f there (A primitive of a complex function on an open set).

[L5]

A continuous integrand has a complex line integral along every rectifiable contour (Continuous integrands have complex and absolute line integrals along every rectifiable path).

Proof

technique · direct
1.1

Fix zU. The segment az is rectifiable and f is continuous on it, so F(z) exists by [L5]. Since U is open, choose ρ>0 with B(z,ρ)U. If 0<h<ρ, the short segment from z to z+h lies in that ball, and every segment from a to a point of the short segment lies in U by star-shapedness; hence Δ[a,z,z+h]U.

givenL5choose
1.2

Parametrizing the short edge by ζ=z+th and using [L2] gives z,z+hf(z)dζ=f(z)h.

L2algebra
2.1

The zero boundary integral of that triangle reads F(z)+z,z+hfF(z+h)=0 by [L1], and therefore F(z+h)F(z)=z,z+hf(ζ)dζ.

step 1.1L1
3.1

By [L3], steps 2.1 and 1.2 imply (F(z+h)F(z))/hf(z)sup0t1f(z+th)f(z).

step 2.1step 1.2L3
4.1

Continuity of f at z makes the right side of step 3.1 tend to zero as h0. Thus F(z)=f(z) for arbitrary zU, including z=a; [L4] says exactly that F is a primitive, and h=0 was only the excluded difference-quotient value.

step 3.1L4

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 123 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