Gravity Seven Gaps Hypersurface Deformation Bracket Coord P Coord P

A basic bracket relation

In classical mechanics, the Poisson bracket measures how two quantities change together in a phase space. For a simple system with one position coordinate q and one momentum coordinate p, the bracket {q, p} equals 1, while {q, q} and {p, p} both equal 0. These relations encode the fundamental independence of position and momentum: knowing one does not determine the other.

The Recognition Science declaration bracket_coordP_coordP establishes the analogous statement for a discrete model: the bracket of a momentum coordinate with itself vanishes identically. In this model, the phase space consists of a periodic lattice with n sites, where each site carries a field value q and a conjugate momentum pi. The bracket is defined as a sum over all sites of products of partial derivatives, implemented using Fréchet derivatives.

This result is part of a larger program to build a discrete version of the ADM constraint algebra from general relativity. Alongside the companion theorem bracket_coordQ_coordQ, which shows the bracket of a position coordinate with itself also vanishes, and bracket_coordQ_coordP, which gives the value 1 when the sites match and 0 otherwise, the three relations together confirm that the lattice coordinates form a canonical set. The theorems are unconditional and axiom-clean, meaning they hold without extra hypotheses.

What this declaration does not claim is just as important. It does not assert anything about the full gravitational field, since this model has no metric degree of freedom. It does not prove the Jacobi identity for the bracket, which remains an open problem for non-polynomial observables. And it does not recover the full Dirac algebra in the continuum limit, a target that remains open.

/-- THEOREM. The bracket of an observable with itself vanishes. -/
theorem bracket_self (F : PhaseSpace n → ℝ) (x : PhaseSpace n) :
    bracket F F x = 0 := by
  have h := bracket_antisymm F F x
  linarith

/-- THEOREM. The bracket of an observable with itself vanishes. -/
theorem bracket_self (F : PhaseSpace n → ℝ) (x : PhaseSpace n) :
    bracket F F x = 0 := by
  have h := bracket_antisymm F F x
  linarith

/-- THEOREM. Canonical relation `{q_k, pi_l} = delta_{kl}`. -/
theorem bracket_coordQ_coordP (k l : ZMod n) (x : PhaseSpace n) :
    bracket (fun y : PhaseSpace n => y.1 k) (fun y : PhaseSpace n => y.2 l) x
      = if k = l then (1 : ℝ) else 0 := by
  have hQ : ∀ i : ZMod n, pderivQ (fun y : PhaseSpace n => y.1 k) i x
      = if k = i then (1 : ℝ) else 0 := by
    intro i
    rw [pderivQ, (hasFDerivAt_coord_fst k x).fderiv]
    simp [coordQ, Pi.single_apply]
  have hP0 : ∀ i : ZMod n, pderivP (fun y : PhaseSpace n => y.1 k) i x = 0 := by
    intro i
    rw [pderivP, (hasFDerivAt_coord_fst k x).fderiv]
    simp [coordQ]
  have hP : ∀ i : ZMod n, pderivP (fun y : PhaseSpace n => y.2 l) i x
      = if l = i then (1 : ℝ) else 0 := by
    intro i
    rw [pderivP, (hasFDerivAt_coord_snd l x).fderiv]
    simp [coordP, Pi.single_apply]
  have hQ0 : ∀ i : ZMod n, pderivQ (fun y : PhaseSpace n => y.2 l) i x = 0 := by
    intro i
    rw [pderivQ, (hasFDerivAt_coord_snd l x).fderiv]
    simp [coordP]
  simp only [bracket, hQ, hP, hQ0, hP0, mul_zero, sub_zero]
  by_cases hkl : k = l
  · subst hkl
    rw [Finset.sum_eq_single k]
    · simp
    · intro b _ hb
      simp [Ne.symm hb]
    · intro h
      exact absurd (Finset.mem_univ _) h
  · rw [if_neg hkl]
    apply Finset.sum_eq_zero
    intro i _
    by_cases hk : k = i
    · subst hk
      have : ¬(l = k) := fun h => hkl h.symm
      simp [this]
    · simp [hk]

What this page does not claim

This declaration does not model the full gravitational field, which has no metric degree of freedom here. It does not prove the Jacobi identity for the bracket, which remains open for non-polynomial observables. It does not recover the full Dirac algebra 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: