Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

ActualReadout

Abstract

Actual complete nested-field extraction and independent outer completion

The original six-word actual homogeneous coefficient equation, at every signed exponent, is transported using the canonical arbitrary-cutoff quotient. The supplied numerator P and cutoff K remain arbitrary. The actual nested extraction retains its entire original conjunction, including an independent inner extraction cutoff I.

Genuine locality of the actual complete intermediate field at each supplied H(j) gives complete outer-residue completion. The finite joint antidiagonal calculation keeps both the completion and the full reindexed weighted-residue conclusion. No local cutoff at the supplied K is imposed. The actual_ab_nested_readout helper is an internal consumed helper used by actual_ab_binary_taylor and actual_ab_joint_outer_support.

Theorem 1.1 (actual_ab_nested_readout).

Lean statement: D5/S3/VertexAlgebra/NestedResidues/LatticeHalfFockABOuterTaylor/ActualReadout.actual_ab_nested_readout

Proof. Machine-checked in Lean as D5/S3/VertexAlgebra/NestedResidues/LatticeHalfFockABOuterTaylor/ActualReadout.actual_ab_nested_readout (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Bojko Bakalov and Victor G. Kac (2004). Twisted Modules over Lattice Vertex Algebras. DOI: 10.1142/9789812702562_0001. URL: https://arxiv.org/abs/math/0402315v1.

Commentary.

Consumed original boundary helper for forward_weighted_identity. The source telescope and complete conclusion are retained.

Theorem 1.2 (actual_ab_joint_outer_support).

Lean statement: D5/S3/VertexAlgebra/NestedResidues/LatticeHalfFockABOuterTaylor/ActualReadout.actual_ab_joint_outer_support

Proof. Machine-checked in Lean as D5/S3/VertexAlgebra/NestedResidues/LatticeHalfFockABOuterTaylor/ActualReadout.actual_ab_joint_outer_support (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Bojko Bakalov and Victor G. Kac (2004). Twisted Modules over Lattice Vertex Algebras. DOI: 10.1142/9789812702562_0001. URL: https://arxiv.org/abs/math/0402315v1.

Commentary.

Consumed original boundary helper for forward_weighted_identity. The source telescope and complete conclusion are retained.

References