Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Original Gaussian Bilinear Trace Exchange

Abstract

Original Gaussian Bilinear Trace Exchange

The literal finite matrix moment equals its unconjugated contraction on the original infinite l2 carrier. Absolutely convergent odd-power series give the difference of the genuine signed inverses. Uniform control of the weighted source and both inverses yields compact-uniform scalar derivative convergence and differentiates the actual infinite cutoff limit. The current operator differentiation owner supplies the negative weighted scalar, and the weighted resolvent owner supplies the positive scalar; together they give the radial logarithmic derivative in terms of the existing period F.

These are analytic identities for the original coefficient model on its infinite carrier. Physical vertex operator algebras, conformal field theory, anomaly and fusion structures, string theory and AdS/CFT realization remain open.

Theorem 1.1 (finiteTraceMoment_eq_actual_cutoff_bilinear).

Lean statement: D5/S3/VertexAlgebra/TwistedGround/OriginalGaussianTraceBilinear.finiteTraceMoment_eq_actual_cutoff_bilinear

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

Source. Repository-derived.

Commentary.

For every N, every natural power including zero and every real parameter, the finite matrix moment equals its literal unconjugated l2 cutoff contraction.

Theorem 1.2 (actual_odd_moment_series_eq_signed_inverse_difference).

Lean statement: D5/S3/VertexAlgebra/TwistedGround/OriginalGaussianTraceBilinear.actual_odd_moment_series_eq_signed_inverse_difference

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

Source. Repository-derived.

Commentary.

For interior radial parameters, the odd scalar series and both signed inverse contractions converge absolutely, and the odd sum equals one half of the difference of the two actual inverse contractions.

Theorem 1.3 (compact_uniform_scalar_derivatives_and_final_exchange).

Lean statement: D5/S3/VertexAlgebra/TwistedGround/OriginalGaussianTraceBilinear.compact_uniform_scalar_derivatives_and_final_exchange

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

Source. Repository-derived.

Commentary.

On each interior open radial interval with enclosing radius below one, the finite logarithm derivatives converge uniformly to the two actual bilinear inverse contractions, and their limit differentiates the infinite logarithm.

Theorem 1.4 (gaussianLogDet_hasDerivAt_bilinear_resolvent).

Lean statement: D5/S3/VertexAlgebra/TwistedGround/OriginalGaussianTraceBilinear.gaussianLogDet_hasDerivAt_bilinear_resolvent

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

Source. Repository-derived.

Commentary.

For every real r strictly between zero and one, the actual infinite logarithm at sqrt r has derivative minus one over two r times the difference of the two unconjugated weighted inverse scalars.

Theorem 1.5 (gaussianLogDet_hasDerivAt_period).

Lean statement: D5/S3/VertexAlgebra/TwistedGround/OriginalGaussianTraceBilinear.gaussianLogDet_hasDerivAt_period

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

Source. Repository-derived.

Commentary.

For every real r strictly between zero and one, the derivative of the original infinite logarithm at sqrt r equals deriv F r divided by F r minus one over four times one minus r, embedded into the complex numbers.

References