Gravity Seven Gaps Weighted Hypersurface Bracket Differentiable Ham W

Differentiability of the weighted Hamiltonian

In classical mechanics, a Hamiltonian is a function that assigns an energy to each state of a system. For a system with finitely many degrees of freedom, such as a chain of particles, the state is described by positions and momenta. The Hamiltonian is differentiable if a small change in the state produces a change in energy that is approximately linear, with the approximation improving as the change shrinks. This property is essential for defining equations of motion and for computing how observables change in time.

The declaration differentiable_HamW in the Recognition Science library proves that a particular weighted Hamiltonian, written HamW w N, is differentiable. This Hamiltonian is a sum over lattice sites of a kinetic term (momentum squared) plus a potential term that penalizes differences between neighboring positions. The novelty is a background weight w, a fixed number attached to each site, that multiplies only the potential (gradient) part. The theorem states that for any choice of weight and any choice of the smearing function N, the function is differentiable at every point of the phase space. The proof is unconditional: it requires no extra assumptions about the weight or the state.

This result is a technical but necessary step in a larger program. The weighted Hamiltonian is used to study how deformations of a spatial slice generate changes in the gravitational field, on a discrete lattice. Differentiability is the foundation for computing the Poisson bracket of two such Hamiltonians, which describes how two successive deformations combine. The library also proves that when the weight is set to one, the weighted Hamiltonian reduces exactly to the previously studied unweighted one, and that the bracket of two weighted Hamiltonians closes on a shift generator with the weight appearing linearly.

What the theorem does not claim is equally important. The weight here is a fixed function of the lattice site, not a function of the phase-space point. A phase-space-dependent structure function, which would be needed for a full recovery of general relativity's constraint algebra, remains an open problem. The theorem also does not address the continuum limit of the full Dirac algebra, nor does it touch the Hojman-Kuchar-Teitelboim rigidity statement. These are targets for future work, not achievements of this declaration.

/-- THEOREM. `HamW w N` is (unconditionally) differentiable. -/
theorem differentiable_HamW (w N : ZMod n → ℝ) :
    Differentiable ℝ (HamW (n := n) w N) :=
  fun x => (hasFDerivAt_HamW w N x).differentiableAt

/-- THEOREM. `HamW w N` is (unconditionally) differentiable. -/
theorem differentiable_HamW (w N : ZMod n → ℝ) :
    Differentiable ℝ (HamW (n := n) w N) :=
  fun x => (hasFDerivAt_HamW w N x).differentiableAt

/-- THEOREM (sanity anchor). At unit weight the weighted generator is the
frozen-1 generator of `HypersurfaceDeformation.lean`, as an equality of
functions on phase space. -/
theorem HamW_one (N : ZMod n → ℝ) : HamW (fun _ => 1) N = Ham N := by
  funext x
  unfold HamW Ham
  refine Finset.sum_congr rfl fun i _ => ?_
  show (N i / 2) *
      (x.2 i * x.2 i + 1 * ((x.1 (i + 1) - x.1 i) * (x.1 (i + 1) - x.1 i)))
      = (N i / 2) * (x.2 i * x.2 i + (x.1 (i + 1) - x.1 i) * (x.1 (i + 1) - x.1 i))
  ring

/-- THEOREM (headline; exact discrete weighted hypersurface deformation).
`{H_w[N], H_w[M]} = sum_j (N_j M_{j+1} - M_j N_{j+1}) * w_j *
(pi_{j+1} (q_{j+1} - q_j))`.

The bracket of two w-weighted Hamiltonian deformations is a D-type (shift)
generator: the point-split momentum density `pi_{j+1} (q_{j+1} - q_j)` smeared
by the discrete lapse Wronskian TIMES the background weight `w_j` at the left
split point. The weight appears exactly where the Dirac structure function
sits (in the continuum, `{H(N), H(M)} = D(g^{xx} (N M' - M N'))`), and it
appears LINEARLY: with the weight in the stiffness slot and the kinetic slot
unweighted, exactly one factor of `w` survives the Kronecker collapse, so the
answer is w-weighted, not w^2-weighted. Antisymmetric in `N, M` by
inspection; vanishes identically for `N = M`.

Honesty (panel lock): this is a BACKGROUND-w structure function, not a
phase-space-dependent inverse metric; it moves toward but does NOT flip
gap5_constraint_recovery; HKT rigidity is untouched and OPEN. -/
theorem bracket_HamW_HamW (w N M : ZMod n → ℝ) (x : PhaseSpace n) :
    bracket (HamW w N) (HamW w M) x
      = ∑ j : ZMod n, (N j * M (j + 1) - M j * N (j + 1))
          * (w j * (x.2 (j + 1) * (x.1 (j + 1) - x.1 j))) := by
  simp only [bracket, pderivQ_HamW, pderivP_HamW]
  have step1 : (∑ j : ZMod n,
      ((N (j - 1) * (w (j - 1) * (x.1 j - x.1 (j - 1)))
          - N j * (w j * (x.1 (j + 1) - x.1 j))) * (M j * x.2 j)
        - N j * x.2 j
          * (M (j - 1) * (w (j - 1) * (x.1 j - x.1 (j - 1)))
              - M j * (w j * (x.1 (j + 1) - x.1 j)))))
      = ∑ j : ZMod n,
          (N (j - 1) * M j - M (j - 1) * N j)
            * (w (j - 1) * (x.2 j * (x.1 j - x.1 (j - 1)))) :=
    Finset.sum_congr rfl fun j _ => by ring
  rw [step1]
  refine sum_reindex 1
    (fun k => (N (k - 1) * M k - M (k - 1) * N k)
      * (w (k - 1) * (x.2 k * (x.1 k - x.1 (k - 1))))) _ fun j => ?_
  have e1 : j + 1 - 1 = j := by ring
  simp only [e1]

What this page does not claim

The weight is not a function of the phase-space point. The theorem does not prove the phase-space-dependent structure function exists. The theorem does not establish the continuum limit of the full Dirac algebra.

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/WeightedHypersurfaceBracket.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: