LatticeSectorMiddleCommonNumerator

Abstract

LatticeSectorMiddleCommonNumerator

Definition 1.1 (crossProductSlice).

Lean statement: D5/S3/VertexAlgebra/Sectors/LatticeSectorMiddleCommonNumerator.crossProductSlice

Formalization. D5/S3/VertexAlgebra/Sectors/LatticeSectorMiddleCommonNumerator.crossProductSlice (✓ std3).

Source. Repository-derived.

Commentary.

The crossProductSlice coefficient construction uses the displayed signed indices and finite polynomial fibers, with exactly the assumptions of its Lean statement.

Theorem 1.2 (actual_three_field_middle_common_numerator).

Lean statement: D5/S3/VertexAlgebra/Sectors/LatticeSectorMiddleCommonNumerator.actual_three_field_middle_common_numerator

Proof. Machine-checked in Lean as D5/S3/VertexAlgebra/Sectors/LatticeSectorMiddleCommonNumerator.actual_three_field_middle_common_numerator (✓ std3). ∎

Source. Repository-derived.

Commentary.

Finite recoupling and the actual Borcherds residue identify the cleared middle channel with the middle substitution of the original common numerator at every signed exponent.

References

• Truth anchor: D5/S3/VertexAlgebra/Sectors/LatticeSectorMiddleCommonNumerator.actual_three_field_middle_common_numerator
• Truth anchor: D5/S3/VertexAlgebra/Sectors/LatticeSectorMiddleCommonNumerator.crossProductSlice
• Dependency: D5/S3/VertexAlgebra/FormalSeries/SupportedMiddleCollision
• Dependency: D5/S3/VertexAlgebra/FormalSeries/ThreeFieldPolynomialCovariance
• Dependency: D5/S3/VertexAlgebra/Sectors/LatticeSectorSecondCollisionSlice