Gravity Seven Gaps Hypersurface Deformation

The discrete constraint algebra

General relativity, in its canonical Hamiltonian form due to Arnowitt, Deser, and Misner (ADM), describes how a spatial slice evolves in time. The theory's consistency rests on a set of constraint equations that must close under the Poisson bracket: the bracket of two Hamiltonian constraints must be a momentum constraint, and the bracket of a momentum constraint with a Hamiltonian must be a Hamiltonian. This closure is the hypersurface deformation algebra, and it is the backbone of the Dirac constraint program. The framework's library, a machine-checked collection of formal theorems, has now built the first theorem-grade layer of this program for a discrete system.

The system is a scalar field on a one-dimensional periodic lattice with n sites, described by a configuration q and conjugate momentum pi. This is one polarization of the linearized transverse-traceless field, and it is offered as a first rung, not as full gravity: there is no metric degree of freedom, so the structure function that encodes spatial geometry is frozen to 1. On this phase space, the library defines a Poisson bracket as a sum over sites of derivatives with respect to q and pi, and it defines discrete generators for the momentum constraint D and the Hamiltonian constraint H. The bracket is built from honest derivatives, with no axiomatized structure.

The central results are closure theorems, each proved from the definitions. The momentum sector closes sharply: the bracket of two momentum generators vanishes identically, not merely up to combinations of shift generators. The bracket of two Hamiltonian generators closes on a momentum-type generator whose smearing is the discrete Wronskian of the two lapses: {H[N], H[M]} = sum_j (N_j M_{j+1} - M_j N_{j+1}) * pi_{j+1} (q_{j+1} - q_j). In the continuum limit, this becomes the Dirac relation with unit structure function. The mixed bracket {D_a, H[N]} is where the subtlety lies. For a forward-difference momentum generator, it does not commute with the Hamiltonian; the exact anomaly is a second-order lattice artifact, quadratic in the differences of the field gradient and momentum, which vanishes on shift-invariant configurations. The symmetric-difference generator, by contrast, satisfies an exact advection relation: {Dsym_a, H[N]} = (1/2) * sum_j (N(j+a) - N(j)) * (pi_j pi_{j+a} + d_j d_{j+a}), and with constant lapse the bracket vanishes exactly, restoring translation invariance.

These results establish that the discrete constraint algebra closes on this rung, with the exact form of the closure anomaly identified. The framework's library proves these identities with no axioms beyond the standard three, and no sorry. The Jacobi identity for the bracket remains open, as does the full recovery of the Dirac algebra in the continuum limit. The Hojman-Kuchar-Teitelboim rigidity statement, which would force the Einstein-Hilbert form from the algebra, is stated but not inhabited: the concrete generators realize the momentum-momentum relation exactly but the mixed and Hamiltonian relations only in point-split form, and that gap is the discrete-closure frontier. The significance is that a discrete gravity program now has a kernel-checked foundation for its constraint algebra, with the precise obstruction to translation invariance made explicit and provable.

/-- THEOREM (momentum sector closes, sharp form). `{D_a, D_b} = 0` for all
lattice displacements `a, b` and every phase-space point. Derived by explicit
computation: after the Kronecker collapse the eight monomial sums cancel in
pairs under the reindexings `j ↦ j + a` and `j ↦ j + b`. -/
theorem bracket_Dgen_Dgen (a b : ZMod n) (x : PhaseSpace n) :
    bracket (Dgen a) (Dgen b) x = 0 := by
  simp only [bracket, pderivQ_Dgen, pderivP_Dgen]
  have h1 : (∑ j : ZMod n, x.2 (j - a) * x.1 (j + b))
      = ∑ j : ZMod n, x.2 j * x.1 (j + (a + b)) := by
    refine sum_reindex a (fun k => x.2 (k - a) * x.1 (k + b)) _ fun j => ?_
    have e1 : j + a - a = j := by ring
    have e2 : j + a + b = j + (a + b) := by ring
    simp only [e1, e2]
  have h2 : (∑ j : ZMod n, x.2 (j - a) * x.1 j)
      = ∑ j : ZMod n, x.2 j * x.1 (j + a) := by
    refine sum_reindex a (fun k => x.2 (k - a) * x.1 k) _ fun j => ?_
    have e1 : j + a - a = j := by ring
    simp only [e1]
  have h3 : (∑ j : ZMod n, x.2 (j - b) * x.1 (j + a))
      = ∑ j : ZMod n, x.2 j * x.1 (j + (a + b)) := by
    refine sum_reindex b (fun k => x.2 (k - b) * x.1 (k + a)) _ fun j => ?_
    have e1 : j + b - b = j := by ring
    have e2 : j + b + a = j + (a + b) := by ring
    simp only [e1, e2]
  have h4 : (∑ j : ZMod n, x.2 (j - b) * x.1 j)
      = ∑ j : ZMod n, x.2 j * x.1 (j + b) := by
    refine sum_reindex b (fun k => x.2 (k - b) * x.1 k) _ fun j => ?_
    have e1 : j + b - b = j := by ring
    simp only [e1]
  have decomp : (∑ j : ZMod n, ((x.2 (j - a) - x.2 j) * (x.1 (j + b) - x.1 j)
      - (x.1 (j + a) - x.1 j) * (x.2 (j - b) - x.2 j)))
      = ((∑ j : ZMod n, x.2 (j - a) * x.1 (j + b))
          - (∑ j : ZMod n, x.2 (j - a) * x.1 j)
          - (∑ j : ZMod n, x.2 j * x.1 (j + b)))
        - ((∑ j : ZMod n, x.2 (j - b) * x.1 (j + a))
          - (∑ j : ZMod n, x.2 (j - b) * x.1 j)
          - (∑ j : ZMod n, x.2 j * x.1 (j + a))) := by
    simp only [← Finset.sum_sub_distrib]
    exact Finset.sum_congr rfl fun j _ => by ring
  rw [decomp, h1, h2, h3, h4]
  ring

/-- THEOREM (discrete hypersurface-deformation relation).
`{H[N], H[M]} = sum_j (N_j M_{j+1} - M_j N_{j+1}) * pi_{j+1} (q_{j+1} - q_j)`.
The bracket of two Hamiltonian deformations is a D-type (momentum) generator:
a point-split momentum density `pi_{j+1} (q_{j+1} - q_j)` smeared by the
discrete Wronskian `N_j M_{j+1} - M_j N_{j+1}` of the two lapses. In the
continuum limit the Wronskian tends to `(N M' - M N') dx` and the density to
`pi q'`, which is the Dirac algebra relation `{H(N), H(M)} = D(N M' - M N')`;
the structure function (the inverse spatial metric in full gravity) is frozen
to 1 on this flat scalar rung. Antisymmetric in `N, M` by inspection, and it
vanishes identically for `N = M`. -/
theorem bracket_Ham_Ham (N M : ZMod n → ℝ) (x : PhaseSpace n) :
    bracket (Ham N) (Ham M) x
      = ∑ j : ZMod n, (N j * M (j + 1) - M j * N (j + 1))
          * (x.2 (j + 1) * (x.1 (j + 1) - x.1 j)) := by
  simp only [bracket, pderivQ_Ham, pderivP_Ham]
  have step1 : (∑ j : ZMod n,
      ((N (j - 1) * (x.1 j - x.1 (j - 1)) - N j * (x.1 (j + 1) - x.1 j)) * (M j * x.2 j)
        - N j * x.2 j
          * (M (j - 1) * (x.1 j - x.1 (j - 1)) - M j * (x.1 (j + 1) - x.1 j))))
      = ∑ j : ZMod n,
          (N (j - 1) * M j - M (j - 1) * N j) * (x.2 j * (x.1 j - x.1 (j - 1))) :=
    Finset.sum_congr rfl fun j _ => by ring
  rw [step1]
  refine sum_reindex 1
    (fun k => (N (k - 1) * M k - M (k - 1) * N k) * (x.2 k * (x.1 k - x.1 (k - 1)))) _
    fun j => ?_
  have e1 : j + 1 - 1 = j := by ring
  simp only [e1]

/-- THEOREM. Constant lapse: the symmetric-difference momentum generator
commutes exactly with the Hamiltonian, `{Dsym_a, H[1]} = 0` (exact discrete
translation invariance). -/
theorem bracket_DgenSym_Ham_one (a : ZMod n) (x : PhaseSpace n) :
    bracket (DgenSym a) (Ham (fun _ => 1)) x = 0 := by
  rw [bracket_DgenSym_Ham]
  simp

/-- THEOREM. `{H[1], Dsym_a} = 0` (the flipped orientation, via antisymmetry). -/
theorem bracket_Ham_one_DgenSym (a : ZMod n) (x : PhaseSpace n) :
    bracket (Ham (fun _ => 1)) (DgenSym a) x = 0 := by
  rw [bracket_antisymm, bracket_DgenSym_Ham_one, neg_zero]

What this page does not claim

This module does not establish full gravity, as there is no metric degree of freedom on this rung. This module does not prove the Jacobi identity for the bracket. This module does not recover the full Dirac algebra or the HKT rigidity theorem in the continuum limit.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Gravity/SevenGaps/HypersurfaceDeformation.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: