Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Actual signed finite Jacobi coefficient transport

Abstract

Actual signed finite Jacobi coefficient transport

All calculations retain the original lattice Carrier, actual twisted tensor carrier, actual source L1 and ordered selected actualForm. The twisted inputs are the negative parity space at rank twenty-four. Actual integer conformal weights start at two; this is used also for zero and weight-one transformed outputs.

The first ordered source product has the original b-mode on the right. On the required test grade E=H+K+d-m-n-r-2 its rightmost output weight is K+d-m-1-p-k. The second ordered product has the lowered original a-mode on the right, of output weight H+d-r-1-q-L-k. Thus p+k<=K+d-m-3 and q+L+k<=H+d-r-3 are actual nonzero-support conditions. These conditions precede every finite convolution.

Two applications of the supported signed Vandermonde identity use the finite maps (j,h) to (t=j+h,j), then (ell,t) to (k=ell+t,ell). Their inverse subtractions occur only under the relevant triangle inequalities. They give (-1)^k choose(B-r-L,k), including negative signed r and B. The factorial contraction uses the independent actual original-source nilpotence cutoff.

The source supplier is GroundRightCurrentTransport.FirstSourceClosure.first_eigen_arbitrary_second, applied to the actual lowered theta-fixed first source and arbitrary original second source. Its three finite support clauses and both ordered terms are retained. The calculations are repository derivations using existing actual covariance, lowering, source inversion and all-source compatibility. They do not assert identification of the fixed restricted dual with the original source, a positive or symmetric selected form, three-twisted crossing, or a complete VOA construction.

Theorem 1.1 (First-input triangle on the actual signed support).

Lean statement: D5/S3/VertexAlgebra/TwistedGround/MixedJacobiCoefficients.mixed_first_input_reindexed_pairing

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

Source. Repository-derived.

Commentary.

The signed output-energy alternative is consumed before padding. The map q_target=i+L+h has the inverse h=q_target-i-L on its finite triangle. The rightmost actual source mode has weight H+d-r-1-i-L-j-h, so integer weights below two make every padding term zero.

Theorem 1.2 (Both ordered actual source products after signed contraction).

Lean statement: D5/S3/VertexAlgebra/TwistedGround/MixedJacobiCoefficients.mixed_source_finite_cancellation

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

Source. Repository-derived.

Commentary.

The public first_eigen_arbitrary_second supplier is applied with the lowered fixed source, gamma=delta=0 and P=r, Q=2H-n-r-2+p-q, R=2d-L-m-r-2. The two finite signed convolutions retain both ordered products. This conclusion uses the actual three-supported source law, without a mixed-law premise.

Theorem 1.3 (Entire first-input branch at k_source=j+h).

Lean statement: D5/S3/VertexAlgebra/TwistedGround/MixedJacobiCoefficients.mixed_first_input_branch_reindexed

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

Source. Repository-derived.

Commentary.

Actual low-energy vanishing bounds the outer signed input action before the triangle is reindexed and the finite Vandermonde identity is applied. The second ordered source product retains the literal phase (-1)^(m+n+r+2-p-H-d+i+L).

Theorem 1.4 (Second-input triangle with total lowering L=ell+z).

Lean statement: D5/S3/VertexAlgebra/TwistedGround/MixedJacobiCoefficients.mixed_second_input_reindexed_pairing

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

Source. Repository-derived.

Commentary.

The map p_target=i+ell+h is evaluated after the signed-output split. Transposition retains both original actualForm slots and the original finite source sum. The target first ordered source product has L=ell+z, k_source=j+ell+h and rightmost output weight K+d-m-1-i-k_source.

Theorem 1.5 (Actual total-source factorial contraction).

Lean statement: D5/S3/VertexAlgebra/TwistedGround/MixedJacobiCoefficients.mixed_second_source_factorial_contraction

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

Source. Repository-derived.

Commentary.

Original source nilpotence bounds both lowering indices before reindexing ell,z by L=ell+z. The literal factor 1/(ell! z!) becomes choose(L,ell)/L! on the actual first ordered source product. Binomial parameters may be signed; they supply no support premise.

Theorem 1.6 (Actual integer-energy lower bound).

Lean statement: D5/S3/VertexAlgebra/TwistedGround/MixedJacobiCoefficients.integer_energy_zero

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

Source. Repository-derived.

Commentary.

The actualAmbientBasis spectrum at rank twenty-four rules out integer weights below two. The common-cube branch contraction and lowering bound consume this result; mixed_input_off_grade uses it for negative transformed input weights.

Theorem 1.7 (Integer energy after actual lowering).

Lean statement: D5/S3/VertexAlgebra/TwistedGround/MixedJacobiCoefficients.lowering_integer_energy

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

Source. Repository-derived.

Commentary.

The existing lowering eigenvalue is evaluated at rank twenty-four. lowering_integer_zero_after consumes the shifted energy to bound the actual input-lowering indices.

Theorem 1.8 (Integer energy of an original mode).

Lean statement: D5/S3/VertexAlgebra/TwistedGround/MixedJacobiCoefficients.original_mode_integer_energy

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

Source. Repository-derived.

Commentary.

Actual corrected-field covariance computes the energy w+d-t-1 without changing the original source or tensor carrier. The complete second-input branch consumes this support calculation.

Definition 1.9 (First ordered source product).

Lean statement: D5/S3/VertexAlgebra/TwistedGround/MixedJacobiCoefficients.mixedSourceFirst

Formalization. D5/S3/VertexAlgebra/TwistedGround/MixedJacobiCoefficients.mixedSourceFirst (✓ std3).

Source. Repository-derived.

Commentary.

This is the actualForm pairing with the lowered original a-mode outside the original b-mode. mixed_second_input_branch_contracted and the common-cube first sum use this same definition.

Definition 1.10 (Second ordered source product).

Lean statement: D5/S3/VertexAlgebra/TwistedGround/MixedJacobiCoefficients.mixedSourceSecond

Formalization. D5/S3/VertexAlgebra/TwistedGround/MixedJacobiCoefficients.mixedSourceSecond (✓ std3).

Source. Repository-derived.

Commentary.

This is the actualForm pairing with the original b-mode outside the lowered original a-mode. The common-cube second sum and first-input padding use this same definition.

Theorem 1.11 (Supported first signed contraction).

Lean statement: D5/S3/VertexAlgebra/TwistedGround/MixedJacobiCoefficients.mixed_first_contraction

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

Source. Repository-derived.

Commentary.

Actual low-energy vanishing supplies the zero tail before the finite signed convolution is contracted. mixed_iterate_cancellation consumes this contraction on the live path to the homogeneous identity.

Theorem 1.12 (Supported second signed contraction).

Lean statement: D5/S3/VertexAlgebra/TwistedGround/MixedJacobiCoefficients.mixed_second_contraction

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

Source. Repository-derived.

Commentary.

Two finite signed convolutions contract against the first ordered source product with its actual output-energy bound. The complete second-input branch and mixed_iterate_cancellation consume the result.

References