Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Native Gaussian finite coordinate cutoffs

Abstract

Whole occupation and genuine two-sided operator cutoffs for the native Gaussian data.

The inputs are the existing InfiniteGaussianFock.Data A and B on an arbitrary coordinate type I with decidable equality. No nonempty or finite dimensional hypothesis is imposed. In particular the results apply to every countable I, including the empty type. The actual bounded complex linear operators have transpose symmetric coordinate kernels, strict norm bounds qA and qB, and unconditionally summable double matrix squares. No cutoff limit, finite vacuum identity or determinant formula is stored as input.

Theorem 1.1 (Absolute native bilinear summability).

Lean statement: D5/S3/VertexAlgebra/TwistedGround/CountableGaussianCutoff.occupation_norm_summable

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

Source. Repository-derived.

Commentary.

The summand is h(d)=weight(d)*coefficient(A.kernel,d)*coefficient(B.kernel,d), with the native factorial weight and holomorphic coefficients. Weighted square summability of each native coefficient family gives absolute summability: twice the norm of each bilinear term is at most the sum of its two weighted squares. This is the elementary quadratic form of the Cauchy-Schwarz summability argument and uses no particle cutoff.

Theorem 1.2 (Whole support restriction converges).

Lean statement: D5/S3/VertexAlgebra/TwistedGround/CountableGaussianCutoff.occupationCutoff_tendsto

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

Source. Repository-derived.

Commentary.

For every finite coordinate F the cutoff is the infinite tsum of h over occupations whose entire support is contained in F. Tannery’s theorem applies with the summable norm bound. Each occupation is eventually retained; the native commonBlock constructor supplies its containing coordinate block. In the finite-tail argument underlying Tannery, one finite union of the supports of the finite occupation tail family contains all of them simultaneously. Finite F does not imply finitely many occupations. No degree or particle cutoff is introduced.

Theorem 1.3 (Both coordinate tails).

Lean statement: D5/S3/VertexAlgebra/TwistedGround/CountableGaussianCutoff.matrixTailSquare_tendsto

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

Source. Repository-derived.

Commentary.

The tail square is the unconditional sum over I times I of norm(K(i,j)) squared when either coordinate is outside F, and zero otherwise. It tends to zero atTop on Finset I. The summable full double-square series dominates it, and retaining both coordinates of each pair makes that pair vanish eventually. Thus a finite double-index tail is controlled by the union of both coordinate projections, without choosing an enumeration of I.

Theorem 1.4 (Actual HS error).

Lean statement: D5/S3/VertexAlgebra/TwistedGround/CountableGaussianCutoff.hs_compression_error

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

Source. Repository-derived.

Commentary.

Let JF be the existing finite ON inclusion, PF=JF JF adjoint, and AF=PF A PF. The projection acts by keeping precisely the F coordinates. The actual coordinate matrix of A-AF equals the original matrix outside F times F and is zero inside. Parseval and unconditional nonnegative double sums identify its HS square with matrixTailSquare. The existing setBasis construction is exposed for reuse, rather than duplicated; it transports the coordinate Hilbert basis to the set-indexed basis required by the Physlib HS suppliers.

Theorem 1.5 (Vanishing HS compression error).

Lean statement: D5/S3/VertexAlgebra/TwistedGround/CountableGaussianCutoff.hs_compression_tendsto

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

Source. Repository-derived.

Commentary.

For every native datum D, hsSize(D.oneParticle-compressed(D,F)) tends to zero along all finite coordinate sets atTop, since it equals the square root of the proved double-square tail. The square root is continuous at zero. No positivity, normalization or trace-one condition is needed.

Theorem 1.6 (Separate compression of both factors).

Lean statement: D5/S3/VertexAlgebra/TwistedGround/CountableGaussianCutoff.product_error_le

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

Source. Repository-derived.

Commentary.

The genuine trace-class carriers are T=AB and TF=(PF A PF)(PF B PF). The exact noncommuting difference is (A-AF)B+AF(B-BF). The attributed Physlib HS product trace-norm bound, applied in the real coordinate basis, gives norm(T-TF) at most deltaF=aTail(F)b+abTail(F), where a and b are the actual matrix HS sizes. Two-sided compression decreases the HS size. PF AB PF is not substituted for TF.

Theorem 1.7 (Trace-norm convergence).

Lean statement: D5/S3/VertexAlgebra/TwistedGround/CountableGaussianCutoff.cutoffProduct_tendsto

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

Source. Repository-derived.

Commentary.

The preceding explicit bound and the two HS tails prove TF tends to T in the existing TraceClass norm. This is actual trace-norm convergence of separately compressed products, with no commutativity or positivity assumption.

Theorem 1.8 (The original trace series is the limit).

Lean statement: D5/S3/VertexAlgebra/TwistedGround/CountableGaussianCutoff.traceLog_cutoff_tendsto

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

Source. Repository-derived.

Commentary.

The operator norms of T and every TF are bounded by q=qAqB<1. TraceClassPowerSeries supplies absolute convergence of the genuine positive-power trace series L and LF, the noncommuting power-trace bound (m+1)q^mnorm(T-TF), and norm(L-LF)<=deltaF/(2(1-q)). Hence LF tends to L. The indexing starts at power m+1 and divides by m+1; q is never divided out. The zero contraction and empty mode cases remain in scope.

Theorem 1.9 (Finite block trace equals compressed operator trace).

Lean statement: D5/S3/VertexAlgebra/TwistedGround/CountableGaussianCutoff.cutoff_power_trace

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

Source. Repository-derived.

Commentary.

For every finite F and every natural m, the genuine trace of TF^(m+1) equals Matrix.trace((A.block(F)*B.block(F))^(m+1)). The actual finite inclusion and its adjoint embed matrix multiplication, since JF adjoint JF is the identity even on the empty space. Positive powers of the compressed product are the corresponding embeddings. The unconditional full-space trace has zero diagonal outside F and exactly the finite matrix diagonal inside F.

Theorem 1.10 (Joint analytical bridge for the same native data).

Lean statement: D5/S3/VertexAlgebra/TwistedGround/CountableGaussianCutoff.native_cutoff_bridge

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

Source. Repository-derived.

Commentary.

For the same A and B, the theorem retains every analytical conclusion together: absolute bilinear occupation summability; whole support cutoff convergence; vanishing actual HS errors for each factor; the explicit deltaF product error and trace-norm convergence; absolute summability of the original and every compressed logarithmic trace series; the bound (m+1)q^mdeltaF for every power-trace difference; the logarithmic error deltaF/(2*(1-q)); convergence of the logarithmic traces; equality of each compressed positive-power trace with the actual finite block matrix trace; and equality of each whole support cutoff with the infinite occupation sum of the native finite principal Gaussian coefficients. The last identification uses the actual restriction/zero-extension equivalence on occupations, coefficient_on_block and weight_restrict. All cutoffs range over Finset I atTop, and all powers range over natural m with actual exponent m+1. This joint conclusion consumes the auxiliary cutoff statements on live proof paths. It has no finite Gaussian identity hypothesis and asserts no vacuum sewing equality.

The trace-class HS, ideal norm and trace suppliers retain Tom Ole Diem’s Physlib provenance at the pinned revision recorded in their source files. The present deductions use the repository’s native coefficients and actual one-particle operators. No literature novelty is claimed. These cutoff results alone do not establish the finite squeezed-vacuum formula or the full countable squeezed-vacuum identity. The finite identity is an external pending supplier. No full VOA, conformal field theory, string theory or AdS/CFT completion follows. Faithful dependent-family four-slot registration remains unfinished under issues 24524 and 24498; no declared_validated registration is asserted.

References