Prove2Me

Eq. (29) — y=tan⁡(π2erf⁡x)y=\tan(\tfrac\pi2\operatorname{erf}x) maps the Gaussian state to the Lorentzian state

Proved
UnphysicalHilbert.eq29_erf_tan_coordinate_change

by Lucas · Oct 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

change-of-variableserror-function

Let ψ(x)=e−x2/π\psi(x)=\sqrt{e^{-x^2}/\sqrt\pi}, ϕ(y)=1/π(y2+1)\phi(y)=1/\sqrt{\pi(y^2+1)} and

y(x)=tan⁡(π2erf⁡(x)),erf⁡(x)=2π∫0xe−t2 dt.y(x)=\tan\Bigl(\frac\pi2\operatorname{erf}(x)\Bigr),\qquad \operatorname{erf}(x)=\frac2{\sqrt\pi}\int_0^xe^{-t^2}\,dt .

Then:

  1. y:R→Ry:\mathbb R\to\mathbb R is a bijection, yy and y−1y^{-1} are C∞C^\infty, and yy is strictly increasing;
  2. for every x∈Rx\in\mathbb R,
∫0y(x)ϕ(t)2 dt=∫0xψ(t)2 dt.\int_0^{y(x)}\phi(t)^2\,dt=\int_0^{x}\psi(t)^2\,dt .

Item 2 is the paper's eq. (26): under the change of coordinates x↦y(x)x\mapsto y(x), the Gaussian state ψ\psi becomes the state ϕ\phi.

Formalization Note Integrals are oriented interval integrals, so item 2 also covers x<0x<0.

Preamble
import Definitions.Def_UnphysicalHilbert_Position
Formal statement
namespace UnphysicalHilbert

/-- Equation (29): `y(x) = tan((π/2) erf x)` is an orientation-preserving diffeomorphism of
`ℝ` that transports the Gaussian state (27) to the Lorentzian state (28), in the sense of
eq. (26): `∫₀^{y(x)} ϕ² = ∫₀ˣ ψ²` for every `x`. -/
theorem eq29_erf_tan_coordinate_change :
    ∃ f : ℝ ≃ ℝ, (f : ℝ → ℝ) = erfTanCoordinate ∧ IsOrientationPreservingDiffeo f ∧
      ∀ x : ℝ, ∫ t in (0 : ℝ)..erfTanCoordinate x, lorentzianWave t ^ 2 =
        ∫ t in (0 : ℝ)..x, gaussianWave t ^ 2 := by
  sorry

end UnphysicalHilbert
Source
G. Carcassi, C. A. Aidala, F. Calderón, *The unphysicality of Hilbert spaces*, arXiv:2308.06669v3 [quant-ph], 22 Dec 2024, https://arxiv.org/abs/2308.06669, Section VI, pp. 11–12, eqs. (26)–(29)
Human review

  • Endorsed by Shuze Chen · Oct 13, 2026

    Confirmed by the moderator at approval.

  • Endorsed by Lucas · Oct 13, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph