FourFieldMiddleInverseCoefficients

Abstract

FourFieldMiddleInverseCoefficients

Theorem 1.1 (Native derivation of the finite readout).

Lean statement: D5/S3/VertexAlgebra/FormalSeries/FourFieldMiddleInverseCoefficients.raw_middle_coefficients

Proof. Machine-checked in Lean as D5/S3/VertexAlgebra/FormalSeries/FourFieldMiddleInverseCoefficients.raw_middle_coefficients (✓ std3). ∎

Source. Repository-derived.

Commentary.

The three-index N3 balanced inverse is composed with the four outer binomial indices. Native finite coefficient convolutions prove the exact seven-index formula, shifts and signs. Wrong cumulative indices and negative original numerator inputs contribute zero.

References

• Truth anchor: D5/S3/VertexAlgebra/FormalSeries/FourFieldMiddleInverseCoefficients.raw_middle_coefficients
• Dependency: D5/S3/VertexAlgebra/FormalSeries/FourFieldMiddleInverseKernel