Encyclopedia Gravity Gravity Seven Gaps Hypersurface Deformation Bracket Const Mul Left

ARTICLE 2 claims 2 theorems

Gravity Seven Gaps Hypersurface Deformation Bracket Const Mul Left

A machine-checked theorem says that in a discrete model of gravity's constraint algebra, pulling a constant out of a Poisson bracket is always legitimate, provided the functions involved are differentiable.

Verify this page

The bracket's scaling rule

In classical mechanics, the Poisson bracket measures how two quantities change together under time evolution. The Recognition Science framework has built a discrete, finite-dimensional version of this bracket for a lattice model of gravity's constraint algebra. The declaration bracket_const_mul_left is a theorem in that setting: it states that for any real constant c and any two functions F and G on the phase space, the bracket of c·F with G equals c times the bracket of F with G. The proof is axiom-clean, meaning it relies only on the standard logical axioms of the machine-checked library, with no additional assumptions.

The theorem is not unconditional. It requires that F be differentiable at the point where the bracket is evaluated. This is a technical but important condition: the bracket is defined using derivatives, so if F is not differentiable, the statement simply does not apply. The same condition appears in the companion theorem bracket_const_mul_right, which handles pulling a constant out of the second argument. Together they form the bilinearity of the bracket in each slot separately, a property any reasonable bracket should have.

What this theorem does not claim is broader significance for gravity itself. The phase space here is one polarization of a linearized field on a one-dimensional periodic lattice, not full spacetime. There is no metric degree of freedom, and the continuum structure function is frozen to 1. The theorem is a technical lemma about the discrete bracket, not a statement about the physical content of general relativity. It is a building block for the closure relations that the framework proves for its constraint generators, but it does not by itself say anything about whether those generators close correctly.

The value of this theorem is that it makes the discrete bracket well-behaved enough to support further proofs. Without it, every calculation involving a constant multiple would require re-deriving the derivative from scratch. With it, the framework can move on to the more substantive results: the momentum-sector closure, the exact advection relation for the symmetric-difference generator, and the discrete hypersurface-deformation relation between two Hamiltonian constraints. Those are the results that carry physical meaning; this one is the plumbing that makes them possible.

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

What this page does not claim

The theorem does not claim anything about full gravity, since the phase space is a linearized one-dimensional lattice with no metric degree of freedom. The theorem does not claim that the bracket is bilinear without differentiability hypotheses. The theorem does not claim that the constraint generators close correctly; that is established by separate closure theorems.

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