Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Physical Translation of Every Corrected Source

Abstract

Physical Translation of Every Corrected Source

Let D:LatticeData be arbitrary, hu:IsUnit D.G.det, source:Carrier D, e:Int and v:ActualTensor D hu. Carrier D consists of finite charge support with algebraic oscillator polynomial coefficients. ActualTensor D hu is the original dependent algebraic tensor module. All signed exponents, zero charges, repeated variables, inhomogeneous states, indefinite Gram data and degenerate fibres remain in scope.

Write A_i(F)=wordField D hu F [i] and S_s(F)=shiftField D hu s F. The physical derivative is a genuine Hahn field with coefficient ((e+2)/2) smul F.coeff(e+2). The existing joint pointwise finite support justifies every singleton mode sum. The jet recurrence (k+1)*jetScalar(k+1,m)=(-m-3/2-k)*jetScalar(k,m) gives the Leibniz identity Dphys(A_i F)=(k+1) smul A_successor(i)(F)+A_i(Dphys F). The split remains the original m<0 negative-left and m>=0 nonnegative-right split.

The Hahn shifts satisfy S_s S_t=S_(s+t) and commute with singleton insertion. Physical differentiation satisfies Dphys S_1=S_1 Dphys-S_2. These identities hold coefficientwise for every integer exponent without division by e+2.

Let Q be a polynomial in the option-indexed correction variables, with t=X none and x_i=X(some i). normalEvaluation E_q sends t multiplication to S_1 and x_i multiplication to A_i. It is a linear evaluator, not an algebra homomorphism. The polynomialField_X_mul theorem supplies the oscillator step through monomial occurrences and word permutation.

The oscillator connection sends t to -t^2 and x_i to (i.2+1) smul x_successor(i). Add multiplication by sum_colour q_colour*x_(colour,0) minus chargeNorm(q)/2 times t, obtaining L_q. The pair derivations in correctionConnection cancel the pair terms in the charge-weighted insertions. The sum of singleton corrections is -chargeNorm(q)/2 times t. Thus correctionConnection Q plus the charge-weighted insertions equals L_q Q.

MvPolynomial.induction_on proves E_q(L_q Q)=Dphys(E_q Q). Constants use the canonical all-ActualTensor charged_seed_physical_coefficient theorem. Addition uses linearity. Oscillator variables use the actual singleton Leibniz rule, and the shift variable uses Dphys S_1=S_1 Dphys-S_2. The public Corr_sectorTranslation contract then gives correctedPolynomial translation in every charge sector, without accessing its private correctedSource helpers. Finsupp.induction_linear over source charges yields the exact endpoint.

The jet, shift and evaluator calculation is adapted from the preserved OriginalTranslation source, SHA256 0442324ef84346403888d5faa093adffdd3ec23b77918c37b81252c5404b008a, and its declared TranslationCalculus supplier 8117eb5f8f5d301d5126a8d2fc054d22a1d7d2c314847a8b1699c89f5d123cd7. The charged ground and creation induction is reused from the canonical ChargedSeedPhysical owner. Classical sources are Frenkel-Lepowsky-Meurman (1988), Dong-Nagatomo math/9808088v1 section 3.2, and Bakalov-Kac math/0402315v1 section 4.4. Inherited half-Fock implementation copyright (c) 2025 Kalle Kytola; additional half-integer matrix implementation copyright (c) 2026; Apache 2.0. No mathematical novelty is asserted.

The result concerns every algebraic polynomial and tensor state; it does not construct a completion by infinite oscillator series. Twisted locality, Jacobi and Borcherds identities, full VOA and CFT constructions, anomaly and fusion structures, string dynamics, spacetime reconstruction and AdS/CFT remain further mathematical obligations.

Theorem 1.1 (The original normalized jet successor).

Lean statement: D5/S3/VertexAlgebra/LatticeHalfFockOriginalTranslation.jet_successor

Proof. Machine-checked in Lean as D5/S3/VertexAlgebra/LatticeHalfFockOriginalTranslation.jet_successor (✓ 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.

Visibility-only exposure of the existing jet successor, with its exact original statement and proof body preserved. ActualMobiusCovariance consumes it to derive the signed-mode Pascal step and L1 product rule; no copied jet recurrence or alternate jet representation is introduced.

Theorem 1.2 (The original empty-correction charged readout).

Lean statement: D5/S3/VertexAlgebra/LatticeHalfFockOriginalTranslation.corrected_singleton_coeff_charged

Proof. Machine-checked in Lean as D5/S3/VertexAlgebra/LatticeHalfFockOriginalTranslation.corrected_singleton_coeff_charged (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Igor B. Frenkel, James Lepowsky, and Arne Meurman (1988). Vertex Operator Algebras and the Monster. DOI: 10.1016/S0079-8169(08)X6136-7.

Commentary.

The existing exact statement and proof body are moved from the higher residue consumer to this common original corrected-field owner and made public. The old consumer uses the shared theorem. ActualMobiusCovariance consumes it in the charged source base. No duplicate supplier, copied correction proof or new covariance premise is introduced.

Theorem 1.3 (The exact canonical Hahn shift).

Lean statement: D5/S3/VertexAlgebra/LatticeHalfFockOriginalTranslation.shiftField_coefficient_public

Proof. Machine-checked in Lean as D5/S3/VertexAlgebra/LatticeHalfFockOriginalTranslation.shiftField_coefficient_public (✓ 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.

For every D:LatticeData, hu:IsUnit D.G.det, s:Nat, A:NativeField D hu and e:Int, (shiftField D hu s A).coeff e = A.coeff(e+2s), as endomorphisms of ActualTensor D hu. Hahn monomial multiplication by t^(-2s) changes the coordinate by exactly -2*s. Physical translation and full-source theta monodromy both use this same shift.

Theorem 1.4 (The exact all-source physical translation identity).

Lean statement: D5/S3/VertexAlgebra/LatticeHalfFockOriginalTranslation.correctedField_translation_physical

Proof. Machine-checked in Lean as D5/S3/VertexAlgebra/LatticeHalfFockOriginalTranslation.correctedField_translation_physical (✓ 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.

For every D:LatticeData, hu:IsUnit D.G.det, source:Carrier D, e:Int and v:ActualTensor D hu, (correctedField D hu (LatticeSugawaraConformal.translation D source)).coeff e v = (((e+2:Int):Complex)/2) smul (correctedField D hu source).coeff (e+2) v. The source translation is the actual Sugawara translation, the field is the native finite Corr-corrected Hahn field, and the target is the actual dependent tensor module. No derivative or seed law is assumed.

Theorem 1.5 (Negative current insertion on every source).

Lean statement: D5/S3/VertexAlgebra/LatticeHalfFockOriginalTranslation.correctedField_negative_current_insertion

Proof. Machine-checked in Lean as D5/S3/VertexAlgebra/LatticeHalfFockOriginalTranslation.correctedField_negative_current_insertion (✓ 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.

For arbitrary D, hu, index and b:Carrier D, set m=index.2+1 and N=vectorFrequencyBound D b+1. The corrected field of neutralMode index.1 (-m) b equals singletonLinear index applied to correctedField b, plus the finite sum for 0<=n<N of c(m,n) times shiftField (m+n) applied to correctedField(neutralMode index.1 n b), where c(m,n)=m*halfBinomial(m)*halfBinomial(n)/(m+n) in Complex. This is equality of whole NativeField values, at every signed exponent and every ActualTensor input. Source and target carriers remain distinct. Zero sources and empty rank fibres remain included; there is no charge, homogeneity, eigenstate, positivity, locality or module-law hypothesis.

The actual correctionLift_X_mul is evaluated by the existing Complex-linear normalEvaluation. Its none-variable power t^s evaluates to the true Hahn shift S_s, using shift_add; no multiplicative evaluator is assumed. For a fixed charge a and arbitrary polynomial p, the derivation on correctionLift p is expanded over its actual finite variable set, enlarged by the Option.some image of p.vars. Outside p.vars, correctionLift_partial and pderiv_eq_zero_of_notMem_vars remove terms. The resulting pair sum is over p.vars with the actual pderiv, retaining every repeated-variable multiplicity. Evaluation gives the singleton insertion, halfBinomial(m)*pairing(index,a) times S_m, and pairScalar(m,sourceWeight(u))*Gram(index,u) times S_(m+sourceWeight(u)) of each corrected partial.

Expand the actual b once over b.support. Two finite sup inequalities bound each supported source variable by B(b); pad the finite source derivative sum to colours times range B(b), and identify positive source mode n with n times the Gram-weighted derivative. The zero mode is handled separately: m>0 gives c(m,0)=halfBinomial(m), while nc(m,n)=pairScalar(m,n) for positive n. Signs are already contained in these scalars. The shift is m+n, so coefficient e is read at e+2(m+n). Only finite sums are newly exchanged; the established singletonLinear pointwise finiteness supplies the normal insertion. This prerequisite does not establish full finite residues, Ward identities or twisted Jacobi.

References