feat(M11.2): add infinite-mode Liouville soliton tensor

[jagg-ix]

M11.2

Builds the soliton density tensor

rho_ij = a_i conjugate(a_j)

from the M11.1 pointwise carrier in a centered Fourier-mode cutoff. The campaign verifies Hermiticity, trace one, rank-one purity, positive semidefiniteness, commuting pointwise left/right actions, fixed-particle-number bookkeeping and monotone retained probability as the mode cutoff grows.

Scope

The implementation is a finite-cutoff realization of an infinite mode set with fixed finite particle number. It does not claim a completed infinite-particle Fock Hilbert space.

Formal authority

Pins LiouvilleSecondQuantization.lean@9d2c905c..., including kernelMode_infinite, kernelOccupationBasis_particleNumber, leftPointwise_rightPointwise_commute and continuumKernelNormSq_nonneg.

[jagg-ix]

Validation complete on ce232fe1e9d72ef482e90405e2292e4a32e43309: workflow run 30516128537 passed compilation, formal-ledger validation and the M11 test suite. Merge after #151 using Create a merge commit.