$\psi$ has no absolutely continuous representative: $\psi\notin D(P)$

Proved

HeathcoteUnbounded.psi_not_mem_momentumDomain

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

functional-analysismathematical-physics

For the wave function $\psi$ of eq. (4) there is no function $g:\mathbb R\to\mathbb C$ that agrees with $\psi$ almost everywhere and is absolutely continuous on every compact interval $[a,b]$ .

In the source's words, $\psi$ "is discontinuous at $x=1$ and so is not in the domain of $P$ "; this shows the failure of $\psi\in D(Q)$ is independent of the canonical commutation relations.

Formalization Note Since elements of $L^2$ are a.e.-classes, the statement quantifies over all a.e.-representatives.

Preamble

import Mathlib
import Definitions.Def_HeathcoteUnbounded_Psi

open MeasureTheory

Formal statement

namespace HeathcoteUnbounded

theorem psi_not_mem_momentumDomain :
    ¬ ∃ g : ℝ → ℂ, psi =ᵐ[volume] g ∧ ∀ a b : ℝ, AbsolutelyContinuousOnInterval g a b := by sorry

end HeathcoteUnbounded

Source

A. Heathcote, "Unbounded Operators and the Incompleteness of Quantum Mechanics", Philosophy of Science 57 (1990), 523–534, pp. 5–6

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

ψ\psiψ has no absolutely continuous representative: ψ∉D(P)\psi\notin D(P)ψ∈/D(P)

$\psi$ has no absolutely continuous representative: $\psi\notin D(P)$