Full source energy restricted dual of original coefficients

Abstract

The original correctedDualCoefficient D hu e x y is the functional a maps to actualForm D hu (A_e(a)x) y, with the unchanged chosen nonsymmetric form and ordered slots. Generic closure uses arbitrary LatticeData with unit Gram determinant; indefinite forms and infinitely many charges in a single energy grade remain in scope.

The original coefficient energy law puts A_e(a)x in signed odd index M+e+2h. The unchanged b076 actualForm_oddGrade_orthogonal theorem is directly used to prove exact selection: the coefficient vanishes unless e+2h=N-M. This helper is consumed on the live proof path to support, full-grade restrictions, reconstruction and truncation.

For arbitrary x and y, their actualAmbientBasis coordinates have finite supports. The finite cover is the set of (N-M-e)/2 for their supported signed odd energies M,N. Selection establishes exact even divisibility before division. Every vector of any excluded full source grade is annihilated.

EnergyRestrictedDual is the dependent direct sum over all integer h of the full algebraic dual of grade D h. Its coordinates are exactly restrictions of the original functional for every h. DFinsupp.mk uses the proved finite cover. DFinsupp.lsum and the existing carrierEnergyDecomposition reconstruct the same functional on every Carrier source. No finite-dimensional grade replacement is used.

Both ordered input linearities are proved from the original form and used in finite basis expansion and the bilinear lifted coefficient. Under positive Gram only, source energy is nonnegative. For reversed exponent r=-e a homogeneous coefficient vanishes below M-N, and an arbitrary full functional and its lift vanish below -maxOddWeight(y). Generic indefinite lower truncation is not claimed.

This is a raw algebraic energy-dual lift. In t squared equals z coordinates raw reversal has physical power h+(M-N)/2. A normalized intertwiner would require the additional input conformal-power shift; rank 24 vacuum raw power zero is not its physical power minus three. Normalization, phases, L1, translation, Jacobi, fusion, anomaly structures and the complete Monster/string/AdS-CFT programme remain open. No literature novelty is asserted.

The faithful mirrored Reg audit remains unfinished under the existing linked issue https://github.com/the-omega-institute/trureturing/issues/21259; kernel checking is separate from registration validation.

Theorem 1.1 (correctedDualCoefficient energy selection).

Lean statement: D5/S3/VertexAlgebra/TwistedGround/ActualEnergyRestrictedDual.correctedDualCoefficient_energy_selection

Proof. Machine-checked in Lean as D5/S3/VertexAlgebra/TwistedGround/ActualEnergyRestrictedDual.correctedDualCoefficient_energy_selection (✓ std3). ∎

Source. Repository-derived.

Commentary.

The exact compiled theorem telescope supplies all parameters, hypotheses and the stated equality or vanishing law.

Theorem 1.2 (correctedDualCoefficient off energy cover).

Lean statement: D5/S3/VertexAlgebra/TwistedGround/ActualEnergyRestrictedDual.correctedDualCoefficient_off_energy_cover

Proof. Machine-checked in Lean as D5/S3/VertexAlgebra/TwistedGround/ActualEnergyRestrictedDual.correctedDualCoefficient_off_energy_cover (✓ std3). ∎

Source. Repository-derived.

Commentary.

The exact compiled theorem telescope supplies all parameters, hypotheses and the stated equality or vanishing law.