SupportedCollisionSlice
Abstract
SupportedCollisionSlice
Definition 1.1 (modeFiber).
Lean statement: D5/S3/VertexAlgebra/FormalSeries/SupportedCollisionSlice.modeFiber
Formalization. D5/S3/VertexAlgebra/FormalSeries/SupportedCollisionSlice.modeFiber (✓ std3).
Source. Repository-derived.
Commentary.
The fixed middle coefficient uses the exact integer interval of intermediate canonical modes.
Theorem 1.2 (mem_modeFiber_iff).
Lean statement: D5/S3/VertexAlgebra/FormalSeries/SupportedCollisionSlice.mem_modeFiber_iff
Proof. Machine-checked in Lean as D5/S3/VertexAlgebra/FormalSeries/SupportedCollisionSlice.mem_modeFiber_iff (✓ std3). ∎
Source. Repository-derived.
Commentary.
Membership in that mode interval is equivalent to indices in the two finite polynomial fibers.