Full canonical Wheeler–DeWitt action identity

Proved

WheelerDeWitt.canonical_constraint

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

canonical-quantizationmathematical-physicsquantum-gravity

For arbitrary nonempty configuration and spatial types, supplied positive-definite metric and curvature data, complex-linear derivative and matter interfaces, positive gravitational coupling and Planck constant, arbitrary cosmological constant, and every wavefunctional, configuration and point, substituting −iℏD into the coefficient-left canonical Hamiltonian yields exactly the expanded Wheeler–DeWitt expression. This is the formal algebraic derivation of equation (7), not an analytic operator construction.

Preamble

import Definitions.Def_wdw_canonical_operators
set_option autoImplicit false

Formal statement

namespace WheelerDeWitt

theorem canonical_constraint {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 : C) (x : X) :
    quantizedHamiltonian g D rho kappa hbar cosmologicalConstant psi q x =
      wheelerDeWittExpression g D rho kappa hbar cosmologicalConstant psi q x := 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 family of real positive-definite $3×3$ matrices $h(q,x)$ equipped also with proofs of positive determinant, every independently supplied 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 same space, all real $κ,ℏ,Λ$ satisfying $κ>0$ and $ℏ>0$ , every function $ψ:C→ℂ$ , and every $q∈C,x∈X$ , the following equality of complex numbers is asserted: $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)=-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)$ . Here indices range over $\{0,1,2\}$ , $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))$ , and $P^x_{ab}=(-iℏ)D^x_{ab}$ . All real coefficients are embedded in $ℂ$ . There is no regularity assumption on $ψ,h,R$ , no derivative realization or commutation hypothesis on $D$ , no additional condition on $ρ$ , and no restriction on $Λ$ . The assertion is equality of the two expressions at each supplied pair; it does not assert that either expression vanishes or that a function satisfying such a vanishing condition exists.

View graph