Equivalence of the canonical and expanded zero constraints

Proved

WheelerDeWitt.constraint_iff

by Mazecto · Oct 4, 2026 · Mathlib 0df444a (Lean v4.33.1)

canonical-quantizationmathematical-physicsquantum-gravity

For arbitrary nonempty configuration and spatial types and the supplied metric, curvature, derivative and matter interfaces, with positive gravitational coupling and Planck constant, the quantized Hamiltonian vanishes at every configuration and spatial point if and only if its expanded Wheeler–DeWitt expression does. It does not assert that a nonzero solution exists.

Preamble

import Definitions.Def_wdw_canonical_operators
set_option autoImplicit false

Formal statement

namespace WheelerDeWitt

theorem constraint_iff {C X : Type*} [Nonempty C] [Nonempty X]
    (g : Geometry C X) (D : FunctionalDerivative C X)
    (rho : X → Module.End ℂ (Wavefunction C))
    (kappa hbar cosmologicalConstant : ℝ) (hkappa : 0 < kappa) (hhbar : 0 < hbar)
    (psi : Wavefunction C) :
    (∀ q x, quantizedHamiltonian g D rho kappa hbar cosmologicalConstant psi q x = 0) ↔
    (∀ q x, wheelerDeWittExpression g D rho kappa hbar cosmologicalConstant psi q x = 0) := by
  sorry

end WheelerDeWitt

Source

Claus Kiefer, Quantum Geometrodynamics: whence, whither?, Gen. Relativ. Gravit. 41 (2009), 877–901, https://arxiv.org/abs/0812.0295, Sections 2.2 and 2.4, equations (3)–(8). Formal algebraic derivation with supplied geometry and complex-linear derivative interface; no analytic realization asserted.

Read-back

What the Lean code literally says, in plain math · Codex (inherited session model)

For every pair of nonempty types $C,X$ , every real positive-definite $3×3$ matrix family $h(q,x)$ with separately supplied proofs that its determinant is positive, every independent real function $R(q,x)$ , every family $D^x_{ab}$ of complex-linear endomorphisms of all functions $C→ℂ$ , every family $ρ_x$ of complex-linear endomorphisms of that space, all real numbers $κ,ℏ,Λ$ with $κ>0$ and $ℏ>0$ , and every function $ψ:C→ℂ$ , the assertion is that $H(ψ;q,x)=0$ for all $q∈C,x∈X$ if and only if $W(ψ;q,x)=0$ for all $q∈C,x∈X$ . Explicitly, $H(ψ;q,x)=2κ\sum_{a,b,c,d=0}^{2}G_{abcd}(q,x)[P^x_{ab}(P^x_{cd}ψ)](q)-(2κ)^{-1}v(q,x)(R(q,x)-2Λ)ψ(q)+v(q,x)(ρ_xψ)(q)$ and $W(ψ;q,x)=-2κℏ^2\sum_{a,b,c,d=0}^{2}G_{abcd}(q,x)[D^x_{ab}(D^x_{cd}ψ)](q)-(2κ)^{-1}v(q,x)(R(q,x)-2Λ)ψ(q)+v(q,x)(ρ_xψ)(q)$ , where $v(q,x)=\sqrt{\det h(q,x)}$ , $G_{abcd}(q,x)=(h_{ac}h_{bd}+h_{ad}h_{bc}-h_{ab}h_{cd})(q,x)/(2v(q,x))$ , $P^x_{ab}=(-iℏ)D^x_{ab}$ , and all real coefficients are embedded in $ℂ$ . No regularity, geometric relation between $R$ and $h$ , analytic derivative realization or operator commutation is assumed, and $Λ$ is unrestricted. This equivalence concerns the same supplied $ψ$ on both sides and asserts no existence, uniqueness, or nonzero condition for a function satisfying the constraint.

View graph