Finite numerator reconstruction of the inner inverse
Abstract
Finite numerator reconstruction of the inner inverse
Theorem 1.1 (Exact three-index numerator formula).
Lean statement: D5/S3/VertexAlgebra/FormalSeries/ThreeFieldInnerInverseCoefficients.raw_inner_coefficients
Proof. Machine-checked in Lean as D5/S3/VertexAlgebra/FormalSeries/ThreeFieldInnerInverseCoefficients.raw_inner_coefficients (✓ std3). ∎
Source. Repository-derived.
Commentary.
Every signed native inverse coefficient equals the sum of innerWeight times the original signed numerator coefficient over innerFiber. The finite antidiagonal convolution is reindexed by u=r+l and v=r+j only under both cumulative guards. The native numerator chart then supplies all three original exponent constraints, including negative and unsorted branches. No infinite sums are rearranged and the numerator may be infinite.