Actual raw balanced reconstruction
Abstract
Actual raw balanced reconstruction
Theorem 1.1 (Actual raw balanced reconstruction).
Lean statement: D5/S3/VertexAlgebra/Sectors/LatticeSectorRawBalancedCoefficients.actual_three_field_raw_balanced_coefficients
Proof. Machine-checked in Lean as D5/S3/VertexAlgebra/Sectors/LatticeSectorRawBalancedCoefficients.actual_three_field_raw_balanced_coefficients (✓ std3). ∎
Source. Repository-derived.
Commentary.
For arbitrary lattice data, charges and oscillator states, the same locality order k is chosen before the fourth charge and state. The same original bounds a and generally infinite P retain canonical truncation, all six signed product laws, inner cleared and action identities, the finite raw inner formula, actual balanced support and balanced clearing. The actual balanced channel is canonical of the first pair acting on the second pair, in tree ((uv)(tw)). Its coefficient equals the finite three-index formula for the same native numerator P(s+x,x,z). Uniform s support comes from truncation of u on v and uniform z support from truncation of t on w; both are uniform in x. Literal polynomial action is proved from the finite balanced clearing and then cancelled on this actual support. No finite numerator, x cutoff, domain, energy, positivity or charge restriction is required. Bakalov–Kac, Matsuo–Nagatomo and Carnahan supplier attributions and canonical normalization are preserved.