Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passaudited 2026-08-28
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.

Riemann extension across a holomorphic hypersurface zero set

Statement

Let UCm be a domain, let g:UC be holomorphic and not identically zero, and let f:UZ(g)C be holomorphic. Assume that f is locally bounded near every point of Z(g). Then there is a unique holomorphic extension F:UC with FUZ(g)=f.

Facts & Assumptions

Given: The domain U, the nonzero holomorphic function g, and the locally bounded holomorphic function f on UZ(g).

[L1]

One-variable locally bounded holomorphic functions extend across isolated punctures (Characterizations of removable singularities).

[L2]

After an invertible complex-linear coordinate change, a nonzero germ becomes regular in the last variable; that regular germ admits a Weierstrass preparation, and the resulting prepared polynomial has a fixed zero count on nearby slices (After a linear coordinate change, every nonzero germ is regular in the last variable, Weierstrass preparation theorem, Nearby slices of a regular germ have the same zero count).

[L3]

A contour integral is holomorphic in one complex parameter, the polydisc Cauchy formula specializes to the usual one-variable formula, and a locally bounded separately holomorphic function is holomorphic (A contour integral of a jointly continuous, parameter-holomorphic integrand is holomorphic, The iterated Cauchy integral formula on a polydisc, Locally bounded and separately holomorphic implies holomorphic).

[L4]

Holomorphic functions are separately holomorphic, and vanishing on a nonempty open subset of a domain forces global vanishing (A holomorphic function of several variables is continuous and separately holomorphic, A holomorphic function vanishing on a nonempty open subset of a domain vanishes identically).

Proof

technique · direct
1.1

Uniqueness is immediate from [L4]: if two holomorphic extensions agree with f on UZ(g), then their difference vanishes on the nonempty open set UZ(g) and hence vanishes identically on the domain U.

givenL4
1.2

Fix aZ(g). The germ of g at a is nonzero, else [L4] would make g vanish identically on U. To prove local extendability at a, we may translate a to 0 and compose with the invertible complex-linear coordinate change from [L2], because holomorphicity, local boundedness, and the existence of a local extension are preserved under such coordinate changes. After that change, [L2] makes the germ of g regular in zm and then yields a smaller product neighbourhood V×{ζ<r} on which g=uW with W Weierstrass, u nowhere zero, and W(z,ζ)0 for ζ=r. Shrinking once more if needed, u stays nonzero on this neighbourhood, so Z(g)=Z(W) there. The compact boundary cylinder V×{ζ=r} is therefore disjoint from Z(g), so f is holomorphic on a neighbourhood of it and hence bounded there.

givenL2L4
2.1

Fix zV. The slice ζf(z,ζ) is holomorphic on the disc ζ<r with the finitely many zeros of W(z,) removed. By step 1.2 it is bounded near each removed point, so [L1] extends that slice holomorphically across all of them. Call the extended slice Fz.

step 1.2L1
2.2

Define F(z,zm):=12πiζ=rf(z,ζ)ζzmdζ. Fixing all variables except one coordinate, [L4] makes the integrand holomorphic in that coordinate and [L3] makes the corresponding slice of F holomorphic. The boundedness from step 1.2 and the ML estimate make F locally bounded. Hence [L3] makes F holomorphic on V×{zm<r}.

step 1.2L3L4
3.1

For fixed z, the one-variable Cauchy formula from [L3] applied to the holomorphic slice extension Fz from step 2.1 shows that the integral in step 2.2 equals Fz(zm) for every zm<r. In particular, when W(z,zm)0 this value is the original f(z,zm). So step 2.2 gives a local holomorphic extension in the chosen coordinates, and undoing the coordinate change extends f across the original point a. By step 1.1 these local extensions agree on overlaps, and therefore glue to a unique global holomorphic extension on U.

step 1.1step 2.1step 2.2L3

Depends on

Used by

Dependency tree · two levels

64 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