Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

LatticeSectorThreeFieldInnerIterate

Abstract

LatticeSectorThreeFieldInnerIterate

Definition 1.1 (innerIterate).

Lean statement: D5/S3/VertexAlgebra/Sectors/LatticeSectorThreeFieldInnerIterate.innerIterate

Formalization. D5/S3/VertexAlgebra/Sectors/LatticeSectorThreeFieldInnerIterate.innerIterate (✓ std3).

Source. Repository-derived.

Commentary.

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

Definition 1.2 (clearedInnerIterate).

Lean statement: D5/S3/VertexAlgebra/Sectors/LatticeSectorThreeFieldInnerIterate.clearedInnerIterate

Formalization. D5/S3/VertexAlgebra/Sectors/LatticeSectorThreeFieldInnerIterate.clearedInnerIterate (✓ std3).

Source. Repository-derived.

Commentary.

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

Theorem 1.3 (actual_three_field_inner_iterate_transport).

Lean statement: D5/S3/VertexAlgebra/Sectors/LatticeSectorThreeFieldInnerIterate.actual_three_field_inner_iterate_transport

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

Source. Repository-derived.

Commentary.

The original all-integer Borcherds identity identifies the actual cleared inner canonical iterate with the legal inner substitution of the same six-product numerator, preserving all original witnesses.

References