Alphabeta Math
PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck 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 U⊆C be open and star-shaped with respect to a∈U in the sense of Complex star-shaped and convex domains are the published Euclidean notions under the identification C=R2, and let f:U→C 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 z∈U. 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:U→C, 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.1givenL5choose

Fix z∈U. 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.

1.2L2algebra

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

2.1step 1.1L1

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

3.1step 2.1step 1.2L3

By [L3], steps 2.1 and 1.2 imply ∣(F(z+h)−F(z))/h−f(z)∣≤sup⁡0≤t≤1∣f(z+th)−f(z)∣.

4.1step 3.1L4∎

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

Depends on

Used by

Dependency tree · two levels

34 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources