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.
Multipoint analytic extension with a bounded exterior dual
Statement
Let be a strongly graded Möbius or conformal vertex algebra with trivial auxiliary grading. All modules considered below are strongly graded generalized -modules with that trivial auxiliary grading, including the explicit three-operator Möbius structure when applicable. Consider an arbitrary finite composable chain of logarithmic intertwining operators, with leaf modules and intermediate modules . Assume these leaves and intermediate modules are C1-cofinite and quasi-finite-dimensional in the real-weight convention. Assume the output is quasi-finite-dimensional. Then for every and leaf vectors the scalar product coefficient converges absolutely for , continues multivalued analytically to distinct nonzero insertion points, and has a finite power/log convergent regular-singular expansion in every finite nested-cluster boundary chart and its simultaneous boundary intersections, including infinity. More precisely, in boundary coordinates and nonsingular shape parameters it is a finite sum of products times convergent Laurent series with a finite lower bound in each coordinate; finite integral shifts can be absorbed into the powers. Powers and logarithms carry the continued branches. No C1 condition on , tensor-product existence, category closure, or global uniform nilpotence assumption on is made.
Statement references
Facts & Assumptions
Given: The actual finite chain and exact finiteness hypotheses of the Statement. Fix a real cutoff containing the finite generalized-weight support of .
Finite Jacobi quotient with a bounded exterior dual and C1-cofinite leaves supplies the finite quotient , its flat connection and global Ward relation, the actual formal coefficient map, finite nested-cluster charts, and monic Euler equations at each finite boundary with parameter-holomorphic coefficients. Only the leaves are C1-reduced; the exterior dual stays in its finite weight cutoff.
Parameter-uniform convergence of formal Euler series proves convergence on every smaller disk of a formal solution of a monic scalar Euler equation with holomorphic parameter coefficients, and its finite exponent/log extension. It is a local proved analytic implication, not a published conformal-block theorem used as a premise.
Strongly graded contragredient duality for Möbius and conformal modules, C1-cofinite generalized module in the ungraded HLZ convention, Quasi-finite-dimensional generalized module and Logarithmic intertwining operator supply actual opposite duals, finite real cutoffs, mode/weight identities and derivative/Jacobi axioms.
Proof
Every C1-cofinite quasi-finite module occurring among leaves or intermediates has finitely many weight cosets modulo and a uniform nilpotence exponent. Quasi-finiteness gives a lower bound as in F1. Choose finitely many homogeneous C1 representatives; expansion into positive-state terms lowers the inner weight by a positive integer, so it terminates at those representatives. They generate the module, and its weights lie in their finitely many real integer cosets. The nilpotent part commutes with each homogeneous mode, because both and its semisimple part have the same integral mode shift. A power killing the finitely many representatives therefore kills their generated module. For the final output only the finite-dimensional exterior space is used, and has a finite nilpotence exponent on it without any C1 assumption on . The intertwiner bracket identifies differentiation in on a fixed block with . The three commuting operators have nilpotent sum of order at most the sum of their nilpotence exponents minus2, by the multinomial formula. Thus the scalar chain has finitely many real exponent cosets and one finite logarithmic-degree bound. To specify the support precisely, split the inputs into homogeneous components and write , and for the projected weight in . Put , . The th insertion power is . For , , the scale power is , and the power is . Each intermediate weight is lower bounded, so these RATIO supports, and the innermost support, are lower bounded after finitely many shifts. Individual outer powers need not have a common lower bound. The displayed ratio powers determine the entire intermediate-weight tuple injectively; logarithmic substitutions are finite polynomial substitutions and do not alter that power map.
We give the local analytic bundle argument needed for continuation. The finite -module has a finite presentation, because is Noetherian. Choose finitely many generators and relations. On a small configuration-space polydisc express the derivatives of generators by holomorphic matrices; connection stability expresses the differentiated relation vectors by holomorphic combinations of finitely many relation vectors. Along each coordinate segment solve the dual finite generator equation by Picard iteration. Its th iterated integral is bounded by , so it converges. The pairings with the relation vectors satisfy their closed finite homogeneous ODE and vanish at the initial point, so they remain zero by the same uniqueness estimate. Hence transport acts on the actual quotient dual fibers. Flatness on the quotient makes it independent of the order of coordinate segments: its formal Taylor coefficients are the same commuting covariant derivatives, and analytic Taylor uniqueness identifies the local solutions. Transport along a path and its reverse are inverse, so fiber dimensions are locally constant. If a presentation has generators and quotient dimension at one point, a nonzero -minor of its relation matrix and the transported independent fiber functionals keep its rank exactly nearby. Elementary elimination by that invertible minor then gives a free holomorphic quotient of rank . This proves local freeness and a flat analytic bundle without assuming algebraic flatness or citing a several-variable differential-system theorem. Its local horizontal solutions continue uniquely along every path; finitely subdividing a homotopy square into such neighborhoods proves homotopy invariance.
We first construct only a convergent germ. Induct on chain length. For one intertwiner, fixed homogeneous inputs and a homogeneous restricted-dual vector give a finite power/log polynomial by the bracket. For a longer chain set and . At a fixed exponent and logarithmic degree, the coefficient of is an algebraic vector in one finite-dimensional generalized-weight space of . After choosing a basis of that particular space, its pairing through the remaining operators is a FINITE sum of shorter-chain scalar coefficients. The final leaf module of each shorter chain is , which is C1-cofinite and quasi-finite by hypothesis; no completed vector is inserted into an operator. By induction those coefficient functions are holomorphic on a coherently continued branch of the full outer radial domain. Choose one simply connected generic polydisc in that domain and use the same branches for all coefficients. Fix finite tensor representatives generating and finite presentation relations among them. Add the finitely many tensors used in their connection matrices and all tensor terms used in those finite relations; split each into its finitely many homogeneous components. Include the fixed tensor whose scalar coefficient is sought. For this ONE finite family, intersect the generic Euler neighborhoods supplied by F1 and shrink to a product , meeting the radial domain, with all inverted outer positions and differences bounded away from zero on smaller parameter compacts. F1's formal Ward and derivative identities remain identities after replacing each coefficient by its shorter-chain analytic sum: every rational function in has a lower-bounded Laurent expansion in here, and a fixed coefficient in its product with a lower-bounded coefficient series uses only finitely many terms. In each such coefficient identity the remaining formal outer series are the prescribed shorter-chain series, convergent by induction; rational multiplication is evaluated on the same branch and sufficiently small outer product neighborhood. For an Euler relation obtained after localization at an additional generic chart denominator, first clear its finitely many denominators (and, if necessary, the finite localization power witnessing equality in ) to obtain an actual -module relation. Apply the same coefficient argument to that cleared relation and divide only on the chosen neighborhood where those denominators are nonzero. The identity theorem continues the resulting zero identity to . This is a coefficientwise finite-convolution argument, not interchange of an unproved multiple projection sum. In particular each of the actual -coefficient families satisfies its F1 monic Euler equation with the holomorphic parameter coefficients on this small product. Step 1.1 supplies the finite exponent/log and lower-support hypotheses, so F2 converges every family normally on smaller disks and compact subsets of . Joint holomorphy and the Cauchy formula in a slightly larger parameter polydisc justify every outer derivative termwise as well as the derivatives supplied by F2. Thus the finite presentation relations and generator connection identities hold analytically: their formal coefficient differences are zero, and the normally convergent finite power/log sums are therefore zero. The generator values descend to a horizontal functional on the actual quotient. For an arbitrary tensor, finite -linear reduction to the and its formal F1 relation identify its prescribed series with the evaluation of that same germ; the coefficients in this reduction are analytic at the chosen nonsingular configurations and have only finite lower poles. Step 1.2 continues the quotient germ along every configuration-space path. No claim is made that its scalar Euler equation has holomorphic coefficients on the full radial disk; its apparent poles away from this neighborhood are bypassed by the holomorphic quotient connection. All-index absolute convergence of the original projection sum will be proved from coefficient recovery and product Cauchy bounds below.
F1 gives regular-singular Euler equations at EVERY finite boundary scale, including exceptional cluster scales. The preservation of pole order plus tensor weight by its leaf-only reductions is the exact proof for these exceptional scales, not an assertion that original smooth-divisor bounds survive blowup. Each fixed finite set of quotient generators has a finite collection of Euler companion systems , holomorphic in and parameters when the other boundary scales are nonzero. This applies to every horizontal functional, since it is a quotient identity, not merely a differential equation for the original chain.
Infinity needs no reflection of the exterior dual into an unbounded leaf module. Choose a maximal diverging insertion as pivot and put , , so . All ratios are bounded on its projective chart; repeat the finite cluster charts of F1 for their coinciding shapes. The global relation imposed in gives, for every horizontal functional , Differentiate the right side in ; its coordinate derivative plus its tensor actions are exactly F1's relation , so the derivative is zero and equality follows at , then by continuation. The actions on any fixed finite generating tensor space are finite-dimensional, preserve its real-weight cutoff, and are finite powers times log polynomials. Thus the transformation is a finite power/log gauge on the finite bundle, not an infinite dual-C1 reduction. The normalized coordinates and differences are monomials in and the cluster scales times holomorphic units. Pulling back a finite Euler system through gives coefficient , holomorphic, and tensoring its finite power/log gauge is again an Euler system. Consequently every generic infinity boundary has an actual regular-singular Euler system for all horizontal functionals, with parameter-holomorphic coefficients. Finite charts cover all such boundaries by choosing a maximal projective pivot; nested growth rates and clusters are handled by the same repeated difference charts. No C1 property of the reflected dual or closure under contragredients has been used.
We prove the simultaneous-boundary assertion explicitly. On a boundary polydisc , continue a horizontal fundamental frame on its universal cover and evaluate it on the finite quotient generators, giving a matrix . Coordinate monodromies commute because the punctured polydisc has commuting coordinate loops; homotopy invariance follows from step 1.2. Choose commuting logarithms with : choose a scalar logarithm on each generalized eigenspace and use the finite nilpotent logarithm series; polynomial interpolation makes each a polynomial in , so all commute. Then is single-valued holomorphic on that punctured polydisc. Fix one scale and a relatively compact parameter polydisc in a nonempty generic open subset of the remaining punctured parameters, where the finitely many Euler systems in steps 2.2–3.1 are holomorphic down to . Such an open subset suffices; no equation without apparent poles on the entire chart is assumed. Shrinking its disk gives a common matrix bound . On one full lifted angular turn their values at radius have a common finite bound . The radial integral equation and its fold iterated integrals give . The matrix factor is bounded by on the same angular turn, by its finite generalized-eigenspace expansion. Other factors are bounded on that parameter compact set. Thus . Cauchy's circle formula for its negative Laurent coefficient gives for . This proves separate meromorphicity with locally uniform finite pole order away from the other axes.
We extend that finite pole bound across the exceptional parameter values. For one entry of and one scale , its Laurent coefficients are holomorphic on the entire connected domain of the remaining punctured parameters: define them by a fixed small circle locally in those parameters, and use one-variable Cauchy deformation to identify the definitions on overlaps. On a parameter polydisc compactly contained in the generic open subset of step 4.1 the bound is uniform, so every coefficient below one integer vanishes there. The identity theorem then makes each such coefficient zero throughout the connected punctured parameter domain, including parameter values where that scalar Euler equation has extra poles. Do this for the finitely many entries and scales and take the largest bounds. The iterated Laurent expansion of has no negative exponent. It is a convergent Taylor series on every smaller full polydisc: iterated circle integrals give its coefficients, bounded on a larger product torus by a product of inverse radius powers, and the geometric series for the Cauchy kernels recovers the function on each smaller product annulus. There is no remaining negative part, so that Taylor series extends through every coordinate hyperplane and their intersections. Finally the commuting-matrix factor is a finite sum of products of coordinate powers and log polynomials, by simultaneous generalized-eigenspace decomposition. Multiplication gives the asserted finite power/log convergent Laurent expansion of the continued germ at every finite nested-cluster intersection, and at infinity by step 3.1. Only the small generic Euler equations were needed for this conclusion.
It remains to identify the actual radial projection sum on its FULL domain. Put and for . Fix in a small simply connected neighborhood of a nonzero value. The radial domain is exactly the product : every is , and every difference is such a monomial times a unit , nonzero throughout this product. The radial corner is a nested-cluster chart. On the logarithm cover of the ENTIRE punctured unit polydisc, step 1.2 supplies a horizontal frame and steps 4.1–5.1 give commuting monodromies, their logarithms and a single-valued holomorphic untwisted matrix . Its Laurent coefficients are independent of the chosen radii, by iterated one-variable annulus Cauchy deformation. Their finite lower bounds, proved near the radial corner in step 5.1, therefore hold on the entire punctured unit polydisc. For the fixed scalar evaluation under consideration, augment the finite tested generator rows by its tensor and, if necessary, the finitely many translates in its dilation gauge. F1 applies to every one of those finitely many tensors, so the same argument gives its own untwisted row with finite lower Laurent bounds. On any product torus , and this row are bounded; its coefficients satisfy . For , summation over is a product of convergent geometric series. Consequently this SAME finite power/log expansion converges absolutely and normally on every compact subset of the full radial logarithm cover. The scale contributes only the finite power/log dilation gauge of step 3.1.
We identify the prescribed original coefficients successively. First hold in the simply connected polydisc from step 2.1 and expand in . On their common small domain, the full-ratio expansion from step 6.1 and the actual series converged by F2 represent the same quotient germ. If is the finite set of actual exponent classes and its logarithmic-degree bound, that initial germ is killed by . The zero identity continues throughout the connected radial logarithm domain by analytic uniqueness. Thus the cyclic monodromy span of this actual germ has no additional eigenclasses. The full quotient frame may have other, even nonreal, exponents; their contribution to the actual coefficient is zero, not a new hypothesis on all quotient solutions. Here is the needed finite exponent/log uniqueness. Include the finitely many exponent classes occurring in BOTH expressions. On a fixed class , the continuation operator for one positive loop acts as times translation , with nilpotent difference of order at most one plus the finite log-degree bound. Distinct classes have distinct eigenvalues. The Chinese remainder identity for the finitely many relatively prime polynomials constructs polynomial projectors in onto their generalized eigenspaces. They separate the finite class sum without rearranging any infinite series. On one class write the difference as , each a convergent integer Laurent series bounded below. Applying kills lower log degrees and gives . If the difference is zero, ordinary Laurent uniqueness gives every coefficient of equal to zero. Descending in log degree proves all coefficients zero. Continuation and finite differences are legitimate on the small punctured disk where both expansions converge; the finite-dimensional continuation matrix of the quotient supplies the same action there. Thus the analytic coefficients coincide on with the algebraic finite sums of shorter-chain coefficients described in step 2.1. These extracted coefficient functions are holomorphic on the entire connected outer radial logarithm domain. Indeed a loop is the last ratio loop, and the radial domain is the product from step 6.1, so that loop has one fixed monodromy matrix under the marking on the outer logarithm domain. Polynomial class projections and log differences are finite holomorphic operations. After removing the finite powers/logs, each Laurent coefficient is a fixed-circle integral on a sufficiently small circle locally in ; overlapping choices agree by annulus Cauchy deformation. Replacing by changes coefficients by a finite triangular polynomial operation in outer logarithms, which are holomorphic on this domain. The shorter-chain coefficient functions also extend holomorphically there by induction. The identity theorem therefore extends their equality from to that connected domain. Repeat this one-variable extraction in , then , and so on. For each FIXED previously extracted index the inserted vector is still algebraic in a finite weight space, so induction applies at every stage; no uniform estimate over the previously extracted indices is needed for this identification. The outcome identifies every iterated coefficient with the scalar obtained from the original finite-dimensional weight projections in their prescribed order. Finally, the explicit triangular power map in step 1.1 converts this iterated coefficient identity to the ratio coefficients. It is injective on intermediate-weight tuples, and each logarithmic coordinate change is a finite invertible polynomial substitution. The ratio supports are bounded below in every coordinate, as proved there, so this conversion is coefficientwise meaningful. Uniform summability over ALL indices comes from the independent product-torus bounds of step 6.1, not from interchanging the successive extraction with an unproved multiple sum.
For homogeneous leaf and exterior vectors, step 1.1 sends a tuple to the ratio powers , with the fixed scale power . Step 7.1 therefore identifies the weight-projected scalar coefficient with the corresponding convergent power/log coefficient family in step 6.1. Each projection is a single algebraic vector evaluation; a basis expansion inside its finite-dimensional weight space is finite, and no estimate on absolute sums of arbitrary basis coordinates as that dimension grows is asserted or needed. After choosing one representative of each of the finitely many exponent-class tuples and absorbing finite shifts, distinct weight tuples WITHIN ONE fixed class tuple give distinct integral ratio-power tuples. Globally the finite exponent-class label together with the integral ratio-power tuple uniquely determines the weight tuple; identical integer indices in different class families are retained as distinct terms. The original term for each tuple is a polynomial in finitely many logarithms, of one uniformly bounded degree by step 1.1. The finite monodromy decomposition expresses its scalar coefficients as fixed finite linear combinations of entries of the single-valued Laurent rows in step 6.1, with only finite integral shifts; any unused exponent class is zero by the uniqueness argument of step 7.1. Their product Cauchy bounds thus give for each of these finitely many scalar coefficient families. On a compact subset with and bounded continued logarithms, multiplication by the fixed finite powers and log polynomials changes only the compact constant. For each fixed class family, summation over the lower-bounded is the product of convergent geometric series; summing these bounds over the finitely many class families remains finite. Hence the sum of the absolute values of the WHOLE projected scalar terms over all intermediate-weight tuples converges normally on compact subsets of the full radial logarithm domain. Finite homogeneous decompositions give the result for arbitrary leaf vectors and . The analytic continuation and simultaneous boundary/infinity expansions were obtained for this same germ in steps 1.2 and 3.1–5.1. For there are no ratio variables or intermediate projections and step 2.1 already gives the result. The full Statement is therefore retained without any output-dual C1 assumption or an assertion that a scalar elimination equation has no apparent poles.
Depends on
Finite Jacobi quotient with a bounded exterior dual and C1-cofinite leaves
Parameter-uniform convergence of formal Euler series
Strongly graded contragredient duality for Möbius and conformal modules
C1-cofinite generalized module in the ungraded HLZ convention
Quasi-finite-dimensional generalized module
Logarithmic intertwining operator
Dependency tree · 2 levels
Sources
- Huang, Lepowsky and Zhang, Part VII, Theorem 11.6, Remark 11.7 and the multipoint conclusion of Theorem 11.8
- Huang, Differential equations and intertwining operators, §§1–2; the proof here uses bounded exterior weights rather than assuming output-dual C1-cofiniteness
- Yuto Moriwaki, Vertex operator algebra and parenthesized braid operad