Critical Damping Partition

Abstract

A finite reflection-symmetric damping spectrum has equivalent diagonal, centered-exponential, and hyperbolic-cosine partition traces, with a nonnegative defect that vanishes precisely on the critical line.

Theorem 1.1 (The centered damping partition has a nonnegative critical defect).

$$\begin{array}{c}\forall d,tau:\mathrm{CenteredSpectrumSymmetric}(d,\frac{1}{2})\wedge tau\ne 0\Rightarrow \\ \mathrm{dampingPartition}(d,tau)=\exp (\frac{tau}{2})\cdot \mathrm{tr}(\exp ,(,(-tau),,\cdot ,,\mathrm{dampingOperator}(d),))\wedge \\ \mathrm{dampingPartition}(d,tau)=\mathrm{tr}(\exp ,(,(-tau),,\cdot ,,\mathrm{centeredDampingOperator}(d,\frac{1}{2}),))\wedge \mathrm{dampingPartition}(d,tau)=\mathrm{tr}(\cosh (tau\cdot \mathrm{centeredDampingOperator}(d,\frac{1}{2})))\wedge \\ 0\le \mathrm{criticalDampingPartitionDefect}(d,tau)\wedge ((\forall i,d_i=\frac{1}{2})⟺\mathrm{criticalDampingPartitionDefect}(d,tau)=0).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Weil/ZetaLinear/CriticalDampingPartition.critical_damping_partition_certificate (✓ std3). ∎

Source. Repository-derived.

Commentary.

A finite family of real damping rates defines a complex diagonal matrix. Subtracting one half times the identity produces the centered damping operator, while the normalized partition function is the exponential prefactor times the finite heat sum.

The reflection hypothesis is witnessed by a permutation that negates every centered rate. It cancels the odd exponential contribution and identifies the partition with the trace of the matrix hyperbolic cosine.

The resulting partition defect is a finite sum of cosh(x)-1 terms and is nonnegative. At every nonzero scale it vanishes exactly when all damping rates equal one half. The same module proves the finite maximum norm formula and explicit critical and off-line three-point witnesses.

References

• Truth anchor: D5/S3/Weil/ZetaLinear/CriticalDampingPartition.critical_damping_partition_certificate
• Dependency: D5/S3/Zeros/Symmetry/CriticalDampingFlatness