Single-Defect Horizon Thermodynamic Asymptotics

Abstract

The squeezing coordinate, occupation number, and free energy of a positive single-defect depth have exact horizon identities and first-order boundary asymptotics.

Theorem 1.1 (The horizon corrections have universal leading coefficients).

$$\forall delta\in {\mathbb{R}}_{\ge 0},delta\ne 0\Rightarrow ((\forall omega,D(delta,omega)=\frac{delt{a}^2-omeg{a}^2}{delt{a}^2})\wedge (\forall omega,|omega|<delta\Rightarrow F(delta,omega)=2\log (\cosh (r(delta,omega)))=\log (1+N(delta,omega)))\wedge \underset{epsilon\to 0^{+}}{\lim }\frac{r(delta,delta-epsilon)-\frac{1}{2}\log (\frac{2delta}{epsilon})}{epsilon}=-\frac{1}{4delta}\wedge \underset{epsilon\to 0^{+}}{\lim }N(delta,delta-epsilon)-\frac{delta}{2epsilon}=-\frac{3}{4}\wedge \underset{epsilon\to 0^{+}}{\lim }\frac{F(delta,delta-epsilon)-\log (\frac{delta}{2epsilon})}{epsilon}=\frac{1}{2delta}\wedge \underset{omega\to delt{a}^{-}}{\lim }F(delta,omega)=\infty ).$$

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

Source. Repository-derived.

Commentary.

For every nonzero nonnegative depth delta, the existing horizon determinant law is retained. In the strict interior, the negative-log free energy equals both twice log cosh of the artanh squeezing coordinate and log of one plus occupation.

Writing epsilon=delta-omega and approaching zero from above, the three normalized errors converge respectively to -1/(4 delta), -3/4, and 1/(2 delta). These exact limits strengthen the source’s two O(epsilon) and one O(1) claims.

The Lean module computes the interior point delta=2, omega=1 and the excluded zero-depth case exactly, preventing totalized division or logarithms from making the theorem vacuous.

References

• Truth anchor: D5/S3/Weil/ZetaLinear/HorizonThermodynamicAsymptotics.single_defect_horizon_thermodynamic_asymptotics
• Dependency: D5/S3/Weil/ZetaLinear/HorizonFreeEnergyDivergence