Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

SupportedMiddleCollision

Abstract

SupportedMiddleCollision

Definition 1.1 (middleNativeSlice).

Lean statement: D5/S3/VertexAlgebra/FormalSeries/SupportedMiddleCollision.middleNativeSlice

Formalization. D5/S3/VertexAlgebra/FormalSeries/SupportedMiddleCollision.middleNativeSlice (✓ std3).

Source. Repository-derived.

Commentary.

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

Definition 1.2 (outerArguments).

Lean statement: D5/S3/VertexAlgebra/FormalSeries/SupportedMiddleCollision.outerArguments

Formalization. D5/S3/VertexAlgebra/FormalSeries/SupportedMiddleCollision.outerArguments (✓ std3).

Source. Repository-derived.

Commentary.

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

Theorem 1.3 (middleNativeSlice_extend).

Lean statement: D5/S3/VertexAlgebra/FormalSeries/SupportedMiddleCollision.middleNativeSlice_extend

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

Source. Repository-derived.

Commentary.

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

Theorem 1.4 (outerCollision_signed).

Lean statement: D5/S3/VertexAlgebra/FormalSeries/SupportedMiddleCollision.outerCollision_signed

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

Source. Repository-derived.

Commentary.

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

Definition 1.5 (middleArguments).

Lean statement: D5/S3/VertexAlgebra/FormalSeries/SupportedMiddleCollision.middleArguments

Formalization. D5/S3/VertexAlgebra/FormalSeries/SupportedMiddleCollision.middleArguments (✓ std3).

Source. Repository-derived.

Commentary.

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

Theorem 1.6 (outer_inner_substitution).

Lean statement: D5/S3/VertexAlgebra/FormalSeries/SupportedMiddleCollision.outer_inner_substitution

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

Source. Repository-derived.

Commentary.

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

References