Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Signed coefficient readout

Abstract

Signed coefficient readout

Theorem 1.1 (polynomialAction_map).

Lean statement: D5/S3/VertexAlgebra/FormalSeries/UngradedLocalWordSeries.polynomialAction_map

Proof. Machine-checked in Lean as D5/S3/VertexAlgebra/FormalSeries/UngradedLocalWordSeries.polynomialAction_map (✓ std3). ∎

Source. Repository-derived.

Commentary.

Finite Laurent convolution commutes with a complex-linear readout.

Theorem 1.2 (signedExtend_map).

Lean statement: D5/S3/VertexAlgebra/FormalSeries/UngradedLocalWordSeries.signedExtend_map

Proof. Machine-checked in Lean as D5/S3/VertexAlgebra/FormalSeries/UngradedLocalWordSeries.signedExtend_map (✓ std3). ∎

Source. Repository-derived.

Commentary.

Signed zero extension commutes with complex-linear maps.

Theorem 1.3 (ungraded_local_word_common_series).

Lean statement: D5/S3/VertexAlgebra/FormalSeries/UngradedLocalWordSeries.ungraded_local_word_common_series

Proof. Machine-checked in Lean as D5/S3/VertexAlgebra/FormalSeries/UngradedLocalWordSeries.ungraded_local_word_common_series (✓ std3). ∎

Source. Repository-derived.

Commentary.

A finite complete word of mutually local fields has one generally infinite vector series after pair clearing and statewise monomial shifting. Its locality order is chosen before the input vector. The existing weighted-locality theorem supplies permutation equality and coordinate lower support.

Definition 1.4 (signedIndex).

Lean statement: D5/S3/VertexAlgebra/FormalSeries/UngradedLocalWordSeries.signedIndex

Formalization. D5/S3/VertexAlgebra/FormalSeries/UngradedLocalWordSeries.signedIndex (✓ std3).

Source. Repository-derived.

Commentary.

Convert each nonnegative signed exponent to a native finitely supported multi-index. This index imposes no finite support on a series.

Definition 1.5 (signedExtend).

Lean statement: D5/S3/VertexAlgebra/FormalSeries/UngradedLocalWordSeries.signedExtend

Formalization. D5/S3/VertexAlgebra/FormalSeries/UngradedLocalWordSeries.signedExtend (✓ std3).

Source. Repository-derived.

Commentary.

Extend the native coefficient function by zero whenever any signed exponent is negative.

References