Critical Endpoint of the Prime Heat Curve
Abstract
The actual prime heat trace diverges at its critical endpoint, and normalization gives an infinite-variation Hilbert curve.
Definition 1.1 (The actual square-summable prime heat vector).
Formalization. D5/S3/AnalyticClosure/PrimeSpectrumBoundaryEscape.primeHeatVector (✓ std3).
Source. Repository-derived.
Commentary.
Under the prime-spectrum hypotheses, x(sigma) has coordinates exp(-(sigma/2) beta(k+1) log p) for sigma>alpha=1/b0. It is an element of the actual lp space over Nat.Primes times Nat; its value outside that open domain is the zero vector. No artificial zero spectral index is added.
Theorem 1.2 (Heat-trace divergence from the right).
Proof. Machine-checked in Lean as D5/S3/AnalyticClosure/PrimeSpectrumBoundaryEscape.prime_spectrum_heat_trace_tendsto_atTop (✓ std3). ∎
Source. Repository-derived.
Commentary.
The boundary prime-reciprocal layer is not summable. Consequently its nonnegative finite partial sums are unbounded. Each such finite heat sum is continuous in sigma, and right-side summability bounds it by the actual heat trace. Thus the real heat trace tends to positive infinity from the right. The total tsum at the divergent endpoint is not interpreted as an infinite real value.
Theorem 1.3 (Divergence of the actual Hilbert norm).
Proof. Machine-checked in Lean as D5/S3/AnalyticClosure/PrimeSpectrumBoundaryEscape.prime_spectrum_heat_norm_tendsto_atTop (✓ std3). ∎
Source. Repository-derived.
Commentary.
The squared lp norm equals the real heat trace at sigma. The norm therefore tends to positive infinity at alpha from the right.
Theorem 1.4 (No strong endpoint limit).
Proof. Machine-checked in Lean as D5/S3/AnalyticClosure/PrimeSpectrumBoundaryEscape.prime_spectrum_normalized_heat_not_tendsto (✓ std3). ∎
Source. Repository-derived.
Commentary.
Every fixed coordinate of the normalized vector tends to zero, since its unnormalized coefficient has a finite endpoint value and its norm diverges. The actual vector is nonzero, so normalization has norm one. Any strong lp limit would have every coordinate zero, contradicting convergence of norms to one.
Theorem 1.5 (Infinite metric variation at the critical endpoint).
Proof. Machine-checked in Lean as D5/S3/AnalyticClosure/PrimeSpectrumBoundaryEscape.prime_spectrum_normalized_heat_eVariationOn_eq_top (✓ std3). ∎
Source. Repository-derived.
Commentary.
For every c>alpha the normalized Hilbert curve has infinite total metric variation on (alpha,c). Finite variation would give a strong right limit in the complete lp space, contradicting the preceding theorem. This establishes metric length of the actual curve; no Fisher-information derivative identity, Riemannian metric identification, global manifold completeness, or RH conclusion is asserted.
References
- Truth anchor:
D5/S3/AnalyticClosure/PrimeSpectrumBoundaryEscape.primeHeatVector - Truth anchor:
D5/S3/AnalyticClosure/PrimeSpectrumBoundaryEscape.prime_spectrum_heat_norm_tendsto_atTop - Truth anchor:
D5/S3/AnalyticClosure/PrimeSpectrumBoundaryEscape.prime_spectrum_heat_trace_tendsto_atTop - Truth anchor:
D5/S3/AnalyticClosure/PrimeSpectrumBoundaryEscape.prime_spectrum_normalized_heat_eVariationOn_eq_top - Truth anchor:
D5/S3/AnalyticClosure/PrimeSpectrumBoundaryEscape.prime_spectrum_normalized_heat_not_tendsto - Dependency: D5/S3/AnalyticClosure/PrimeSpectrumHeatL2