Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

LatticeSectorSecondCollisionSlice

Abstract

LatticeSectorSecondCollisionSlice

Definition 1.1 (middleIterate).

Lean statement: D5/S3/VertexAlgebra/Sectors/LatticeSectorSecondCollisionSlice.middleIterate

Formalization. D5/S3/VertexAlgebra/Sectors/LatticeSectorSecondCollisionSlice.middleIterate (✓ std3).

Source. Repository-derived.

Commentary.

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

Definition 1.2 (clearedMiddleSlice).

Lean statement: D5/S3/VertexAlgebra/Sectors/LatticeSectorSecondCollisionSlice.clearedMiddleSlice

Formalization. D5/S3/VertexAlgebra/Sectors/LatticeSectorSecondCollisionSlice.clearedMiddleSlice (✓ std3).

Source. Repository-derived.

Commentary.

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

Definition 1.3 (sliceResidueTerm).

Lean statement: D5/S3/VertexAlgebra/Sectors/LatticeSectorSecondCollisionSlice.sliceResidueTerm

Formalization. D5/S3/VertexAlgebra/Sectors/LatticeSectorSecondCollisionSlice.sliceResidueTerm (✓ std3).

Source. Repository-derived.

Commentary.

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

Theorem 1.4 (actual_collision_slice_finite_residue).

Lean statement: D5/S3/VertexAlgebra/Sectors/LatticeSectorSecondCollisionSlice.actual_collision_slice_finite_residue

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

Source. Repository-derived.

Commentary.

A maximum of actual outer-state truncation bounds over the finite intermediate-mode interval makes the middle Borcherds residue a finite sum. No cutoff over all descendants is used.

References