Gravity Seven Gaps Weighted Hypersurface Bracket Pderiv P Ham W

The momentum partial

In classical mechanics, a Hamiltonian is a function of positions and momenta whose derivatives generate the equations of motion. On a periodic lattice, the Recognition Science framework builds a discrete Hamiltonian HamW (a sum over lattice sites of kinetic plus gradient energy, with a site-dependent weight in the gradient term) and asks how it changes when one momentum coordinate is varied. The declaration pderivP_HamW answers exactly that: the partial derivative of the weighted Hamiltonian with respect to the momentum at site j equals the lapse N_j times that momentum pi_j. The weight w does not appear, because the weight sits only in the stiffness (gradient-squared) slot, while the kinetic slot is unweighted.

This is a proved theorem in the machine-checked library of formal theorems, with no axioms beyond the standard three and no hypotheses on the weight. It is a sanity anchor: at unit weight, the weighted generator reduces to the frozen-1 generator, and the derivative matches the known unweighted result. The theorem also feeds the headline bracket identity, where two weighted Hamiltonian deformations close on a shift generator whose structure function is the background weight, appearing linearly. The momentum partial is the piece that carries no weight, so the bracket's weight factor comes entirely from the configuration partial.

What the declaration does not claim is as important as what it proves. The weight is a fixed function of the lattice site, never of the phase-space point; a phase-space-dependent structure function, which a full Dirac algebra would require, remains open. No claim is made about the continuum limit of the bracket itself, and no Hojman-Kuchar-Teitelboim rigidity target is inhabited. The theorem is a discrete algebraic identity, unconditional and exact, not a statement about general relativity.

/-- THEOREM. The momentum partial of the weighted generator: the kinetic slot
is unweighted, so the weight does not appear. -/
theorem pderivP_HamW (w N : ZMod n → ℝ) (j : ZMod n) (x : PhaseSpace n) :
    pderivP (HamW w N) j x = N j * x.2 j := by
  rw [pderivP, (hasFDerivAt_HamW w N x).fderiv, HamWD, ContinuousLinearMap.sum_apply]
  have step : ∀ i : ZMod n,
      (((N i / 2) • ((x.2 i • coordP i + x.2 i • coordP i)
        + w i • ((x.1 (i + 1) - x.1 i) • (coordQ (i + 1) - coordQ i)
            + (x.1 (i + 1) - x.1 i) • (coordQ (i + 1) - coordQ i))) :
          PhaseSpace n →L[ℝ] ℝ))
        ((0, Pi.single j 1) : PhaseSpace n)
      = (N i * x.2 i) * (if i = j then (1 : ℝ) else 0) := by
    intro i
    simp [Pi.single_apply]
    split_ifs <;> ring
  rw [Finset.sum_congr rfl fun i _ => step i, sum_mul_ite]

What this page does not claim

The weight is a fixed background function, not a phase-space-dependent inverse metric. No continuum limit of the bracket is proved here. No Hojman-Kuchar-Teitelboim rigidity statement is inhabited.

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: