Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Supported collision coefficients and reconstruction

Abstract

SupportedChannelSeries

Classical binomial-series algebra is applied to lower-supported vector coefficients. Mathlib supplies binomialSeries_add and native MvPowerSeries substitution. The finite diagonal arguments establish both the signed inverse expansion of (x-y)^N and the positive-factor inverse expansion of (y+t)^A. Native substitution has zero constant arguments; its antidiagonal coefficient fiber is finite even when the numerator has infinite support. Coefficient readouts are complex-linear and need not preserve multiplication.

Definition 1.1 (clear).

Lean statement: D5/S3/VertexAlgebra/FormalSeries/SupportedChannelSeries.clear

Formalization. D5/S3/VertexAlgebra/FormalSeries/SupportedChannelSeries.clear (✓ std3).

Source. Repository-derived.

Commentary.

The exact assumptions, coefficient conventions and quantifiers are given by the Lean telescope.

Definition 1.2 (powerIndex).

Lean statement: D5/S3/VertexAlgebra/FormalSeries/SupportedChannelSeries.powerIndex

Formalization. D5/S3/VertexAlgebra/FormalSeries/SupportedChannelSeries.powerIndex (✓ std3).

Source. Repository-derived.

Commentary.

The exact assumptions, coefficient conventions and quantifiers are given by the Lean telescope.

Definition 1.3 (extend).

Lean statement: D5/S3/VertexAlgebra/FormalSeries/SupportedChannelSeries.extend

Formalization. D5/S3/VertexAlgebra/FormalSeries/SupportedChannelSeries.extend (✓ std3).

Source. Repository-derived.

Commentary.

The exact assumptions, coefficient conventions and quantifiers are given by the Lean telescope.

Definition 1.4 (binomialTransform).

Lean statement: D5/S3/VertexAlgebra/FormalSeries/SupportedChannelSeries.binomialTransform

Formalization. D5/S3/VertexAlgebra/FormalSeries/SupportedChannelSeries.binomialTransform (✓ std3).

Source. Repository-derived.

Commentary.

The exact assumptions, coefficient conventions and quantifiers are given by the Lean telescope.

Theorem 1.5 (supported_reconstruction).

Lean statement: D5/S3/VertexAlgebra/FormalSeries/SupportedChannelSeries.supported_reconstruction

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

Source. Repository-derived.

Commentary.

The exact assumptions, coefficient conventions and quantifiers are given by the Lean telescope.

Definition 1.6 (collisionArguments).

Lean statement: D5/S3/VertexAlgebra/FormalSeries/SupportedChannelSeries.collisionArguments

Formalization. D5/S3/VertexAlgebra/FormalSeries/SupportedChannelSeries.collisionArguments (✓ std3).

Source. Repository-derived.

Commentary.

The exact assumptions, coefficient conventions and quantifiers are given by the Lean telescope.

Definition 1.7 (collision).

Lean statement: D5/S3/VertexAlgebra/FormalSeries/SupportedChannelSeries.collision

Formalization. D5/S3/VertexAlgebra/FormalSeries/SupportedChannelSeries.collision (✓ std3).

Source. Repository-derived.

Commentary.

The exact assumptions, coefficient conventions and quantifiers are given by the Lean telescope.

Theorem 1.8 (collision_coeff).

Lean statement: D5/S3/VertexAlgebra/FormalSeries/SupportedChannelSeries.collision_coeff

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

Source. Repository-derived.

Commentary.

The exact assumptions, coefficient conventions and quantifiers are given by the Lean telescope.

Theorem 1.9 (cleared_collision_coeff).

Lean statement: D5/S3/VertexAlgebra/FormalSeries/SupportedChannelSeries.cleared_collision_coeff

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

Source. Repository-derived.

Commentary.

The exact assumptions, coefficient conventions and quantifiers are given by the Lean telescope.

Definition 1.10 (mapSeries).

Lean statement: D5/S3/VertexAlgebra/FormalSeries/SupportedChannelSeries.mapSeries

Formalization. D5/S3/VertexAlgebra/FormalSeries/SupportedChannelSeries.mapSeries (✓ std3).

Source. Repository-derived.

Commentary.

The exact assumptions, coefficient conventions and quantifiers are given by the Lean telescope.

Theorem 1.11 (collision_map).

Lean statement: D5/S3/VertexAlgebra/FormalSeries/SupportedChannelSeries.collision_map

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

Source. Repository-derived.

Commentary.

The exact assumptions, coefficient conventions and quantifiers are given by the Lean telescope.

Definition 1.12 (positiveClear).

Lean statement: D5/S3/VertexAlgebra/FormalSeries/SupportedChannelSeries.positiveClear

Formalization. D5/S3/VertexAlgebra/FormalSeries/SupportedChannelSeries.positiveClear (✓ std3).

Source. Repository-derived.

Commentary.

The exact assumptions, coefficient conventions and quantifiers are given by the Lean telescope.

Theorem 1.13 (supported_positive_reconstruction).

Lean statement: D5/S3/VertexAlgebra/FormalSeries/SupportedChannelSeries.supported_positive_reconstruction

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

Source. Repository-derived.

Commentary.

The exact assumptions, coefficient conventions and quantifiers are given by the Lean telescope.

References