Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

LatticeSectorThreeFieldCommonSeries

Abstract

LatticeSectorThreeFieldCommonSeries

Definition 1.1 (labelledFields).

Lean statement: D5/S3/VertexAlgebra/Sectors/LatticeSectorThreeFieldCommonSeries.labelledFields

Formalization. D5/S3/VertexAlgebra/Sectors/LatticeSectorThreeFieldCommonSeries.labelledFields (✓ std3).

Source. Repository-derived.

Commentary.

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

Definition 1.2 (nestedCanonical).

Lean statement: D5/S3/VertexAlgebra/Sectors/LatticeSectorThreeFieldCommonSeries.nestedCanonical

Formalization. D5/S3/VertexAlgebra/Sectors/LatticeSectorThreeFieldCommonSeries.nestedCanonical (✓ std3).

Source. Repository-derived.

Commentary.

The nestedCanonical 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_common_series).

Lean statement: D5/S3/VertexAlgebra/Sectors/LatticeSectorThreeFieldCommonSeries.actual_three_field_common_series

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

Source. Repository-derived.

Commentary.

For arbitrary even integral symmetric lattice data and arbitrary descendants, all six signed canonical products share the same generally infinite series. The pair locality order precedes the fourth charge and state; monomial bounds come from their actual truncation.

References