The exact finite numerator formula
Abstract
The exact finite numerator formula
Theorem 1.1 (The exact finite numerator formula).
Lean statement: D5/S3/VertexAlgebra/FormalSeries/ThreeFieldBalancedInverseCoefficients.raw_balanced_coefficients
Proof. Machine-checked in Lean as D5/S3/VertexAlgebra/FormalSeries/ThreeFieldBalancedInverseCoefficients.raw_balanced_coefficients (✓ std3). ∎
Source. Repository-derived.
Commentary.
The signed native inverse equals the finite sum over the balanced numerator fiber with input (s+k-r-l,x+a0+a1+2k+r+j+l,z+a2-j). The finite convolution is reindexed by u=r+l and v=r+j+l after their cumulative guards are established. Signed outside-cone targets and unsorted numerator indices give zero without additional positivity assumptions.