Encyclopedia Gravity Gravity Seven Gaps Hypersurface Deformation Bracket Const Mul Right

ARTICLE 4 claims 3 theorems 1 model

Gravity Seven Gaps Hypersurface Deformation Bracket Const Mul Right

A machine-checked proof establishes that the Poisson bracket of the lattice wave field obeys a constant-multiplication rule, a small but necessary step toward a discrete theory of gravity.

Verify this page

A rule for the bracket

In classical mechanics, the Poisson bracket measures how two quantities change together in phase space. The declaration bracket_const_mul_right establishes a specific algebraic property of the bracket defined for a lattice wave field: pulling a constant out of the second argument of the bracket is valid. Concretely, for any constant c and any two differentiable functions F and G on the phase space, the bracket of F with c times G equals c times the bracket of F with G. This is a linearity rule, one of the standard identities that any well-behaved bracket must satisfy.

The proof is not a formal assumption. It is a theorem in the machine-checked library of formal theorems, derived from the definition of the bracket as a sum over lattice sites of partial derivatives. The rule holds under an explicit hypothesis: both functions must be differentiable at the point where the bracket is evaluated. This differentiability condition is not an axiom; it is a premise of the theorem, discharged automatically for the quadratic generators used elsewhere in the framework. The statement is unconditional for those generators, because their differentiability is proved separately.

This rule matters because it is one of the building blocks for the larger goal of the Seven-Gaps campaign: showing that the discrete constraint algebra of gravity closes consistently. The bracket must behave like its continuum counterpart, the Dirac bracket of general relativity, before the discrete theory can be taken seriously as a route to quantum gravity. Linearity under constant multiplication is a prerequisite for the more substantial closure relations, such as the bracket of two Hamiltonian generators producing a momentum generator, which the library also proves.

What the declaration does not claim is just as important. It does not assert that the bracket satisfies the Jacobi identity, the deep consistency condition for a Poisson structure. That remains an open target. It does not claim that the full Dirac algebra of general relativity is recovered on the lattice; only a linearized, one-dimensional polarization with a frozen structure function is treated here. And it does not claim that the bracket is defined for all functions: the differentiability hypothesis is real, and for non-differentiable observables the underlying derivative returns a junk value of zero, so bracket statements about such functions are meaningless.

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
THEOREM differentiable_Dgen · differentiable_Ham · IndisputableMonolith/Gravity/SevenGaps/HypersurfaceDeformation.lean
differentiable_Dgen · IndisputableMonolith/Gravity/SevenGaps/HypersurfaceDeformation.lean:443 
/-- THEOREM. `Dgen a` is (unconditionally) differentiable. -/
theorem differentiable_Dgen (a : ZMod n) : Differentiable ℝ (Dgen (n := n) a) :=
  fun x => (hasFDerivAt_Dgen a x).differentiableAt
differentiable_Ham · IndisputableMonolith/Gravity/SevenGaps/HypersurfaceDeformation.lean:481 
/-- THEOREM. `Ham N` is (unconditionally) differentiable. -/
theorem differentiable_Ham (N : ZMod n → ℝ) : Differentiable ℝ (Ham (n := n) N) :=
  fun x => (hasFDerivAt_Ham N x).differentiableAt
MODEL bracket · IndisputableMonolith/Gravity/SevenGaps/HypersurfaceDeformation.lean
bracket · IndisputableMonolith/Gravity/SevenGaps/HypersurfaceDeformation.lean:136 
/-- MODEL. The Poisson bracket
`{F, G}(x) = sum_i (dF/dq_i * dG/dpi_i - dF/dpi_i * dG/dq_i)`.
Honest but total: for observables not differentiable at `x` the `fderiv` junk
value `0` enters, which is why the general structure theorems below carry
explicit `DifferentiableAt` hypotheses. -/
def bracket (F G : PhaseSpace n → ℝ) (x : PhaseSpace n) : ℝ :=
  ∑ i : ZMod n, (pderivQ F i x * pderivP G i x - pderivP F i x * pderivQ G i x)

What this page does not claim

The Jacobi identity for the bracket is not proved here. The full Dirac algebra of general relativity is not recovered on this one-dimensional lattice. The bracket is not defined for non-differentiable functions, where the derivative returns a junk value.

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