Alphabeta Math
ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-26
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.

Dixon's gluing traced on the boundary cycle of an annulus

Example

Let Ω={z:12<∣z∣<3}, let C1(t)=exp⁡(it) and C2(t)=2exp⁡(it) on [0,2π], let Γ=C2−C1 and let f(z)=1/z, holomorphic on Ω. Then Γ is a cycle with trace {∣z∣=1}∪{∣z∣=2}⊆Ω, null-homologous in Ω, and

Ω0={z∉Γ∗:n(Γ,z)=0}={∣z∣<1}∪{∣z∣>2},Ω∪Ω0=C.

Dixon's glued function is identically zero here: the transform

h1(z)=12πi∫Γf(ζ)ζ−z dζ

vanishes at every z∈Ω0, by direct computation and not only by Liouville's theorem. At z=32, which lies in Ω off the trace, both sides of the global Cauchy formula equal 23.

Facts & Assumptions

Given: The sets and contours above, with f(z)=1/z.

[L1]

If Ω is open, f is holomorphic on Ω, and Γ is a null-homologous cycle with trace in Ω, then, with g the filled difference quotient of f, the function equal to (2πi)−1∫Γg(ζ,z) dζ on Ω and to (2πi)−1∫Γf(ζ)(ζ−z)−1 dζ on Ω0 is a well-defined entire function, bounded and tending to 0 at infinity (Dixon's glued function is entire and vanishes at infinity). The filled difference quotient is (f(ζ)−f(z))/(ζ−z) off the diagonal and f′(z) on it (The filled difference quotient of a holomorphic function is jointly continuous).

[L2]

For a cycle null-homologous in an open Ω and f holomorphic there, n(Γ,z)f(z)=(2πi)−1∫Γf(ζ)(ζ−z)−1 dζ for every z∈Ω∖Γ∗ (Cauchy's integral formula for a null-homologous cycle).

[L3]

For p∈C and 0<r1<r2 the chain built from the positively oriented circles of radii r2 and r1 about p with coefficients +1 and −1 is a cycle with trace the two circles, index 0 for ∣z−p∣<r1, 1 for r1<∣z−p∣<r2 and 0 for ∣z−p∣>r2; it is null-homologous in {s1<∣z−p∣<s2} whenever 0<s1<r1 and r2<s2 (The boundary cycle of a round annulus has index 1 inside the annulus and 0 on either side).

[L4]

A cycle with trace in an open Ω is null-homologous in Ω when its index vanishes at every point outside Ω (Null-homologous cycles and homologous cycles in an open set).

[L5]

∫Γf dz=∑k<r, mk≠0mk∫γkf dz, and for z∉Γ∗ one has n(Γ,z)=(2πi)−1∫Γdζ/(ζ−z) (Integration over a complex chain and the index of a chain); a chain is a finite list of integer-weighted contours (Complex chains, their traces, and cycles).

[L6]

For a∈C, r>0 and every integer m, the positively oriented circle γ(t)=a+rexp⁡(it) on [0,2π] satisfies ∫γ(z−a)m dz=2πi when m=−1 and 0 otherwise (On a positively oriented circle about a, the integral of (z-a)^m is zero for every integer m except -1, and is 2 pi i for m=-1).

[L7]

Chain integration and the index are additive in the chain and reverse with it (Chain integration and the index are additive in the chain, and reverse with it); complex line integrals are linear in the integrand (Complex line integrals are linear in the integrand).

[L8]

For a∈C, r>0 and k∈Z, the contour a+rexp⁡(ikt) on [0,2π] has index k for ∣z−a∣<r and 0 for ∣z−a∣>r (A circle traversed k times has winding number k inside and 0 outside).

[L9]

Every bounded entire function is constant (Liouville's theorem: every bounded entire function is constant).

[L10]

Nonvanishing quotients of functions complex differentiable at a point are complex differentiable there (Linearity, product, reciprocal, and quotient rules for complex derivatives).

Verification

technique · direct
1.1givenL3L4L5

By [L3] with p=0, r1=1, r2=2, s1=12 and s2=3, the chain Γ is a cycle with trace {∣z∣=1}∪{∣z∣=2} contained in Ω, its index is 0 for ∣z∣<1, 1 for 1<∣z∣<2 and 0 for ∣z∣>2, and it is null-homologous in Ω. Hence Ω0={∣z∣<1}∪{∣z∣>2}, and Ω∪Ω0=C because a point with ∣z∣≤12 or ∣z∣≥3 lies in Ω0.

1.2givenL10

The function f(z)=1/z is holomorphic on Ω by [L10], since 0∉Ω.

2.1step 1.1step 1.2L5L6L7L8algebra

For z∈Ω0 with z≠0 and ζ on either circle, the identity 1ζ(ζ−z)=1z(1ζ−z−1ζ) holds, and [L5], [L6] and [L8] give ∫Cjdζζ−z=2πi n(Cj,z) and ∫Cjdζζ=2πi. For ∣z∣<1 both indices are 1, so each circle integral is 1z(2πi−2πi)=0; for ∣z∣>2 both indices are 0, so each is 1z(0−2πi)=−2πi/z. In both cases [L7] gives h1(z)=0 as the difference of the two equal circle contributions.

2.2step 1.1L5L6

At z=0 the integrand is ζ−2, and [L6] with m=−2 gives ∫Cjζ−2 dζ=0 for both circles, so h1(0)=0 as well.

3.1step 2.1step 2.2L1L9

Steps 2.1 and 2.2 give h1≡0 on Ω0; by [L1] the glued function agrees with h1 there and is entire and bounded, so [L9] makes it the constant 0, and the value on Ω is therefore 0 too.

4.1step 1.1step 2.1step 3.1L2L6L7L8algebra∎

Take z=32, so 1<∣z∣<2 and z∈Ω∖Γ∗. The left side of [L2] is n(Γ,z)f(z)=1⋅23=23 by step 1.1. For the right side, step 2.1's partial-fraction identity with n(C2,z)=1 and n(C1,z)=0 from [L8] gives ∫C2dζζ(ζ−z)=1z(2πi−2πi)=0 and ∫C1dζζ(ζ−z)=1z(0−2πi)=−2πi/z, so by [L7] the right side is 12πi(0+2πi/z)=1z=23. The two sides agree.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

85 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