Gravity Seven Gaps Weighted Hypersurface Bracket Has Fderiv At Ham W

The weighted generator's derivative

A Hamiltonian is a function on phase space that generates the time evolution of a physical system. The declaration hasFDerivAt_HamW establishes that a specific lattice Hamiltonian, called the weighted generator, has a well-defined derivative at every point of its phase space. The derivative is an explicit continuous linear map, written out in full, and the proof is unconditional: it holds for any background weight function on the lattice sites, with no extra hypotheses.

The weighted generator models a discrete system with a kinetic energy term and a potential energy term. The potential term carries a fixed background weight w that multiplies the squared difference between neighboring lattice positions, while the kinetic term is unweighted. The weight depends only on the lattice site, never on the phase-space point. The theorem shows that this function is differentiable everywhere, and it gives the derivative explicitly: the derivative is a sum over lattice sites of terms involving the momentum and the weighted gradient of the configuration.

This differentiability result is a technical foundation. It is used to compute the partial derivatives of the weighted generator, and those partial derivatives feed into the bracket of two such generators. The bracket, which measures how two deformations fail to commute, turns out to be a shift generator whose smearing is the discrete lapse Wronskian multiplied by the background weight. The weight appears linearly, exactly where the Dirac structure function sits in the continuum theory. At unit weight, the weighted generator reduces to the frozen-1 generator, and the weighted bracket reproduces the previously proved frozen-1 bracket.

In Recognition Science, this result is part of a campaign to build up the constraint algebra of gravity from a lattice starting point. The framework's machine-checked library of formal theorems proves the derivative statement and the bracket identity with no gaps and no extra axioms. The continuum limit of the weighted structure smearing is also proved, under explicit continuity hypotheses on the sampled profiles.

What the declaration does not claim is just as important. The background weight is fixed, not phase-space-dependent. The full Dirac algebra requires a structure function that depends on the phase-space point, and that object remains open. The framework does not claim to recover general relativity from this lattice model, nor does it claim to touch the Hojman-Kuchar-Teitelboim rigidity statement. The differentiability result is a stepping stone, not the destination.

lemma hasFDerivAt_HamW (w N : ZMod n → ℝ) (x : PhaseSpace n) :
    HasFDerivAt (HamW w N) (HamWD w N x) x := by
  unfold HamW HamWD
  exact HasFDerivAt.fun_sum fun i _ =>
    ((((hasFDerivAt_coord_snd i x).mul (hasFDerivAt_coord_snd i x)).add
      ((((hasFDerivAt_coord_fst (i + 1) x).sub (hasFDerivAt_coord_fst i x)).mul
        ((hasFDerivAt_coord_fst (i + 1) x).sub (hasFDerivAt_coord_fst i x))).const_mul
          (w i))).const_mul (N i / 2))

lemma hasFDerivAt_HamW (w N : ZMod n → ℝ) (x : PhaseSpace n) :
    HasFDerivAt (HamW w N) (HamWD w N x) x := by
  unfold HamW HamWD
  exact HasFDerivAt.fun_sum fun i _ =>
    ((((hasFDerivAt_coord_snd i x).mul (hasFDerivAt_coord_snd i x)).add
      ((((hasFDerivAt_coord_fst (i + 1) x).sub (hasFDerivAt_coord_fst i x)).mul
        ((hasFDerivAt_coord_fst (i + 1) x).sub (hasFDerivAt_coord_fst i x))).const_mul
          (w i))).const_mul (N i / 2))

/-- MODEL. The background-weighted smeared Hamiltonian
`H_w[N] = sum_i (N_i / 2) * (pi_i^2 + w_i * (q_{i+1} - q_i)^2)`.
The fixed background weight `w` sits in the stiffness (gradient) slot; the
kinetic slot is unweighted. `w` depends on the lattice site only, never on
the phase-space point: this is a BACKGROUND-w object. -/
def HamW (w N : ZMod n → ℝ) (x : PhaseSpace n) : ℝ :=
  ∑ i : ZMod n, (N i / 2) *
    (x.2 i * x.2 i + w i * ((x.1 (i + 1) - x.1 i) * (x.1 (i + 1) - x.1 i)))

/-- THEOREM (frozen-1 recovery). Substituting the unit weight into the
weighted bracket literally reproduces the proved frozen-1 statement
`bracket_Ham_Ham`: the weighted theorem is an honest generalization, not a
parallel construction. Proof: rewrite by `HamW_one` and apply the existing
theorem. -/
theorem bracket_HamW_HamW_one (N M : ZMod n → ℝ) (x : PhaseSpace n) :
    bracket (HamW (fun _ => 1) N) (HamW (fun _ => 1) M) x
      = ∑ j : ZMod n, (N j * M (j + 1) - M j * N (j + 1))
          * (x.2 (j + 1) * (x.1 (j + 1) - x.1 j)) := by
  rw [HamW_one, HamW_one, bracket_Ham_Ham]

What this page does not claim

The background weight is not phase-space-dependent and does not approximate a phase-space-dependent inverse metric. The theorem does not prove that the lattice model recovers general relativity in any limit. The differentiability result does not establish the Jacobi identity for the bracket.

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: