Homogeneous slice quotient compatibility
Abstract
Arbitrary-cutoff homogeneous Laurent quotients for the actual nested-Q distribution.
Theorem 1.1 (The supplied numerator and the locality supplier define the same rational slice).
Lean statement: D5/S3/VertexAlgebra/NestedResidues/LatticeHalfFockSliceQuotient.actual_slice_quotient_compat
Proof. Machine-checked in Lean as D5/S3/VertexAlgebra/NestedResidues/LatticeHalfFockSliceQuotient.actual_slice_quotient_compat (✓ 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.
The lawful WeightedLocalCorrelator.common_cleared_fields supplies the actual common array. Finite homogeneous carrier slicing, the left and swapped J/B supplier, and the original attributed signed Laurent collision form the Laurent-carrier, supported-readout and weighted-extraction stages of this quotient. Their original computations supply the full result. For the exact actual JAB distribution and the full coefficient telescope, let P and P₀ be finite Laurent polynomials at arbitrary natural cutoffs K and K₀. Their signed total degrees are L+M+K-d-r-n-3 and L+M+K₀-d-r-n-3. Neither cutoff is required to be a source/source locality witness. With C=v-z and T=max K K₀, the theorem proves C^(T-K) P=C^(T-K₀) P₀, and equality of P/Q_K and P₀/Q_K₀ in the common rational field.
Multiplication by a labelled difference translates a scalar homogeneous slice by exactly one degree. Iterating this finite coefficient identity, and composing the polynomial actions on the same actual distribution, puts both numerators on the identical degree slice at T. The three labelled differences are nonzero, so the common denominator is nonzero. All global Laurent exponents remain signed; negative total degree, zero numerators, and K=0 remain in scope. No support assertion is imposed on the whole distribution.
The comparison is consumed in the same theorem by the actual complete left and swapped current/second-source local readouts. The actual supplier’s quotient is transported to the supplied P/Q_K, retaining arbitrary output mode, input tensor, linear functional, signed indices, and independent outer cutoffs. The supplied complete-field locality laws also transport their complete outer-residue support and cutoff-padding statements. These are statements about complete two-order residues.
Classical provenance is Matsuo–Nagatomo and Bakalov–Kac (math/0402315); mathlib Hahn/Laurent series and partial fractions and Scott Carnahan/vertexAlg composition retain their Apache 2.0 attribution in the source. The faithful Reg source reconstruction is attempted; whole-family variation, sensitivity, observational dependence and lawful sourceSelection/escapeFrom/enrolled-template evidence remain incomplete. Joint finite Taylor support and the final actual Taylor identifications are further obligations. In the swapped branch, the expected joint support is alpha+a+k=M-j-1 and alpha+a+beta+b=degree; establishing that support and its local coefficient map is necessary before the final Taylor convolution. In the forward branch, the complete inner A/B rational residue and its pole bound L+M+(K-r-j-1).toNat remain necessary. The quotient comparison alone proves none of the three final Taylor identifications.