Encyclopedia Gravity Gravity Seven Gaps Hypersurface Deformation Bracket Ham One Dgen Sym

ARTICLE 3 claims 3 theorems

Gravity Seven Gaps Hypersurface Deformation Bracket Ham One Dgen Sym

In the framework's discrete model of gravity, one carefully chosen way of writing the momentum constraint preserves exact translation symmetry, while a naive version breaks it.

Verify this page

The translation symmetry

In classical mechanics, a Poisson bracket measures how two quantities change with respect to each other on a phase space. The framework's library of formal theorems builds a finite-dimensional version of this on a periodic lattice, a ring of n sites where each site carries a field value q and a conjugate momentum pi. The bracket is defined as a sum over sites of products of partial derivatives, and it is a genuine mathematical object, not an axiom. The declaration bracket_Ham_one_DgenSym states a theorem about two specific generators: Ham, the Hamiltonian constraint with a constant lapse function, and DgenSym, the momentum constraint written with a symmetric difference. The theorem proves that the bracket of these two generators vanishes identically, meaning they commute exactly on the lattice.

The result is not trivial, because a naive forward-difference version of the momentum generator does not commute with the Hamiltonian. That naive version, called Dgen, produces a nonzero bracket, an explicit second-order lattice artifact that vanishes only on shift-invariant configurations and in the continuum limit. The symmetric version avoids this obstruction. Its bracket with the Hamiltonian equals a point-split smearing of the Hamiltonian density by the lattice derivative of the lapse, and when the lapse is constant, that expression sums to zero. The theorem bracket_Ham_one_DgenSym is the corollary that makes this exact, and it is proved in the machine-checked library with no unproved assumptions.

What the declaration does not claim is as important as what it proves. It does not establish the full Dirac algebra of hypersurface deformations, the algebraic structure that underlies general relativity's constraints. The library states but does not prove the Hojman-Kuchar-Teitelboim rigidity target, which would force the Einstein-Hilbert form from the deformation algebra. The Jacobi identity for the bracket remains open, and the recovery of the continuum Dirac algebra in the limit of zero lattice spacing is also unproved. The theorem is one rung, not the whole ladder.

For a reader, the practical takeaway is that discretization choices matter. A symmetric difference preserves a symmetry that a forward difference breaks, and the framework's library can certify that fact with a formal proof. This is a concrete lesson in how numerical methods can respect or violate the underlying physics.

THEOREM bracket_Ham_one_DgenSym · IndisputableMonolith/Gravity/SevenGaps/HypersurfaceDeformation.lean
bracket_Ham_one_DgenSym · IndisputableMonolith/Gravity/SevenGaps/HypersurfaceDeformation.lean:866 
/-- 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]
THEOREM bracket_Dgen_Dgen · IndisputableMonolith/Gravity/SevenGaps/HypersurfaceDeformation.lean
bracket_Dgen_Dgen · IndisputableMonolith/Gravity/SevenGaps/HypersurfaceDeformation.lean:580 
/-- 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 bracket_DgenSym_DgenSym · IndisputableMonolith/Gravity/SevenGaps/HypersurfaceDeformation.lean
bracket_DgenSym_DgenSym · IndisputableMonolith/Gravity/SevenGaps/HypersurfaceDeformation.lean:622 
/-- THEOREM (momentum sector closes, symmetric discretization).
`{Dsym_a, Dsym_b} = 0`. -/
theorem bracket_DgenSym_DgenSym (a b : ZMod n) (x : PhaseSpace n) :
    bracket (DgenSym a) (DgenSym b) x = 0 := by
  simp only [bracket, pderivQ_DgenSym, pderivP_DgenSym]
  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 - 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 h3 : (∑ j : ZMod n, x.2 (j + a) * x.1 (j + b))
      = ∑ j : ZMod n, x.2 j * x.1 (j + (b - a)) := 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 + (b - a) := by ring
    simp only [e1, e2]
  have h4 : (∑ 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 h5 : (∑ 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 h6 : (∑ 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 h7 : (∑ j : ZMod n, x.2 (j - b) * x.1 (j - a))
      = ∑ j : ZMod n, x.2 j * x.1 (j + (b - a)) := 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 + (b - a) := by ring
    simp only [e1, e2]
  have h8 : (∑ 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 decomp : (∑ j : ZMod n,
      ((x.2 (j - a) - x.2 (j + a)) / 2 * ((x.1 (j + b) - x.1 (j - b)) / 2)
        - (x.1 (j + a) - x.1 (j - a)) / 2 * ((x.2 (j - b) - x.2 (j + b)) / 2)))
      = (((∑ j : ZMod n, x.2 (j - a) * x.1 (j + b))
          - (∑ j : ZMod n, x.2 (j - a) * x.1 (j - b))
          - (∑ j : ZMod n, x.2 (j + a) * x.1 (j + b))
          + (∑ j : ZMod n, x.2 (j + a) * 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 - a))
          - (∑ j : ZMod n, x.2 (j + b) * x.1 (j + a))
          + (∑ j : ZMod n, x.2 (j + b) * x.1 (j - a)))) / 4 := by
    simp only [← Finset.sum_sub_distrib, ← Finset.sum_add_distrib, Finset.sum_div]
    exact Finset.sum_congr rfl fun j _ => by ring
  rw [decomp, h1, h2, h3, h4, h5, h6, h7, h8]
  ring

What this page does not claim

The full Dirac algebra of hypersurface deformations is not recovered. The Jacobi identity for the bracket is not proved. The continuum limit of the discrete bracket is not established.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND