Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

LatticeHalfFockOuterTaylorEvaluation

Abstract

Current and first-source Laurent residue

Theorem 1.1 (local_laurent_pair_residue).

Lean statement: D5/S3/VertexAlgebra/NestedResidues/LatticeHalfFockOuterTaylorEvaluation.local_laurent_pair_residue

Proof. Machine-checked in Lean as D5/S3/VertexAlgebra/NestedResidues/LatticeHalfFockOuterTaylorEvaluation.local_laurent_pair_residue (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Bojko Bakalov and Victor G. Kac (2004). Twisted Modules over Lattice Vertex Algebras. DOI: 10.1142/9789812702562_0001. URL: https://arxiv.org/abs/math/0402315v1.

Commentary.

The current/source diagonal is taken before either remaining order. The signed monomial residue and the finite associated-coordinate contraction feed the exact fused FIRST proof. Negative degrees, empty supports and independent bounds remain included.

Theorem 1.2 (current_source_local_monomial).

Lean statement: D5/S3/VertexAlgebra/NestedResidues/LatticeHalfFockOuterTaylorEvaluation.current_source_local_monomial

Proof. Machine-checked in Lean as D5/S3/VertexAlgebra/NestedResidues/LatticeHalfFockOuterTaylorEvaluation.current_source_local_monomial (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Bojko Bakalov and Victor G. Kac (2004). Twisted Modules over Lattice Vertex Algebras. DOI: 10.1142/9789812702562_0001. URL: https://arxiv.org/abs/math/0402315v1.

Commentary.

The current/source diagonal is taken before either remaining order. The signed monomial residue and the finite associated-coordinate contraction feed the exact fused FIRST proof. Negative degrees, empty supports and independent bounds remain included.

Definition 1.3 (currentSourceMonomialValue).

Lean statement: D5/S3/VertexAlgebra/NestedResidues/LatticeHalfFockOuterTaylorEvaluation.currentSourceMonomialValue

Formalization. D5/S3/VertexAlgebra/NestedResidues/LatticeHalfFockOuterTaylorEvaluation.currentSourceMonomialValue (✓ std3).

Source. Repository-derived.

Acknowledgement. Bojko Bakalov and Victor G. Kac (2004). Twisted Modules over Lattice Vertex Algebras. DOI: 10.1142/9789812702562_0001. URL: https://arxiv.org/abs/math/0402315v1.

Commentary.

The current/source diagonal is taken before either remaining order. The signed monomial residue and the finite associated-coordinate contraction feed the exact fused FIRST proof. Negative degrees, empty supports and independent bounds remain included.

Theorem 1.4 (current_source_monomial_residue).

Lean statement: D5/S3/VertexAlgebra/NestedResidues/LatticeHalfFockOuterTaylorEvaluation.current_source_monomial_residue

Proof. Machine-checked in Lean as D5/S3/VertexAlgebra/NestedResidues/LatticeHalfFockOuterTaylorEvaluation.current_source_monomial_residue (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Bojko Bakalov and Victor G. Kac (2004). Twisted Modules over Lattice Vertex Algebras. DOI: 10.1142/9789812702562_0001. URL: https://arxiv.org/abs/math/0402315v1.

Commentary.

The current/source diagonal is taken before either remaining order. The signed monomial residue and the finite associated-coordinate contraction feed the exact fused FIRST proof. Negative degrees, empty supports and independent bounds remain included.

Theorem 1.5 (current_source_laurent_residue).

Lean statement: D5/S3/VertexAlgebra/NestedResidues/LatticeHalfFockOuterTaylorEvaluation.current_source_laurent_residue

Proof. Machine-checked in Lean as D5/S3/VertexAlgebra/NestedResidues/LatticeHalfFockOuterTaylorEvaluation.current_source_laurent_residue (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Bojko Bakalov and Victor G. Kac (2004). Twisted Modules over Lattice Vertex Algebras. DOI: 10.1142/9789812702562_0001. URL: https://arxiv.org/abs/math/0402315v1.

Commentary.

The current/source diagonal is taken before either remaining order. The signed monomial residue and the finite associated-coordinate contraction feed the exact fused FIRST proof. Negative degrees, empty supports and independent bounds remain included.

Theorem 1.6 (finite_rectangle_cut).

Lean statement: D5/S3/VertexAlgebra/NestedResidues/LatticeHalfFockOuterTaylorEvaluation.finite_rectangle_cut

Proof. Machine-checked in Lean as D5/S3/VertexAlgebra/NestedResidues/LatticeHalfFockOuterTaylorEvaluation.finite_rectangle_cut (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Bojko Bakalov and Victor G. Kac (2004). Twisted Modules over Lattice Vertex Algebras. DOI: 10.1142/9789812702562_0001. URL: https://arxiv.org/abs/math/0402315v1.

Commentary.

The same finite rectangle is summed along either natural bound, for an arbitrary complex sequence. The original associated contraction and forward Taylor convolution use this reindexing, including the zero bounds.

Theorem 1.7 (finite_associated_contraction).

Lean statement: D5/S3/VertexAlgebra/NestedResidues/LatticeHalfFockOuterTaylorEvaluation.finite_associated_contraction

Proof. Machine-checked in Lean as D5/S3/VertexAlgebra/NestedResidues/LatticeHalfFockOuterTaylorEvaluation.finite_associated_contraction (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Bojko Bakalov and Victor G. Kac (2004). Twisted Modules over Lattice Vertex Algebras. DOI: 10.1142/9789812702562_0001. URL: https://arxiv.org/abs/math/0402315v1.

Commentary.

The current/source diagonal is taken before either remaining order. The signed monomial residue and the finite associated-coordinate contraction feed the exact fused FIRST proof. Negative degrees, empty supports and independent bounds remain included.

Theorem 1.8 (finite_left_outer_taylor).

Lean statement: D5/S3/VertexAlgebra/NestedResidues/LatticeHalfFockOuterTaylorEvaluation.finite_left_outer_taylor

Proof. Machine-checked in Lean as D5/S3/VertexAlgebra/NestedResidues/LatticeHalfFockOuterTaylorEvaluation.finite_left_outer_taylor (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Bojko Bakalov and Victor G. Kac (2004). Twisted Modules over Lattice Vertex Algebras. DOI: 10.1142/9789812702562_0001. URL: https://arxiv.org/abs/math/0402315v1.

Commentary.

The current/source diagonal is taken before either remaining order. The signed monomial residue and the finite associated-coordinate contraction feed the exact fused FIRST proof. Negative degrees, empty supports and independent bounds remain included.

References