Mathematical Physics

Motivation

Quantum mechanics represents the states of a system by unit vectors (normed rays) of a complex Hilbert space $\mathcal H$ and its observables by self-adjoint operators on $\mathcal H$. The most important observables — position, momentum, energy — are unbounded. A. Heathcote's paper Unbounded Operators and the Incompleteness of Quantum Mechanics (Philosophy of Science 57, 1990, 523–534) draws attention to a mathematical fact that is routinely glossed over in physical texts: an unbounded self-adjoint operator cannot be defined on all of $\mathcal H$, and there are concrete normalized wave functions on which the position and momentum operators do not act at all. The paper uses this to argue that the standard postulates of quantum mechanics are, in a precise sense, incomplete.

This mission isolates the mathematical content of that argument, which is a clean and checkable piece of functional analysis on $L^2(\mathbb R)$.

Setting

Let $\mathcal H$ be a complex Hilbert space. A (partially defined) linear operator $A$ has a domain $D(A)\subseteq\mathcal H$; it is bounded if there is $k\in\mathbb R$ with $\|A\psi\|\le k\|\psi\|$ for all $\psi\in D(A)$, and unbounded otherwise. It is self-adjoint if it equals its Hilbert adjoint, $A=A^*$, which includes $D(A)=D(A^*)$.

On $\mathcal H=L^2(\mathbb R)$:

1. The position operator acts by $(Q\psi)(x)=x\,\psi(x)$ on

$$D(Q)=\Big\{\psi\in L^2(\mathbb R): \int_{\mathbb R}x^2|\psi(x)|^2\,dx<\infty\Big\}\qquad\text{(eq. (3))}.$$

2. The momentum operator $P\psi=\hbar i^{-1}\,d\psi/dx$ has, in the paper's description, domain $D(P)$ consisting of the absolutely continuous functions in $L^2(\mathbb R)$.
3. Heathcote's wave function (eq. (4)) is

$$\psi(x)=\begin{cases}x^{-1}, & x\ge 1,\\ 0, & x<1.\end{cases}$$

Formalization targets

Goal

There is a unit vector of $L^2(\mathbb R)$, namely the class of $\psi$, lying in neither domain:

$$\exists\,\varphi\in L^2(\mathbb R):\quad \varphi=\psi\ \text{a.e.},\qquad \|\varphi\|=1,\qquad \varphi\notin D(Q),\qquad \varphi\notin D(P).$$

Milestones

1. Hellinger–Toeplitz (p. 2, footnote 1): a symmetric operator defined on all of a Hilbert space is bounded (an existing platform theorem).
2. Unbounded self-adjoint operators (p. 2, footnote 2): if $A=A^*$ is unbounded then $D(A)$ is dense and $D(A)\neq\mathcal H$.
3. Normalization (p. 5): $\psi\in L^2(\mathbb R)$ and $\int|\psi|^2=\int_1^\infty x^{-2}dx=1$.
4. Not in $D(Q)$ (p. 5): $\int x^2|\psi(x)|^2dx=\infty$.
5. Not in $D(P)$ (pp. 5–6): no a.e.-representative of $\psi$ is absolutely continuous on every compact interval.
6. Infinite position expectation (p. 9): $\int|x|\,|\psi(x)|^2dx=\int_1^\infty x^{-1}dx=\infty$.

Significance

The result. The goal shows that the two postulates "every normed ray is a state" and "observables are self-adjoint operators" force the existence of states on which the position operator (and, independently, the momentum operator) is undefined. Milestone 5 is what the paper uses to separate this phenomenon from the canonical commutation relations: the failure of $\psi\in D(Q)$ is not explained by $\psi$ being "sharp in momentum", because $\psi$ is not even in $D(P)$. Milestone 6 records the physical reading: the mean position of this normalized state is infinite.

Formalizing it. The individual facts are standard and elementary; none of them is new. What the mission produces is a machine-checked version of the paper's argument stated against the actual $L^2$ space and Mathlib's notion of unbounded operators and adjoints, with the domain conventions made explicit.

Difficulty

The calculus is easy; the subtleties are in the bookkeeping. Elements of $L^2(\mathbb R)$ are almost-everywhere classes, so "$\psi$ is discontinuous at $1$" does not by itself show $\psi\notin D(P)$: one must rule out every a.e.-modification of $\psi$ being absolutely continuous. Similarly, the Hellinger–Toeplitz argument gives $D(A)\neq\mathcal H$ but not density, which comes from the adjoint being a genuine operator.

Formalization scope

• Operators are Mathlib's partially defined linear maps H →ₗ.[ℂ] H; self-adjointness is IsSelfAdjoint with respect to the adjoint A†, over a complex complete inner product space.
• $L^2(\mathbb R)$ is Lp ℂ 2 volume on ℝ; $D(Q)$ and $D(P)$ are subsets of it. Integrals of non-negative quantities are Lebesgue integrals valued in $[0,\infty]$, so "$=\infty$" is literal and not a junk value.
• $D(P)$ follows the paper (absolutely continuous elements, i.e. having a representative absolutely continuous on every $[a,b]$) and omits the standard requirement $\psi'\in L^2$. This set contains the standard domain, so non-membership is a stronger statement.
• The paper's further claim that $\psi\notin D(H)$ for a Hamiltonian $H=P^2/2m+V$ is stated there without proof and for an unspecified potential $V$, and is not included.
• Trivialization is excluded: the goal pins $\varphi$ to the explicit function $\psi$ and requires $\|\varphi\|=1$.

Selected references

• A. Heathcote, Unbounded Operators and the Incompleteness of Quantum Mechanics, Philosophy of Science 57 (1990), 523–534.
• M. Reed and B. Simon, Methods of Modern Mathematical Physics I: Functional Analysis, revised ed., Academic Press, 1980.

Motivation

The Yang–Mills functional measures the total curvature of a connection on a principal bundle. Its critical points, the Yang–Mills connections, are the non-abelian generalization of solutions of Maxwell's equations, and in four dimensions the most important among them are the self-dual and anti-self-dual connections (instantons), whose moduli spaces underlie Donaldson theory of smooth four-manifolds. A basic and frequently used fact, recorded as Proposition 3.1.1 in K. Uhlenbeck's lectures Equations of Gauge Theory (notes by L. Fredrickson, Temple University, 2012), is that instantons are not merely critical points: within a fixed topological class and with fixed boundary data they are absolute minimizers of the Yang–Mills energy. The same "energy identity" argument is the template the notes later apply to the Kapustin–Witten equations (Proposition 3.1.5).

Timeline of the ideas involved: Yang and Mills introduce the equations (1954); Belavin, Polyakov, Schwartz and Tyupkin observe the topological lower bound on the energy and its saturation by self-dual fields (1975); Atiyah, Hitchin and Singer study the deformation theory of instantons (1977–78); Donaldson uses the instanton moduli space in four-manifold topology (1983).

Setting

Work on the trivial principal $SU(n)$-bundle over a closed box $\Omega=[a,b]=\prod_{\mu=0}^{3}[a_\mu,b_\mu]\subset\mathbb R^4$ with the Euclidean metric. A connection is $D_A=d+A$ with $A=\sum_\mu A_\mu\,dx^\mu$, where each $A_\mu$ is a smooth map into the Lie algebra $\mathfrak{su}(n)$ of traceless skew-Hermitian $n\times n$ complex matrices. Its curvature is the $\mathfrak{su}(n)$-valued two-form $F_A=dA+A\wedge A$ with coefficients

$$(F_A)_{\mu\nu}=\partial_\mu A_\nu-\partial_\nu A_\mu+[A_\mu,A_\nu].$$

The Hodge star on two-forms is $(\star F)_{\mu\nu}=\tfrac12\sum_{\rho,\sigma}\varepsilon_{\mu\nu\rho\sigma}F_{\rho\sigma}$, with $\varepsilon$ the Levi-Civita symbol. A two-form is self-dual if $\star F=F$ and anti-self-dual if $\star F=-F$. The pointwise norm is $|F|^2=\sum_{\mu<\nu}\operatorname{Re}\operatorname{tr}(F_{\mu\nu}F_{\mu\nu}^{*})$, and the Yang–Mills functional on $\Omega$ is

$$\mathrm{Ym}_\Omega(A)=\int_\Omega |F_A|^2\,d\mathrm{vol}.$$

The Chern–Weil density $\operatorname{tr}(F\wedge F)$ is the coefficient $\tfrac14\sum\varepsilon_{\mu\nu\rho\sigma}\operatorname{tr}(F_{\mu\nu}F_{\rho\sigma})$ of $dx^0\wedge dx^1\wedge dx^2\wedge dx^3$, and the Chern–Simons three-form is $CS(A)=\operatorname{tr}(A\wedge dA+\tfrac23A\wedge A\wedge A)$, with flux components $K^\mu=\sum\varepsilon_{\mu\nu\rho\sigma}\operatorname{tr}(A_\nu\partial_\rho A_\sigma+\tfrac23A_\nu A_\rho A_\sigma)$.

Formalization targets

Goal (Proposition 3.1.1, box version)

If $A$ and $B$ are smooth $SU(n)$-connections on $\Omega$ that agree on $\partial\Omega$, and $F_A$ is self-dual on all of $\Omega$ or anti-self-dual on all of $\Omega$, then

$$\mathrm{Ym}_\Omega(A)\le \mathrm{Ym}_\Omega(B).$$

Milestones

1. Lemma 3.1.2. For an $\mathfrak{su}(n)$-valued two-form $F$: $|F\pm\star F|^2=2|F|^2\mp2\operatorname{tr}(F\wedge F)$.
2. Fact 3.1.3, local form. $\operatorname{tr}(F_A\wedge F_A)=\sum_\mu\partial_\mu K^\mu$, i.e. $\operatorname{tr}(F_A\wedge F_A)=d\,CS(A)$.
3. Fact 3.1.3, box form. $\int_\Omega\operatorname{tr}(F_A\wedge F_A)=\int_{\partial\Omega}CS(A)$ (the topological term vanishes for the trivial bundle).
4. Energy bound (proof of Proposition 3.1.1). $\mathrm{Ym}_\Omega(A)\ge \mp\int_{\partial\Omega}CS(A)$.
5. Equality case (proof of Proposition 3.1.1). On a non-degenerate box, $\mathrm{Ym}_\Omega(A)=-\int_{\partial\Omega}CS(A)$ iff $F_A$ is self-dual on $\Omega$, and $\mathrm{Ym}_\Omega(A)=\int_{\partial\Omega}CS(A)$ iff $F_A$ is anti-self-dual on $\Omega$.

Significance

The energy identity turns a second-order variational problem into a first-order one: any connection satisfying the first-order self-duality equation is automatically a Yang–Mills connection, and in fact a global minimizer in its class. This is the reason instanton moduli spaces are the natural objects of four-dimensional gauge theory, and it is the model for the corresponding minimization statements for the Kapustin–Witten equations treated later in the same notes. The result is classical and its proof is known; the remaining work is formal: a machine-checked development of the curvature, Hodge star, Chern–Simons transgression and the boundary integration on boxes, none of which are currently packaged in this form in Mathlib.

Difficulty

The algebraic identity of Lemma 3.1.2 is a finite computation. The substantive step is the transgression formula $\operatorname{tr}(F_A\wedge F_A)=d\,CS(A)$, a cancellation between derivative terms and cubic terms that depends on cyclicity of the trace and on the antisymmetry of $\varepsilon$, followed by Stokes' theorem on the box with correct face orientations. The naive approach of comparing $|F_A|^2$ and $|F_B|^2$ pointwise fails: the two connections agree only on the boundary, and only the integrated topological term is boundary-determined.

Formalization scope

The general setting of the notes (a $G$-bundle over a compact oriented Riemannian four-manifold with boundary, topological class $c_2(P)=k$) is replaced by the trivial $SU(n)$-bundle over a closed axis-parallel box in Euclidean $\mathbb R^4$, so the topological term $8\pi^2c_2(P)$ is zero. Connections are smooth on all of $\mathbb R^4$ (equivalently, smooth up to the boundary of the box) and every coefficient takes values in $\mathfrak{su}(n)$. Two-forms are stored as antisymmetric $4\times4$ families of matrices; partial derivatives are taken entrywise; integrals are Lebesgue integrals over the box and over its faces. "Fixed boundary data" means $A=B$ at every point of $\partial\Omega$. Self-duality is $\star F=F$, matching $F=\star F$ in Section 2.2 of the notes.

Two sign/normalization corrections relative to the printed notes are made deliberately: Lemma 3.1.2 is stated with the sign obtained in its own proof on p. 32 ($\mp$ rather than the printed $\pm$, because $B^*=-B$ on $\mathfrak{su}(n)$), and the Chern–Simons form uses the standard coefficient $\tfrac23$ in $\operatorname{tr}(A\wedge dA+\tfrac23A^3)$, i.e. $\operatorname{tr}(A\wedge F_A)-\tfrac13\operatorname{tr}(A^3)$, for which $d\,CS=\operatorname{tr}(F\wedge F)$ holds, instead of the printed $\tfrac16$.

A trivializing formalization would make the boundary condition or the self-duality hypothesis unsatisfiable; here the zero connection is self-dual and satisfies every hypothesis, and the statements are not vacuous.

Reusable infrastructure: Levi-Civita symbol and Hodge star on $\Lambda^2\mathbb R^4$ with matrix coefficients, curvature of matrix-valued connections, the Chern–Simons transgression, and Stokes' theorem for flux forms on boxes (Mathlib's divergence theorem on boxes is the natural tool). Contributions to any milestone are welcome.

Selected references

• K. Uhlenbeck, Equations of Gauge Theory, notes by L. Fredrickson, Emil Grosswald Lectures, Temple University, 2012 (the source of all statements; Section 3.1, pp. 29–32).
• C. N. Yang, R. L. Mills, Conservation of isotopic spin and isotopic gauge invariance, Phys. Rev. 96 (1954), 191–195. https://doi.org/10.1103/PhysRev.96.191
• A. A. Belavin, A. M. Polyakov, A. S. Schwartz, Yu. S. Tyupkin, Pseudoparticle solutions of the Yang–Mills equations, Phys. Lett. B 59 (1975), 85–87. https://doi.org/10.1016/0370-2693(75)90163-X
• S. K. Donaldson, An application of gauge theory to four-dimensional topology, J. Differential Geom. 18 (1983), 279–315. https://doi.org/10.4310/jdg/1214437665

Motivation

The second law of thermodynamics is a physical law based on universal empirical observation concerning heat and energy interconversions. Two of its classical statements are impossibility statements about machines. Rudolf Clausius (1854): "Heat can never pass from a colder to a warmer body without some other change, connected therewith, occurring at the same time." Lord Kelvin: "It is impossible for any system to operate in a thermodynamic cycle and deliver a net amount of energy by work to its surroundings while receiving energy by heat transfer from a single thermal reservoir." The Wikipedia article Second law of thermodynamics records that these two have been shown to be equivalent.

The law is not only prohibitive. Sadi Carnot's analysis of heat engines (1824) yields an upper bound on the efficiency of any engine running between two heat reservoirs, attained by reversible engines and strictly missed by irreversible ones, and — crucially — the same for all reversible engines whatever the working substance. That substance-independence is what makes a thermodynamic temperature possible: as the article puts it, "The second law allows a distinguished temperature scale, which defines an absolute, thermodynamic temperature, independent of the properties of any particular reference thermometric body."

This mission formalizes that chain: from the two impossibility statements, through Carnot's theorem, to the existence and uniqueness of the absolute temperature scale normalized by the Kelvin convention at the triple point of water.

Setting

A cyclically operating device is recorded by the heat it exchanges with thermal reservoirs over one complete cycle. Reservoirs are labelled by empirical temperature, an element of a linearly ordered type $\Theta$ ($s<t$: the reservoir at $s$ is colder). A cycle is a finitely supported function $c:\Theta\to\mathbb R$, where $c(t)$ is the net heat absorbed by the device from the reservoir at $t$ (negative if rejected). Because the device returns to its initial state, the first law makes the net work delivered equal to the total heat absorbed:

$$W(c)=\sum_{t}c(t).$$

The cycles that can actually be realized form a set $\mathcal C$, assumed to be a convex cone: the null cycle is realizable; two realizable devices can be run side by side, their heat exchanges adding; and a realizable device can be scaled by any factor $r\ge0$. A cycle is reversible when $c\in\mathcal C$ and $-c\in\mathcal C$, and operates between $h$ and $k$ when it exchanges heat with no other reservoir. A Carnot engine between a hot $h$ and a cold $k$ is a reversible cycle operating between them with $c(h)>0$, $c(k)<0$ and $W(c)>0$. The efficiency relative to the hot reservoir is $\eta=W(c)/c(h)$.

In this language:

• Clausius statement. For $k<h$: every realizable cycle operating between $h$ and $k$ with $W(c)=0$ satisfies $c(k)\le0$.
• Kelvin statement. Every realizable cycle exchanging heat with a single reservoir satisfies $W(c)\le0$.
• $\mathcal C$ admits Carnot engines when a Carnot engine exists between every pair of reservoirs at different temperatures.

Formalization targets

Goal: the thermodynamic temperature scale

Assume $\mathcal C$ is a convex cone satisfying the Clausius statement and admitting Carnot engines, and fix a reference reservoir $T_0$. Then there is exactly one $T:\Theta\to\mathbb R$ with

$$T>0,\qquad T(T_0)=273.16,\qquad \frac{|e(k)|}{|e(h)|}=\frac{T(k)}{T(h)}\quad\text{for every Carnot engine } e \text{ between } k<h.$$

The content is that the left-hand ratio, a property of an engine, depends on the engine only through its two reservoirs, and does so as a ratio of numbers attached to the reservoirs. The normalization $273.16$ at $T_0$ is the Kelvin convention; as the article notes, "any reference temperature and any positive numerical value could be used".

The two impossibility statements

$$\text{Clausius}(\mathcal C)\iff\text{Kelvin}(\mathcal C)$$

for a convex cone admitting Carnot engines over at least two reservoir temperatures.

Carnot's theorem

For $k<h$ and a Carnot engine $e$ between them, every realizable engine $c$ between the same two reservoirs satisfies $\eta(c)\le\eta(e)$, with strict inequality when $c$ is irreversible ($-c\notin\mathcal C$); and any two Carnot engines between $h$ and $k$ have equal efficiency.

Significance

The goal makes explicit which features of the realizable processes are used when a textbook defines absolute temperature. The three hypotheses — convex cone, Clausius statement, existence of Carnot engines — are exactly what the derivation needs; the working substance, the equation of state, and the mechanism of a device never appear. Uniqueness is the part that is usually left implicit: the Kelvin normalization at one reservoir pins the scale completely.

The milestones follow the article's own order: equation (1) for the efficiency of an arbitrary engine; the equivalence of the Clausius and Kelvin statements; the three clauses of Carnot's theorem; the composition law $f(T_1,T_3)=f(T_1,T_2)f(T_2,T_3)$ for the reversible heat ratio across an intermediate reservoir; the conversion of that law into a scale; and the resulting Carnot efficiency $\eta=1-T_{\mathrm C}/T_{\mathrm H}$.

Difficulty

The mathematics is elementary — convex cones in a space of finitely supported real functions, and one functional equation — but the bookkeeping is where faithfulness is won or lost. Carnot's theorem is proved by scaling a candidate engine against a reversed Carnot engine so that the composite does no net work, which makes the Clausius statement applicable; the equality case has to identify the candidate as a positive multiple of the Carnot engine before concluding that it is reversible. The composition law requires the intermediate reservoir to be exactly balanced, so that the composite is again a two-reservoir engine — the article's remark that "the heat $q_2$ flown from the engine 2 to the intermediate reservoir must be equal to the heat $q_2^*$ flown out from the reservoir to the engine 3". The functional equation must be solved without assuming the reference reservoir is the hottest or the coldest, so the scale is defined by $f(T_0,\cdot)$ below $T_0$ and by $1/f(\cdot,T_0)$ above it, and the composition law is applied in four different orderings.

Formalization scope

• Reservoir temperatures form an arbitrary linearly ordered type; the order is the empirical hotter/colder relation and nothing else is assumed of it.
• Heat is positive into the device. Work is the sum of the heats, which is the first law for a cycle; the first law is therefore built into the model rather than stated.
• A device is recorded only by its heat exchanges. Working substance, the states traversed, quasi-staticity and the internal construction do not appear; "reversible" means exactly that the reversed heat exchange pattern is also realizable.
• The Clausius statement is formalized for a cycle with zero net work exchanging heat with exactly two reservoirs: that is the article's "without some other change, connected therewith, occurring at the same time".
• Out of scope for this mission: the Clausius inequality $\oint \delta Q/T_{\mathrm{surr}}\le0$, the definition of entropy as a state function, Carathéodory's and Planck's formulations, the statistical-mechanical derivations, and the Clausius–Duhem inequality for continua.

Selected references

• Wikipedia, Second law of thermodynamics, revision oldid=1378607758. https://en.wikipedia.org/w/index.php?title=Second_law_of_thermodynamics&oldid=1378607758
• S. Carnot, Réflexions sur la puissance motrice du feu, 1824.
• R. Clausius, Über eine veränderte Form des zweiten Hauptsatzes der mechanischen Wärmetheorie, Annalen der Physik 93 (1854), 481–506.

Motivation

The Einstein field equations (EFE) are the field equations of general relativity. They relate the curvature of spacetime, encoded in the metric $g_{\mu\nu}$, to its matter–energy content, encoded in the stress–energy tensor $T_{\mu\nu}$:

$$G_{\mu\nu}+\Lambda g_{\mu\nu}=\kappa T_{\mu\nu},\qquad \kappa=\frac{8\pi G}{c^4}.$$

They were published by Einstein in 1915. A structural requirement on any such equation is that it be compatible with the local conservation of energy and momentum, $\nabla_\beta T^{\alpha\beta}=0$. For the EFE this compatibility is automatic: the left-hand side is identically divergence-free by the contracted Bianchi identity, so the field equations force conservation of the right-hand side. This mission formalizes that implication together with the standard algebraic reformulations of the equations, following the Wikipedia article Einstein field equations (revision 1374672993).

Setting

Everything is written in one coordinate chart. A point is $x\in\mathbb{R}^D$, where $D$ is the spacetime dimension (not fixed to $4$). A 2-tensor field is a matrix-valued function $x\mapsto T_{ab}(x)$. A metric on an open set $U$ is a 2-tensor field $g$ whose components are $C^\infty$ on $U$ and which is symmetric and nondegenerate at each point of $U$; $g^{ab}$ denotes the inverse matrix. Partial derivatives $\partial_a$ are coordinate (Fréchet) derivatives. Using the Misner–Thorne–Wheeler $(+\,+\,+)$ convention adopted by the source:

• Christoffel symbols $\Gamma^c_{ab}=\tfrac12g^{cs}(\partial_ag_{sb}+\partial_bg_{sa}-\partial_sg_{ab})$;
• Riemann tensor $R^\mu{}_{\alpha\beta\gamma}=\partial_\beta\Gamma^\mu_{\alpha\gamma}-\partial_\gamma\Gamma^\mu_{\alpha\beta}+\Gamma^\mu_{\sigma\beta}\Gamma^\sigma_{\gamma\alpha}-\Gamma^\mu_{\sigma\gamma}\Gamma^\sigma_{\beta\alpha}$;
• Ricci tensor $R_{\mu\nu}=R^\alpha{}_{\mu\alpha\nu}$, scalar curvature $R=g^{\mu\nu}R_{\mu\nu}$, Einstein tensor $G_{\mu\nu}=R_{\mu\nu}-\tfrac12Rg_{\mu\nu}$;
• covariant derivative $\nabla_\lambda T_{\mu\nu}=\partial_\lambda T_{\mu\nu}-\Gamma^\sigma_{\lambda\mu}T_{\sigma\nu}-\Gamma^\sigma_{\lambda\nu}T_{\mu\sigma}$ and divergence $(\operatorname{div}T)_\mu=g^{\nu\lambda}\nabla_\lambda T_{\mu\nu}$, the index-lowered form of $\nabla_\nu T^{\mu\nu}$;
• the field equations on $U$: $G_{\mu\nu}(x)+\Lambda g_{\mu\nu}(x)=\kappa T_{\mu\nu}(x)$ for all $x\in U$.

Formalization targets

Goal: local energy–momentum conservation

For a smooth nondegenerate symmetric metric $g$ on an open $U\subseteq\mathbb{R}^D$, constants $G,c>0$, $\kappa=8\pi G/c^4$, any $\Lambda$, and any $T$ such that the field equations hold on $U$:

$$g^{\beta\lambda}\nabla_\lambda T_{\alpha\beta}=0\quad\text{on }U.$$

Milestones

• Symmetry of the Einstein tensor, $G_{\mu\nu}=G_{\nu\mu}$.
• Metric compatibility, $\nabla_\lambda g_{\mu\nu}=0$.
• The differential Bianchi identity $R^\mu{}_{\alpha[\beta\gamma;\varepsilon]}=0$.
• The contracted Bianchi identity, $G^{\alpha\beta}{}_{;\beta}=0$.
• The trace of the EFE, $R-\tfrac D2R+D\Lambda=\kappa T$.
• Equivalence with the trace-reversed form $R_{\mu\nu}-\tfrac2{D-2}\Lambda g_{\mu\nu}=\kappa(T_{\mu\nu}-\tfrac1{D-2}Tg_{\mu\nu})$ for $D\neq2$.
• The vacuum equations $R_{\mu\nu}=\Lambda g_{\mu\nu}/(\tfrac D2-1)$ when $T=0$, $D\neq2$.
• The cosmological term as vacuum stress–energy $T^{(\mathrm{vac})}_{\mu\nu}=-\tfrac\Lambda\kappa g_{\mu\nu}$, with $\rho_{\mathrm{vac}}=-p_{\mathrm{vac}}=\Lambda/\kappa$.
• Minkowski space $\operatorname{diag}(-1,1,1,1)$ is a vacuum solution.

Significance

Conservation of $T_{\mu\nu}$ is a consistency condition that any relativistic field equation for gravity has to satisfy; it is also the starting point for deriving the motion of matter (for dust, the geodesic equation) from the field equations alone. The trace-reversed and vacuum forms are the ones used in practice to study vacuum solutions such as Schwarzschild and Kerr, and Einstein manifolds in geometry.

All of these results are classical and fully proved in the literature. What is not yet available is a machine-checked development of the Levi-Civita curvature calculus in coordinates suitable for these statements: Mathlib currently has no Riemann or Ricci tensor of a pseudo-Riemannian metric. The mission produces that layer and the proofs on top of it.

Difficulty

The algebraic milestones (trace, trace reversal, vacuum form, vacuum energy) only need matrix algebra and the symmetry of $g$; without symmetry the identity $g^{\mu\nu}g_{\mu\nu}=D$ fails, so symmetry is essential. The analytic core is the contracted Bianchi identity: it needs the symmetry of mixed second and third partial derivatives (Schwarz's theorem on an open set), derivatives of the matrix inverse $g^{-1}$, and lengthy index bookkeeping with sums over $\operatorname{Fin} D$. Since all objects are total functions, every derivative step must be justified by differentiability on the open set $U$, not taken for granted.

Formalization scope

• Coordinates: $\mathbb{R}^D$ is represented as Fin D → ℝ; tensors are Matrix (Fin D) (Fin D) ℝ-valued functions; no manifold structure. $D$ is arbitrary, and no Lorentzian signature is imposed (the results hold for any nondegenerate symmetric metric, which includes the Lorentzian case).
• Regularity: the metric components are $C^\infty$ on the open set $U$; $T$ carries no assumptions, as the field equations determine it on $U$.
• Total-function conventions: the inverse of a singular matrix is $0$ and the derivative of a non-differentiable function is $0$; nondegeneracy on $U$ and openness of $U$ make these junk values irrelevant at points of $U$.
• Divergence is taken on the second index; for symmetric tensors such as $G$ this is the same as the first.
• Not formalized: the Newtonian limit (it rests on approximations), the Einstein–Maxwell system, and the polynomial form.
• Reusable output: coordinate Christoffel/Riemann/Ricci calculus, metric compatibility, Bianchi identities.

Selected references

• Wikipedia, Einstein field equations, revision 1374672993. https://en.wikipedia.org/w/index.php?title=Einstein_field_equations&oldid=1374672993
• C. W. Misner, K. S. Thorne, J. A. Wheeler, Gravitation, W. H. Freeman, 1973.
• S. Carroll, Spacetime and Geometry: An Introduction to General Relativity, Addison Wesley, 2004.

Motivation

The electroweak interaction is the unified description of electromagnetism and the weak nuclear force in the Standard Model of particle physics. Glashow, Salam and Weinberg shared the 1979 Nobel Prize in Physics for this unification, and its central predictions — neutral weak currents (Gargamelle, 1973) and the massive $W^\pm$ and $Z^0$ bosons (UA1/UA2, 1983) — have been confirmed experimentally. The algebraic core of the theory is short: an $\mathrm{SU}(2)\times\mathrm{U}(1)$ gauge theory whose symmetry is broken by the vacuum value of a Higgs doublet, after which the neutral gauge fields are rotated by the weak mixing angle $\theta_W$ into the photon and the $Z^0$, and the masses satisfy $m_Z = m_W/\cos\theta_W$.

This mission formalizes those tree-level algebraic facts as they are stated in the Wikipedia article Electroweak interaction (revision 1360331872), sections Formulation and Lagrangian.

Timeline (as recounted in the article). After the Wu experiment (1956) exposed parity violation, Glashow combined a chiral and an achiral symmetry and predicted a $Z$ boson; Salam and Ward (1964) proposed a massless photon and three massive gauge bosons with manually broken symmetry; Weinberg (1967) used spontaneous symmetry breaking (Englert–Brout, Higgs, Guralnik–Hagen–Kibble, 1964) and predicted rough $W$ and $Z$ masses; 't Hooft (1971) proved that spontaneously broken gauge theories are renormalizable. Neutral currents were observed in 1973 and the $W$, $Z$ in 1983.

Setting

Fix the weak isospin coupling $g>0$ and the weak hypercharge coupling $g'>0$. The gauge fields at a spacetime point, for one Lorentz component, are real numbers $W_1, W_2, W_3$ (weak isospin) and $B$ (weak hypercharge).

1. Weak mixing angle. $\theta_W = \arctan(g'/g)$, the angle of the right triangle with legs $g$, $g'$ and hypotenuse $\sqrt{g^2+g'^2}$ (the figure Weinberg's weak mixing angle in the article). The electromagnetic coupling is the altitude of that triangle, $e = gg'/\sqrt{g^2+g'^2}$.
2. Physical neutral fields. $\gamma = \cos\theta\,B + \sin\theta\,W_3$ and $Z^0 = -\sin\theta\,B + \cos\theta\,W_3$.
3. Charged fields. $W^\pm = (W_1 \mp i W_2)/\sqrt 2$.
4. Higgs sector. The Higgs field is a complex doublet $h\in\mathbb C^2$ with $|h|^2 = |h_1|^2+|h_2|^2$ and potential $V(h) = \lambda\,(|h|^2 - v^2/2)^2$. Its vacuum is $h_0 = (0, v/\sqrt2)$.
5. Covariant derivative. $D_\mu = \partial_\mu - i\tfrac{g'}{2} Y B_\mu - i \tfrac{g}{2}\sigma_j W^j_\mu$ with $\sigma_j$ the Pauli matrices. On the constant vacuum the derivative term vanishes, so $|D_\mu h_0|^2 = |M h_0|^2$ with $M = \tfrac{g'}{2}YB\,\mathbb 1 + \tfrac g2(W_1\sigma_1+W_2\sigma_2+W_3\sigma_3)$ and $Y=1$ for the Higgs.
6. Charge. $Q = T_3 + \tfrac12 Y$.
7. Masses. $m_W = gv/2$ and $m_Z = \sqrt{g^2+g'^2}\,v/2$.

Formalization targets

Goal: the gauge boson mass terms

For all real $v, W_1, W_2, W_3, B$,

$$|M h_0|^2 = m_W^2\, W^+ W^- + \tfrac12 m_Z^2 \,(Z^0)^2 ,$$

which is the mass part $m_W^2 W^+_\mu W^{-\mu} + \tfrac12 m_Z^2 Z_\mu Z^\mu$ of $\mathcal L_K$ in the article. The photon field $\gamma$ does not appear: it stays massless.

Milestones

1. The Weinberg triangle: $\cos\theta_W = g/\sqrt{g^2+g'^2}$, $\sin\theta_W = g'/\sqrt{g^2+g'^2}$.
2. $e = g\sin\theta_W = g'\cos\theta_W$.
3. $(\gamma, Z^0)$ is a rotation of $(B, W_3)$: it can be inverted and $\gamma^2+(Z^0)^2 = B^2+W_3^2$.
4. $W^- = \overline{W^+}$, $W_1 = (W^++W^-)/\sqrt2$, $W_2 = i(W^+-W^-)/\sqrt2$, $W^+W^- = (W_1^2+W_2^2)/2$.
5. $m_Z = m_W/\cos\theta_W$.
6. $h_0$ minimizes the Higgs potential, and the zero set of $V$ is the sphere $|h|^2 = v^2/2$.
7. $Q = T_3 + \tfrac12 Y$ annihilates $h_0$, and (for $v\neq0$) it is the only combination $aT_3 + b\,Y/2$, up to scale, that does.
8. The neutral-current coupling: $gT_3W_3 + g'\tfrac Y2 B = eQ\,\gamma + \frac{g}{\cos\theta_W}(T_3 - \sin^2\theta_W\,Q)\,Z^0$.

Significance

These identities are the content behind the article's statements that "the axes ... have been rotated by the angle $\theta_W$", that $m_Z = m_W/\cos\theta_W$, that $e = g\sin\theta_W = g'\cos\theta_W$, and that $\mathrm U(1)_{em}$ is unbroken because it does not couple to the Higgs. The formal library produced here (Pauli matrices, the Higgs doublet, the mixing rotation, the mass formulas) can be reused by later missions on the full electroweak Lagrangian, on the Yukawa sector, or on the custodial relation $\rho = m_W^2/(m_Z^2\cos^2\theta_W) = 1$.

All statements are classical tree-level results. None is open; the work is to formalize them.

Difficulty

The mathematics is finite-dimensional linear algebra and trigonometry. The main pitfalls are conventions: the factor $\tfrac12$ in front of the Pauli matrices, the hypercharge normalization $Q = T_3 + Y/2$ (so the Higgs has $Y=1$), and the sign conventions in the rotation matrix. The goal also requires handling complex doublets, $\sqrt 2$ factors and the inverse trigonometric definition of $\theta_W$ at the same time.

Formalization scope

All fields are real numbers at one spacetime point and for one Lorentz component; the Lorentz contraction and the kinetic (derivative) terms are not modeled. The Higgs doublet is a function Fin 2 → ℂ, and its squared norm is written out as $|h_1|^2 + |h_2|^2$ (not the sup norm of the product type). The Pauli matrices are defined explicitly. The angle is $\theta_W = \arctan(g'/g)$; with $g>0$ this agrees with the triangle. The standing convention $g, g' > 0$ is a hypothesis wherever $\theta_W$ appears. The goal is stated as an equation in $\mathbb C$ so that the product $W^+W^-$ appears exactly as in $\mathcal L_K$.

All declarations live in the namespace ElectroweakWiki.

Selected references

• Wikipedia contributors, Electroweak interaction, revision 1360331872. https://en.wikipedia.org/w/index.php?title=Electroweak_interaction&oldid=1360331872
• S. Weinberg, A Model of Leptons, Phys. Rev. Lett. 19 (1967) 1264. https://doi.org/10.1103/PhysRevLett.19.1264
• D. J. Griffiths, Introduction to Elementary Particles, Wiley, 1987.

Motivation

The Wheeler–DeWitt equation is the quantum version of the Hamiltonian constraint of general relativity. In the canonical formulation, a spacetime is described by the evolution of the metric $h_{ab}$ of a spatial slice, and Einstein's equations include a constraint: the Hamiltonian density vanishes at every point of space. Quantizing this constraint, as DeWitt did (Phys. Rev. 160, 1967), gives a second-order functional differential equation for a wavefunctional $\Psi[h]$ with no external time parameter.

Three structural facts make the equation distinctive:

• its kinetic term is built from an indefinite metric on the space of metrics, the DeWitt supermetric, so the equation is hyperbolic;
• the timelike direction of that supermetric is the local volume, which serves as an intrinsic time;
• in the limit $\hbar\to0$, a WKB ansatz turns the equation into the Einstein–Hamilton–Jacobi equation, recovering classical general relativity.

A fourth issue is not settled: consistency. In the continuum, the Poisson bracket of two Hamiltonian constraints is a combination of the momentum constraints, so imposing all constraints is consistent (Dirac's first-class condition). Any regularization of the quantum equation, a lattice for instance, must reproduce this. Generic lattice discretizations do not: the constraints become second class (Bander 1987; Dittrich 2008; Bahr–Dittrich 2009). Whether, and with which anomaly, the Hamiltonian-constraint commutators close as the lattice is refined was singled out as an open question by Loll (Living Rev. Rel. 1998, §2.12).

The first three facts are the standard entry points of quantum geometrodynamics, as reviewed by Kiefer (arXiv 0812.0295): Section 2 for the constraints and their quantization, eqs. (3)–(8), and Section 3 for the Hamilton–Jacobi equation, eq. (10), and the semiclassical approximation, eq. (11).

Setting

A spatial metric at a point is a symmetric positive-definite $3\times3$ matrix $h=(h_{ab})$. Write $\sqrt h=\sqrt{\det h}$. The DeWitt supermetric is

$$G_{abcd}(h)=\frac{h_{ac}h_{bd}+h_{ad}h_{bc}-h_{ab}h_{cd}}{2\sqrt h}.$$

It is a quadratic form $G(p,p)=G_{abcd}\,p^{ab}p^{cd}$ on symmetric momenta. Its inverse $G^{abcd}=\tfrac12\sqrt h\,(h^{ac}h^{bd}+h^{ad}h^{bc}-2h^{ab}h^{cd})$ acts on velocities.

Space is represented by a finite set $X$ of sites; this is a lattice regularization. A configuration assigns to each site $x$ a matrix $h(x)$. All nine entries are coordinates, so configuration space is $\mathbb{R}^{9|X|}$, and physical configurations are those that are symmetric and positive definite at every site. A wavefunction is a function $\Psi$ from configurations to $\mathbb{C}$. The functional derivative $\delta/\delta h_{ab}(x)$ is the partial derivative $\partial_{ab}(x)$ with respect to the coordinate $h_{ab}(x)$, with the cell volume normalized to one.

The Wheeler–DeWitt operator at site $x$, with gravitational coupling $\kappa$, cosmological constant $\Lambda$, and a supplied potential $R(h,x)$ playing the role of the spatial scalar curvature, is

$$\widehat{\mathcal H}_x\Psi=-2\kappa\hbar^2\,G_{abcd}(h(x))\,\partial_{ab}(x)\,\partial_{cd}(x)\Psi-\frac{\sqrt{h(x)}}{2\kappa}\,(R-2\Lambda)\,\Psi .$$

Write $V_z(h)=-\tfrac{\sqrt{h(z)}}{2\kappa}(R(h,z)-2\Lambda)$ for the potential at site $z$. On the classical phase space of pairs $(h,p)$, with $p^{ab}(z)$ conjugate to $h_{ab}(z)$, the lattice constraints are

$$H_z(h,p)=2\kappa\,G_{abcd}(h(z))\,p^{ab}(z)\,p^{cd}(z)+V_z(h),$$

with the canonical Poisson bracket. They are first class if each bracket $\{H_x,H_y\}$ vanishes wherever all constraints vanish.

The supermetric stands to the left of both derivatives (Kiefer, eq. (7), vacuum case; the coupling is $\kappa=8\pi G$, so $2\kappa=16\pi G$ as in Kiefer's eq. (10)). The kinetic term involves only derivatives at the same site, as in the continuum; it is ultralocal. The potential may couple neighbouring sites.

Formalization targets

Milestones: geometry of the supermetric

• Signature. $G(p,p)>0$ for every nonzero symmetric $p$ with $\operatorname{tr}(hp)=0$, and $G(h^{-1},h^{-1})<0$.
• Inverse. $G^{abcd}G_{cdef}\,p^{ef}=p^{ab}$ for symmetric $p$.
• Intrinsic time. With $h=s\hat h$, $\det\hat h=1$ and $\tau=\sqrt{32/3}\,s^{3/4}$, the velocity form of the supermetric is $-d\tau^2+\tfrac{3}{32}\tau^2\operatorname{tr}\big((\hat h^{-1}d\hat h)^2\big)$.

Milestone: the conformal sector

For $\Psi=f(\sqrt{\det h(x_0)})$ with $f\in C^2$ and $v=\sqrt{\det h(x_0)}$:

$$G_{abcd}\,\partial_{ab}\partial_{cd}\Psi=-\tfrac38\,\big(vf''(v)+7f'(v)\big).$$

Milestone: the semiclassical limit

For every real $C^2$ function $S$ and $\hbar\neq0$:

$$e^{-iS/\hbar}\,\widehat{\mathcal H}_x\,e^{iS/\hbar}=2\kappa\,G_{abcd}\,\partial_{ab}S\,\partial_{cd}S-\frac{\sqrt h}{2\kappa}(R-2\Lambda)\;-\;i\hbar\,2\kappa\,G_{abcd}\,\partial_{ab}\partial_{cd}S .$$

The $\hbar$-independent part is the Einstein–Hamilton–Jacobi functional of Kiefer's eq. (10), Hamiltonian part, with $S$ the eikonal of the WKB form (11) (amplitude $C=1$). This is the weakest statement exhibiting the classical limit, and it holds for every potential.

Milestone: the lattice commutator

For $\Psi\in C^4$ and sites $x\neq y$:

$$[\widehat{\mathcal H}_x,\widehat{\mathcal H}_y]\Psi=-2\kappa\hbar^2\Big(G_{abcd}(h(x))\big(2\,\partial^{x}_{ab}V_y\,\partial^{x}_{cd}\Psi+\partial^{x}_{ab}\partial^{x}_{cd}V_y\,\Psi\big)-(x\leftrightarrow y)\Big).$$

Milestone: the strong-coupling case

If every $V_z$ depends only on $h(z)$, then $\{H_x,H_y\}=0$ identically.

Goal: lattice constraints are second class

If the symmetric part of $\partial V_y/\partial h_{ab}(x)$ is nonzero at a physical $h$, for some $x\neq y$, then there is a point of the constraint surface over $h$ at which $\{H_x,H_y\}\neq0$.

Every finite-difference curvature couples neighbouring sites, so the goal applies to every such discretization. It is the weakest statement that the discretized constraint algebra is inconsistent, and it holds uniformly in the discretization.

Stronger targets

• The limit form $\hbar\to0$, as a Tendsto statement.
• The same results with the Laplace–Beltrami ordering of the kinetic term on the six-dimensional fibre of symmetric matrices, and an explicit formula for the difference between the two orderings.
• A potential realized as the scalar curvature of a smooth metric field on a coordinate patch, computed from Christoffel symbols, with its scaling law $R[sh]=R[h]/s$ for constant $s>0$.
• The momentum constraints (Kiefer, eq. (8)).
• Open as far as the drafter could determine. Fix a cubic lattice of spacing $\varepsilon$ and a standard finite-difference scalar curvature. Determine the limit $\varepsilon\to0$ of the suitably rescaled commutator $[\widehat{\mathcal H}_x,\widehat{\mathcal H}_y]$, and decide whether it reproduces the continuum Dirac algebra $\{H(x),H(y)\}=(h^{ab}H_b(x)+h^{ab}H_b(y))\,\partial_a\delta(x,y)$ or leaves an anomaly. Give the anomaly explicitly if there is one. This is the metric-variable analogue of the question Loll raised.

Significance

The signature theorem is the mathematical content behind two physical facts: the hyperbolic character of the Wheeler–DeWitt equation, and the instability of the conformal mode (the "conformal factor problem" of Euclidean quantum gravity). DeWitt's cone form identifies the local volume as an intrinsic clock. On this rests the reading of the equation as a wave equation in superspace, with $\tau$ as time. The conformal-sector reduction shows explicitly how the timelike direction appears in the operator, with the sign opposite to the traceless modes. The WKB identity is the precise sense in which the quantum constraint contains classical general relativity: its leading order is the Hamilton–Jacobi form of the Einstein constraint (Peres 1962; Kiefer, eq. (10)), and its next order is the one used in derivations of the Schrödinger equation from quantum gravity.

All of these are classical computations. The drafter knows of no machine-checked version. A formalization fixes conventions that the literature handles loosely:

• the normalization of $G_{abcd}$;
• the treatment of symmetric versus independent metric components;
• the ordering of operators.

It does so with genuine derivatives in place of formal symbols.

The constraint-algebra part turns a phenomenon described qualitatively in the literature into a theorem with exact hypotheses. Lattice constraints are second class as soon as curvature couples sites, and the quantum commutator is given in closed form. It also isolates precisely what a consistent discretization would have to cancel. The continuum-limit target addresses an open question in canonical quantum gravity.

Difficulty

The supermetric statements are finite-dimensional, but none is a single computation. The signature requires a positivity argument for $\operatorname{tr}\big((h^{1/2}ph^{1/2})^2\big)$ on an $h$-traceless subspace. The cone form requires separating the trace part of a velocity in a non-orthonormal frame.

The analytic targets require second derivatives of compositions through the determinant and the matrix inverse. The derivative of $\det$ at $h$ in the direction of a single entry is $\det h\,(h^{-1})_{ba}$, and the derivative of $h^{-1}$ produces terms like $h^{-1}E_{ab}h^{-1}$; a sign or index slip changes the constant $7$. Treating the nine entries as independent coordinates, rather than the six symmetric ones, changes the numerical coefficients; the conventions below fix this.

For the constraint algebra, the quantum commutator involves up to fourth derivatives of $\Psi$, which cancel only by the symmetry of mixed partials. The classical goal needs a point on the constraint surface where the bracket is nonzero. Each constraint fixes the value of an indefinite quadratic form in the momenta, and the bracket is linear in them, so the proof must use the Lorentzian signature to show that the bracket is not constant on that quadric.

A naive formalization that replaces $\partial_{ab}$ by an abstract linear map reduces every target to ring arithmetic, and is ruled out by the definitions.

Formalization scope

• Definitions (module Def_WheelerDeWittSuperspace):
  • metric components as Fin 3 → Fin 3 → ℝ, so that configuration space X → Fin 3 → Fin 3 → ℝ with X a Fintype is a normed space;
  • matrices via Matrix.of;
  • $\partial_{ab}(x)$ as fderiv ℝ Ψ h applied to the coordinate direction of $h_{ab}(x)$;
  • $\sqrt h$ as Real.sqrt of the determinant;
  • the operator with the supermetric on the left.
• Conventions:
  • all nine metric entries are independent coordinates, and statements that need symmetry assume it at the evaluation point (Matrix.PosDef includes symmetry);
  • lattice cell volume equal to $1$;
  • vacuum (no matter term).
• Not formalized; the potential is an interface: the potential $R$ is supplied data on configurations and sites, and every target holds for all such $R$. The continuum limit of the lattice, a Hilbert-space domain for $\widehat{\mathcal H}$, regularization of coincident derivatives in the continuum, and existence of solutions are outside the mission and must not be inferred from it.
• Trivial cases to rule out:
  • the WKB milestone must hold for every $C^2$ phase $S$, not only for $\Psi=0$ or constant $S$;
  • the goal must exhibit a point on the full constraint surface, with every $H_z$ vanishing, not merely a point where the bracket is nonzero;
  • the dependence hypothesis is on the symmetric part, because antisymmetric metric directions are invisible to $G$.
• Phase-space convention: the bracket is the canonical one on all nine components per site. The symmetric reduction changes off-diagonal normalizations but not the first-class property.
• Welcome contributions: the stronger targets, a matter field with its energy density, and minisuperspace reductions (e.g. homogeneous isotropic metrics $h=a^2\delta$) derived from the operator here rather than postulated.

Selected references

• B. S. DeWitt, Quantum Theory of Gravity. I. The Canonical Theory, Phys. Rev. 160 (1967), 1113–1148. https://doi.org/10.1103/PhysRev.160.1113
• C. Kiefer, Quantum Geometrodynamics: whence, whither?, Gen. Relativ. Gravit. 41 (2009), 877–901. https://arxiv.org/abs/0812.0295
• A. Peres, On Cauchy's problem in general relativity – II, Nuovo Cimento 26 (1962), 53–62. https://doi.org/10.1007/BF02754342
• C. Kiefer, Quantum Gravity, 3rd ed., Oxford University Press (2012), Chapter 5. https://doi.org/10.1093/acprof:oso/9780199585205.001.0001
• R. Loll, Discrete approaches to quantum gravity in four dimensions, Living Rev. Relativ. 1 (1998), 13, Section 2.12. https://arxiv.org/abs/gr-qc/9805049
• R. Loll, On the diffeomorphism-commutators of lattice quantum gravity, Class. Quantum Grav. 15 (1998), 799–809. https://arxiv.org/abs/gr-qc/9708025
• P. Renteln, Some results of SU(2) spinorial lattice gravity, Class. Quantum Grav. 7 (1990), 493–502.
• M. Bander, Hamiltonian lattice gravity. Deformations of discrete manifolds, Phys. Rev. D 36 (1987), 2297. https://doi.org/10.1103/PhysRevD.36.2297
• R. Gambini, J. Pullin, Canonical quantization of general relativity in discrete space-times, 2002. https://arxiv.org/abs/gr-qc/0206055
• B. Dittrich, Diffeomorphism symmetry in quantum gravity models, 2008. https://arxiv.org/abs/0810.3594
• B. Bahr, B. Dittrich, (Broken) Gauge symmetries and constraints in Regge calculus, 2009. https://arxiv.org/abs/0905.1670
• C. J. Isham, Some quantum field theory aspects of the superspace quantization of general relativity, Proc. R. Soc. Lond. A 351 (1976), 209.
• K. Pilati, Strong-coupling quantum gravity. I. Solution in a particular gauge, Phys. Rev. D 26 (1982), 2645. https://doi.org/10.1103/PhysRevD.26.2645
• H. W. Hamber, R. M. Williams, Discrete Wheeler–DeWitt equation, 2011. https://arxiv.org/abs/1109.2530