Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedaudited 2026-09-22
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.

Admissible cycle around a compact plane set

Statement

Let K⊆U⊆C with K compact and U open. Then:

  1. there is a finite polygonal complex cycle Γ in U∖K — a finite chain of directed line segments (Complex chains, their traces, and cycles, Filled complex triangles, their oriented three-edge boundary contours, diameter, and perimeter) — such that n(Γ,z)=1for every z∈K,n(Γ,z)=0for every z∉U;
  2. there are two such cycles β,γ, both with index 1 on K and 0 outside U, whose traces are disjoint, and which are nested: n(γ,w)=1for every w∈β∗,n(β,w)=0for every w∈γ∗.

All indices are those of Integration over a complex chain and the index of a chain. The construction is choice-free: the only selections are from the finitely many cells of a grid, and no supremum over an infinite family is used.

Facts & Assumptions

Given: A compact K and an open U with K⊆U⊆C.

[L1]

There is a compact Jordan set J, a finite union of closed rectangles of one axis-parallel grid with pairwise disjoint interiors, such that K⊆int⁡J⊆J⊆U; we write Q for its finitely many cells (A compact subset of an open Euclidean set has a compact Jordan neighborhood inside that open set).

[L2]

A finite sum of closed complex contours with integer coefficients is a complex chain; the trace of a sum is the union of the traces, a closed contour is a cycle, and the concatenation of the four sides ℓab,ℓbc,ℓcd,ℓda of an axis-parallel rectangle is a closed contour whose trace is its boundary (Complex chains, their traces, and cycles, Filled complex triangles, their oriented three-edge boundary contours, diameter, and perimeter, Goursat's theorem for rectangles: a holomorphic function integrates to zero around every rectangle contained in its domain).

[L3]

For a chain Γ and p∉Γ∗, the index is n(Γ,p)=12πi∫Γdzz−p; it is additive over sums of chains, and reversing a contour negates its index (Integration over a complex chain and the index of a chain, Chain integration and the index are additive in the chain, and reverse with it).

[L4]

For a closed complex contour γ and p∉γ∗, a continuous argument θ of γ−p exists along γ, and n(γ,p)=(θ(b)−θ(a))/2π (Every contour missing a point admits a continuous logarithm, unique up to a constant in 2πiZ, The winding number is the increment of a continuous argument divided by 2π).

[L5]

The index of a cycle is continuous, hence locally constant, on the complement of its trace, and is constant on every connected component of that complement (The index of a cycle is locally constant off its trace and vanishes far from it).

[L6]

If f is holomorphic on an open set containing a closed axis-parallel rectangle R, then ∫∂Rf dz=0 for the positively oriented boundary ∂R=ℓab∗ℓbc∗ℓcd∗ℓda (Goursat's theorem for rectangles: a holomorphic function integrates to zero around every rectangle contained in its domain).

Proof

technique · direct
1.1L2L4algebra

Cell index inside. Let Q be one of the closed grid rectangles, with ∂Q its positively oriented boundary, and let p∈Q∘. Along each of the four sides of Q the point ζ−p has a continuous argument: by [L4] a continuous argument θ of ∂Q−p exists, and along a side the perpendicular foot from p to the side's supporting line lies in the relative interior of the side, because both coordinates of p lie strictly between the corresponding coordinates of Q; hence θ varies monotonically along each side by exactly the angle subtended at p by that side, and the four such angles sum to 2π because the four triangles from p to the sides tile Q and their angles at p cover one full turn. By [L4], n(∂Q,p)=(θend−θstart)/2π=1.

1.2L2L4algebra

Cell index outside. Let Q be one of the closed grid rectangles and let p∉Q. Then p is strictly to the left of the left side, to the right of the right side, below the bottom side, or above the top side of Q; in each case the whole trace ∂Q∗ lies in an open half-plane bounded by a line through p, so a continuous argument of ∂Q−p takes values in an interval of length π; its increment is a multiple of 2π by [L4], hence 0, and n(∂Q,p)=0.

1.3L3L6

Cell index outside by Goursat. For Q and p∉Q the function z↦1/(z−p) is holomorphic on an open set containing Q, so [L6] gives ∫∂Qdz/(z−p)=0 and hence n(∂Q,p)=0 again; the two computations agree and either may be used below.

1.4L1L2algebra

Choose J and its cells Q as in [L1]. For each cell Q, write its four positively oriented directed side contours separately. Form Γ directly as the finite list of those directed side occurrences that are not shared with another cell; a shared grid side has exactly two occurrences, with opposite directions, and neither is put in Γ. This is a chain under [L2], without identifying it with or deleting terms from the list ∑Q∂Q. Its trace is exactly the exposed grid sides, hence ∂J. It is a cycle: the sum of the endpoint-boundary functions of all four sides of every cell is zero, while each omitted opposite pair also has zero endpoint-boundary function, so the remaining endpoint counts cancel at every grid vertex.

2.1step 1.1step 1.3step 1.4L3algebra

For p lying on no grid line, n(Γ,p)=∑Q∈Qn(∂Q,p)=1 if p∈J∘ and =0 if p∉J: the first equality holds because the omitted opposite pairs contribute zero to the index by [L3] and the index is additive, and the second because exactly one cell contains p in its interior when p∈J∘, while no cell contains p when p∉J.

3.1step 2.1L5

The index n(Γ,⋅) is continuous on C∖∂J by [L5]; since the points on no grid line are dense in C∖∂J, [step 2.1] extends by continuity to n(Γ,z)=1 for every z∈J∘ and n(Γ,z)=0 for every z∉J.

4.1step 3.1L1

Claim 1 follows with this Γ: K⊆int⁡J=J∘ and J⊆U, so n(Γ,z)=1 for z∈K; and z∉U implies z∉J, so n(Γ,z)=0; the trace of Γ is ∂J⊆J∖K⊆U∖K.

4.2step 1.4step 3.1L1

For claim 2, choose a compact Jordan set J2, again a finite union of grid rectangles, with K⊆int⁡J2⊆J2⊆int⁡J, and let β be the cycle obtained from J2 by the construction of [step 1.4]; then β∗=∂J2⊆int⁡J and γ∗=∂J are disjoint, and n(γ,w)=1 for every w∈int⁡J, in particular for every w∈∂J2=β∗.

5.1step 3.1step 4.2

With β and γ as in [step 4.2], also n(β,w)=0 for every w∈γ∗=∂J: indeed w∉J2 because ∂J∩J2=∅, and [step 3.1] applied to the Jordan set J2 gives n(β,w)=0 for w∉J2; moreover n(β,z)=1 for z∈K because K⊆int⁡J2.

6.1step 4.1step 4.2step 5.1∎

Claims 1 and 2 are established by [step 4.1] and [step 5.1] together with [step 4.2]: the cycle Γ, and the nested pair β,γ, have the stated index properties and traces.

Remarks

  • Why the index-one clause is the only one used to define f(a). Both Holomorphic functional calculus and its homomorphism theorem need a cycle whose index is exactly one on the spectrum and zero outside the holomorphy domain; the nested pair of claim 2 is what makes the product rule for the calculus a single separated double integral rather than a limiting argument.

  • Two different cycles, two different constructions of the same index. The argument-increment computation [step 1.1] and the Goursat computation [step 1.3] are independent, and both are used: the first identifies the index of a cell as one, the second as zero outside.

Depends on

Used by

Dependency tree · two levels

71 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