Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Real Heat of the Actual Centered Boundary Operator

Abstract

The original real centered boundary space G0 carries a spectral heat semigroup whose generator is exactly minus the original boundary operator on its entire centered domain.

Definition 1.1 (The Real Heat Multiplier).

Lean statement: D5/S3/Arith/FibonacciAtomic/Geometry/BiasedBoundaryHeat.heat

Formalization. D5/S3/Arith/FibonacciAtomic/Geometry/BiasedBoundaryHeat.heat (✓ std3).

Source. Repository-derived.

Commentary.

For a real Hilbert basis e of the original G0 and positive covariance eigenvalues mu, heat(e,mu,t) transports the bounded coordinate multipliers exp(-t/mu(i)) through e.repr. Time t is nonnegative. The map acts on every vector of G0; it does not replace that space by finite sequences.

Definition 1.2 (The Ambient Heat).

Lean statement: D5/S3/Arith/FibonacciAtomic/Geometry/BiasedBoundaryHeat.fullHeat

Formalization. D5/S3/Arith/FibonacciAtomic/Geometry/BiasedBoundaryHeat.fullHeat (✓ std3).

Source. Repository-derived.

Commentary.

On the original ambient G, fullHeat fixes constG(mean(F)) and applies centered heat to the orthogonal centered part Pi(F), included isometrically back into G. It uses the original real carriers and the same covariance sequence.

Theorem 1.3 (The Actual Heat, Trace and Generator).

Lean statement: D5/S3/Arith/FibonacciAtomic/Geometry/BiasedBoundaryHeat.actual_heat

Proof. Machine-checked in Lean as D5/S3/Arith/FibonacciAtomic/Geometry/BiasedBoundaryHeat.actual_heat (✓ std3). ∎

Source. Repository-derived.

Commentary.

One application of the actual spectral counting theorem supplies paired bases e on G0 and k on the effective edge space K, together with one positive nonincreasing covariance sequence mu tending to zero. The original Sigma and ambient C have their actual paired diagonal actions on this same family. The original source centeredTrace with codomain G0 has the same paired action before inclusion. Its composition with the actual isometric inclusion G0 into G equals ambient C, and centeredTrace adjoint composed with centeredTrace is literally Sigma on the entire original edge carrier. Every repeated eigenvalue keeps its own basis occurrence.

The transported heat operators form a strongly continuous contraction semigroup. They are positive, and their intrinsic extended positive trace is the sum of ofReal(exp(-t/mu(i))) for every nonnegative t. The formula also holds at time zero as an extended value. At every positive time the series is summable and the intrinsic positive trace is finite. The real trace value is the toReal of this proved finite extended trace.

For all centered vectors u and v, the strong limit at time zero from the right of t inverse times (S(t)u-u) equals v if and only if (u,-v) lies in the original boundaryOperator graph after the original isometric inclusion into G. The parameterized polar graph and coefficient identities apply to the same e,k,mu and give the exact all-vector coefficient graph. Continuous coefficient functionals prove one direction. Finite basis projections of both the vector and its original graph image, followed by the real semigroup generator-limit theorem, prove the reverse direction.

Any other strongly continuous contraction semigroup with this same full generator graph equals S. The multiplier, finite-span continuity and uniqueness design reuse the standard construction in DiagonalHeat and the attributed MarkovProcess supplies in ContractionSemigroup. No self-adjoint realization, inverse-domain, spectral exhaustion or counting proof is repeated.

The ambient heat is also a strongly continuous positive contraction semigroup, with the strong generator equal to minus the original boundaryOperator on every vector in its exact domain. It uniquely has that generator. Its restriction to the original G0 is the centered heat, and it fixes every original constant. A complete orthonormal basis consisting of constG(1) and the included centered basis proves that its intrinsic trace is exactly one plus the centered trace, with exactly one added constant mode.

For every s>0 the centered trace lies between (b/s) exp(-s/b) and B/s, with b=phi to the power minus two and B=2 phi cubed. When 0<s<=b, its lower bound is b/(exp(1) s), including equality in the time cutoff. The proof compares the same ordered reciprocal eigenvalues with shifted geometric exponentials. Their summability is established before using real infinite sums or the toReal trace.

The inclusive finite cutoff count equals the sum of inclusive mode indicators, counting every repeated occurrence. The Laplace identity is proved with the original positiveCount: the centered trace is s times the integral on u>0 of exp(-s u) Nplus(u). Each indicator tail is integrable; the norms of their integrals have a summable series. Interchanging sum and integral is therefore justified, and the closed tail endpoint has zero Lebesgue measure.

The logarithm of the inclusive positive count divided by log(lambda) tends to one at infinity. The logarithm of the original one-based eigenvalue divided by log(j) also tends to one. The centered and ambient heat logarithms divided by log(1/s) tend to one from positive times at zero. The proof squeezes each quotient between positive constant multiples with the same diverging logarithmic denominator. It asserts no Weyl coefficient or additive counting remainder.

The separate operator approximation-number/singular-value correspondence, Schatten classes and equivalence of finite intrinsic positive trace with trace class remain open. The heat and intrinsic-trace statements therefore do not establish the full original Theorem 3.1 or its covariance ideal corollary. Sigma, rather than C, is the object of the source Hilbert-Schmidt assertion. The original C has centered codomain G0. Its precise ambient inclusion and Gram equality are proved here; the full-carrier singular-value correspondence remains open.

References