LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

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.

Formal delta substitution identity for module Jacobi

Statement

With the two-variable formal delta distribution and binomial expansions of Formal distributions and fields on a vector space,

z_{0}^{- 1} δ ⁣ (\frac{z_{1} - z_{2}}{z_{0}}) - z_{0}^{- 1} δ ⁣ (\frac{z_{2} - z_{1}}{- z_{0}}) = z_{2}^{- 1} δ ⁣ (\frac{z_{1} - z_{0}}{z_{2}}),

where the first term expands in nonnegative powers of $z_{2}$ , the second in nonnegative powers of $z_{1}$ , and the right side in nonnegative powers of $z_{0}$ .

Facts & Assumptions

Given: Three independent formal variables $z_{0}, z_{1}, z_{2}$ and the formal delta and binomial-expansion conventions of Formal distributions and fields on a vector space.

[F1]

Formal distributions and fields on a vector space: for every integer $r$ , $ι_{z_{1}, z_{2}} (z_{1} - z_{2})^{r} = \sum_{j \geq 0} (\binom{r}{j}) (- 1)^{j} z_{1}^{r - j} z_{2}^{j}$ and $ι_{z_{2}, z_{1}} (z_{1} - z_{2})^{r} = \sum_{j \geq 0} (\binom{r}{j}) z_{1}^{j} (- z_{2})^{r - j}$ ; $δ (x) = \sum_{n \in Z} x^{n}$ .

Proof

1.1F1algebra

For $N \geq 0$ , the coefficient of $z_{0}^{- N - 1}$ in the first term is the polynomial $(z_{1} - z_{2})^{N}$ expanded in $z_{2}$ . In the second term the same coefficient is $(z_{1} - z_{2})^{N}$ expanded in $z_{1}$ : the sign from $(- z_{0})^{- N}$ cancels the sign in $(z_{2} - z_{1})^{N}$ . These are the same polynomial, so their difference is zero. The right side has only nonnegative powers of $z_{0}$ .

2.1F1step 1.1algebra∎

Fix $j \geq 0$ . The coefficient of $z_{0}^{j}$ in the first term is $\sum_{k \geq 0} (\binom{j + k}{j}) z_{1}^{- j - 1 - k} z_{2}^{k}$ . The coefficient in the second delta term before its outer minus is $(- 1)^{j + 1} \sum_{k \geq 0} (\binom{j + k}{j}) z_{1}^{k} z_{2}^{- j - 1 - k}$ , by expanding $(z_{2} - z_{1})^{- j - 1}$ in nonnegative powers of $z_{1}$ . Thus the left-side coefficient is the sum of the first series and $(- 1)^{j}$ times $\sum_{k \geq 0} (\binom{j + k}{j}) z_{1}^{k} z_{2}^{- j - 1 - k}$ . On the right, the coefficient is $(- 1)^{j} \sum_{n \in Z} (\binom{n}{j}) z_{1}^{n - j} z_{2}^{- n - 1}$ . Splitting at $n = j$ , using $n = - 1 - k$ for the negative indices and $(\binom{- 1 - k}{j}) = (- 1)^{j} (\binom{j + k}{j})$ , gives exactly the same two series. Coefficients of every integer power of $z_{0}$ agree, proving the identity.

Depends on

Formal distributions and fields on a vector space

Used by

Dependency tree · two levels

2 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

Christophe Nozaradan, Introduction to Vertex Algebras, §§1.3–1.4 (standard reference, not scraped)
Yi-Zhi Huang, James Lepowsky, and Lin Zhang, Logarithmic Tensor Category Theory for Generalized Modules for a Conformal Vertex Algebra, I, equation (2.37) (standard reference, not scraped)