ThreeFieldPolynomialCovariance
Abstract
ThreeFieldPolynomialCovariance
Theorem 1.1 (finite_inner_recoupling).
Lean statement: D5/S3/VertexAlgebra/FormalSeries/ThreeFieldPolynomialCovariance.finite_inner_recoupling
Proof. Machine-checked in Lean as D5/S3/VertexAlgebra/FormalSeries/ThreeFieldPolynomialCovariance.finite_inner_recoupling (✓ std3). ∎
Source. Repository-derived.
Commentary.
Finite polynomial expansion regroups the original cleared inner channel into fixed middle-mode product slices without an infinite interchange.