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

ARTICLE 2 claims 2 theorems

Gravity Seven Gaps Hypersurface Deformation Bracket Dgen Sym Dgen Sym

In a discrete model of gravity, the machine-checked library proves that two translation generators always commute, a first step toward a full constraint algebra.

Verify this page

A discrete translation symmetry

In the Hamiltonian formulation of general relativity, the theory's dynamics are encoded not in a single equation but in a set of constraints. These constraints must be consistent: if you apply one and then another, the order should not matter for the final result. This consistency is expressed by the Poisson bracket, a mathematical operation that measures how two quantities change together. When the bracket of two constraints vanishes, they are said to commute, meaning they can be applied in any sequence without conflict.

The Recognition Science framework's machine-checked library of formal theorems, a collection of proofs verified by a computer, contains a result about a specific discrete model. This model places a wave field on a ring of n points, with a configuration value and a conjugate momentum at each site. The declaration bracket_DgenSym_DgenSym proves a fact about two of the model's constraint generators, called DgenSym. These generators represent spatial translations, shifting the field by a fixed number of sites. The theorem states that the bracket of any two such translation generators is exactly zero, for any lattice size and any shift amount. This means the translation sector is abelian, closing sharply: the generators commute perfectly, with no extra terms needed.

This result is the first rung of a larger program. In the continuum theory of gravity, the constraints form the hypersurface-deformation algebra, a structure that dictates how the geometry evolves. The framework's library proves this discrete translation closure as a foundation, but it does not claim to have recovered the full algebra. The bracket of two Hamiltonian constraints, which generate time evolution, is proved separately to close on a momentum generator, but only in a point-split form. The full Dirac algebra, including the Jacobi identity and the recovery of the continuum limit as the lattice spacing goes to zero, remains an open target. The framework also does not claim that this discrete model is full gravity; it is one polarization of a linearized field, with no metric degree of freedom.

What the theorem changes is the starting point. It shows that a discrete, machine-checked foundation can reproduce the simplest part of the constraint algebra exactly. This gives a concrete base from which the harder, open questions about Hamiltonian closure and the continuum limit can be attacked. The proof is unconditional and axiom-clean, meaning it relies only on the standard rules of logic, not on any special assumptions about the framework.

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
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

This result does not prove the full Dirac algebra or its continuum limit. This model does not include a metric degree of freedom and is not full gravity. The Jacobi identity for the bracket is not proved here.

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