Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Full-space thermal Hamiltonians

Abstract

Continuous singular reference energy constructs one full-space all-temperature Hamiltonian.

Definition 1.1 (Finite levels on the complete spectral basis).

Formalization. D5/S3/Quantum/Analysis/TraceClass/ContinuousEnergyHamiltonian.thermalBaseLevel (✓ std3).

Source. Repository-derived.

Acknowledgement. M. E. Shirokov (2012). On a conjectured property of the von Neumann entropy valid in the commutative case. URL: https://arxiv.org/abs/1201.1093v1.

Commentary.

H is a complete complex Hilbert space, sigma is a positive trace-class contraction, and r is an actual full SpectralResolution of sigma. For an arbitrary code from r.index to the natural numbers, thermalBaseLevel(r,code,i) is (code(i)+1)*log(2) when r.values(i)=0 and -log(r.values(i)) otherwise. Every level is a finite real number. No basis vectors are removed and no unused natural coordinate becomes a physical mode.

Definition 1.2 (Joint conclusions for one literal operator).

Formalization. D5/S3/Quantum/Analysis/TraceClass/ContinuousEnergyHamiltonian.ThermalOn (✓ std3).

Source. Repository-derived.

Acknowledgement. M. E. Shirokov (2012). On a conjectured property of the von Neumann entropy valid in the commutative case. URL: https://arxiv.org/abs/1201.1093v1.

Commentary.

ThermalOn(b,h,A) abbreviates the following conjunction for the literal K=DiagonalHeat.hamiltonian(b,h) and the literal positive-time heat DiagonalHeat.heat(b,h,hh,t), with hh the proof that every h(i) is nonnegative. All real coefficients are at least one; for every real beta>0, exp(-beta*h(i)) is genuinely summable. K is self-adjoint and has dense domain in the entire H. Its graph is exactly the coefficient equation b.repr(y)(i)=h(i)*b.repr(x)(i), and its operator domain is exactly the weighted-l2 condition Memlp(i maps to h(i)b.repr(x)(i),2). The heat coefficients are exp(-th(i))*b.repr(x)(i), and the actual bounded heat operator is positive for every nonnegative time.

There is a strongly continuous contraction semigroup S equal to the real scalar restriction of this literal heat. For every x,v in H, its right difference quotient at zero tends to v if and only if (x,-v) belongs to K.graph. Any strongly continuous contraction semigroup with that same full generator graph equals S. For every x in the operator domain, norm(x)^2 is at most Re inner(x,K(x)). For every positive NNReal beta, the literal heat is trace class, and both its complex and real coefficient series have HasSum equal to its actual complex trace and real trace, respectively.

The mixed-state energy is exactly DiagonalEnergy.stateEnergy(b,h,hh,rho.1,TraceClass.isTraceClass_coe(rho)), defined by the actual bounded resolvent-cap traces. It is finite on A, and both this ENNReal-valued function and its real value are ContinuousOn A in trace norm. Operator domain, quadratic-form domain and mixed-state energy remain distinct. No unbounded product K*rho is formed; no trace-class assertion at beta=0 is made.

Theorem 1.3 (Thermal construction from continuous singular energy).

Proof. Machine-checked in Lean as D5/S3/Quantum/Analysis/TraceClass/ContinuousEnergyHamiltonian.exists_thermalHamiltonian_of_continuous_spectralEnergy (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. M. E. Shirokov (2012). On a conjectured property of the von Neumann entropy valid in the commutative case. URL: https://arxiv.org/abs/1201.1093v1.

Commentary.

H is complete and separable over the complex numbers. The actual positive trace-class contraction sigma additionally has actual real trace one; normalization is not a field of Reference. The supplied r is any complete full Set-index spectral resolution of sigma, including nativeResolution(sigma). A is a nonempty compact subset of the actual trace-class Banach space. Every rho in A is positive and has actual real trace one. The actual singular spectralEnergy(sigma,rho) is finite on A and its real value is continuous there. No convexity assumption is used. For every strictly positive NNReal delta, one injective code, one natural weight w, and one real h on the original index satisfy the displayed joint conclusion. The weight is at least one, monotone, and tends to infinity; h(i)=1+w(code(i))*thermalBaseLevel(r,code,i).

Separability and orthonormality make the full index countable. Only scalar energy terms are extended by zero along its injection into the natural numbers. Finite singular energy implies that each rho kills every zero-eigenvalue vector of sigma; those diagonal masses therefore vanish. Thus the actual energy is the sum of ofReal(a(i)*diagonal(b,rho,i)), with a=thermalBaseLevel. Actual normalization gives HasSum of the reference eigenvalues equal to one. The estimate exp(-a(i))<=s(i)+(1/2)^(code(i)+1) yields a summable majorant, including the full kernel.

First prove finiteness of the extended nonnegative energy series, then pass to its genuine real sum. The real finite prefixes are continuous and increase to the assumed finite continuous real spectral energy. Dini’s theorem on compact A gives precisely uniform shifted ENNReal tails. UniformTailAmplification supplies both the weighted cost and uniform weighted tails. The original generic summable_of_uniform_ennreal_tails and continuous_of_uniform_ennreal_tails in OrliczCommonEnergy apply directly to the weighted real scalar family, giving its actual finiteness and continuity.

For each beta>0, eventually betaw(n)>=1. Injectivity makes the preimage of any finite initial code segment finite. On its complement exp(-betah(i))<=exp(-a(i)); the remaining finite contribution proves summability. This requires no cofinal image, eigenvalue ordering, infinite index, faithful reference or finite ambient dimension. DiagonalHeat.diagonal_heat supplies the full graph, domain, heat, generator iff and uniqueness; DiagonalEnergy supplies the actual state-energy identity and lower form bound. AmplifiedDiagonalSeries(r,code,w,rho) denotes exactly the sum over the original i of ofReal((w(code(i)):Real)*thermalBaseLevel(r,code,i)*diagonal(r.basis,rho,i)). The constant one in the state energy comes from the actual trace-one diagonal HasSum. That same energy equals one plus this genuine amplified diagonal series and is at most 1+spectralEnergy(sigma,rho)+delta, with the corresponding finite real inequality.

Theorem 1.4 (Full-space energy bound from the original entropy premises).

Proof. Machine-checked in Lean as D5/S3/Quantum/Analysis/TraceClass/ContinuousEnergyHamiltonian.exists_thermalHamiltonian_of_continuous_entropy (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. M. E. Shirokov (2012). On a conjectured property of the von Neumann entropy valid in the commutative case. URL: https://arxiv.org/abs/1201.1093v1.

Commentary.

H is complete and separable over the complex numbers. A is nonempty, trace-norm closed and real convex; its operators are positive and have actual real trace one. Every actual spectral entropy is finite and actual realEntropy is ContinuousOn A. Compactness, bounded entropy, maximizing centers, a common reference, uniform tails, thermal coefficients and a Hamiltonian are not premises.

exists_unique_entropy_maximizer first supplies gamma0 in A. Bundle gamma0 as a positive contraction g0. Finiteness identifies spectralEntropy(g0) with ofReal(realEntropy(gamma0)), and the real value is nonnegative. Apply spectralEnergy_le_entropy_of_isMaxOn to get an energy bound on every rho in A. Hence A lies in the entire energySublevel(g0,realEntropy(gamma0)). isCompact_energySublevel and the original closedness make A compact. Apply fullCompactCommonReference to obtain gamma in A maximizing entropy and sigma in A with finite actual reference energy bounded by realEntropy(gamma)+log(2), with the corresponding finite real bound and both ENNReal and real continuity on A. All of these common-reference conclusions are retained in the endpoint.

Membership gives sigma its separate trace-one premise. Apply the new conditional construction to the native full basis with delta=1. The result is one literal full-space K, heat, strong generator and mixed-state energy satisfying ThermalOn, together with the strictly positive finite real bound 2+realEntropy(gamma)+log(2). Every rho in A satisfies the ENNReal bound by ofReal of this number and the same real inequality. All original kernel directions remain finite physical Hamiltonian modes. This is the mathematical Conjecture 1 endpoint under the explicit separable-H premises. No genuine relative-entropy D definition, continuity conclusion or Conjecture 2 conclusion is asserted. The relation to the source conjecture is stated without a literature-priority or official-acceptance claim.

References