Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

LatticeSectorSameRLeftCovariance

Abstract

LatticeSectorSameRLeftCovariance

Definition 1.1 (middlePolynomial).

Lean statement: D5/S3/VertexAlgebra/Sectors/LatticeSectorSameRLeftCovariance.middlePolynomial

Formalization. D5/S3/VertexAlgebra/Sectors/LatticeSectorSameRLeftCovariance.middlePolynomial (✓ std3).

Source. Repository-derived.

Commentary.

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

Definition 1.2 (finalPolynomial).

Lean statement: D5/S3/VertexAlgebra/Sectors/LatticeSectorSameRLeftCovariance.finalPolynomial

Formalization. D5/S3/VertexAlgebra/Sectors/LatticeSectorSameRLeftCovariance.finalPolynomial (✓ std3).

Source. Repository-derived.

Commentary.

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

Theorem 1.3 (actual_three_field_same_R_left_covariance).

Lean statement: D5/S3/VertexAlgebra/Sectors/LatticeSectorSameRLeftCovariance.actual_three_field_same_R_left_covariance

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

Source. Repository-derived.

Commentary.

The original all-integer Borcherds identity and common-middle equality give the finite action of the literal final polynomial on the actual left-nested channel. Actual original-state truncation removes the temporary extra multiplier, retaining the original k, a, P and six signed laws.

References