Encyclopedia Gravity Gravity Seven Gaps Weighted Hypersurface Bracket Bracket Ham W Ham W

ARTICLE 3 claims 3 theorems

Gravity Seven Gaps Weighted Hypersurface Bracket Bracket Ham W Ham W

A machine-checked theorem shows how a fixed background weight enters the algebra of gravitational constraints on a lattice, and exactly where it does not reach.

Verify this page

The weighted bracket

In the canonical formulation of general relativity, the Hamiltonian and diffeomorphism constraints do not commute; their bracket produces a further constraint. On a periodic lattice, this relation becomes an exact algebraic identity. The theorem bracket_HamW_HamW in the framework's machine-checked library of formal theorems establishes the precise form of this identity when the Hamiltonian carries a fixed background weight weight, a number assigned to each lattice site that multiplies the gradient-squared term in the energy density.

The result is an equation. For two smeared Hamiltonians H_w[N] and H_w[M], their Poisson bracket equals a sum over lattice sites: (N_j M_{j+1} - M_j N_{j+1}) * w_j * (pi_{j+1} (q_{j+1} - q_j)). In words, the bracket of two weighted Hamiltonian deformations is a shift generator whose smearing is the discrete lapse Wronskian multiplied by the background weight. The weight appears linearly, once, because it sits only in the stiffness slot; the kinetic slot is unweighted. This mirrors the continuum Dirac structure function, where the inverse spatial metric multiplies the Wronskian.

The theorem is unconditional and axiom-clean, with no unproved assumptions. At unit weight, the weighted generator reduces exactly to the frozen-1 generator, and the weighted bracket reproduces the earlier unweighted result. A companion theorem shows that the weighted structure sums converge to the continuum integral for continuous profiles. These are exact statements on the lattice, not limits taken informally.

What the theorem does not claim is as important as what it proves. The weight w is a fixed function of the lattice site only; it is not a phase-space-dependent inverse metric. The full Dirac algebra, with a structure function depending on the configuration variables, remains open. The theorem does not recover general relativity in the continuum, does not touch the Hojman-Kuchar-Teitelboim rigidity statement, and does not establish Jacobi identities for the bracket. It is a step toward the constraint algebra, not the algebra itself.

THEOREM bracket_HamW_HamW · IndisputableMonolith/Gravity/SevenGaps/WeightedHypersurfaceBracket.lean
bracket_HamW_HamW · IndisputableMonolith/Gravity/SevenGaps/WeightedHypersurfaceBracket.lean:194 
/-- 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]
THEOREM HamW_one · bracket_HamW_HamW_one · IndisputableMonolith/Gravity/SevenGaps/WeightedHypersurfaceBracket.lean
HamW_one · IndisputableMonolith/Gravity/SevenGaps/WeightedHypersurfaceBracket.lean:110 
/-- 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
bracket_HamW_HamW_one · IndisputableMonolith/Gravity/SevenGaps/WeightedHypersurfaceBracket.lean:233 
/-- 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]
THEOREM weightedStructureSum_tendsto · IndisputableMonolith/Gravity/SevenGaps/WeightedHypersurfaceBracket.lean
weightedStructureSum_tendsto · IndisputableMonolith/Gravity/SevenGaps/WeightedHypersurfaceBracket.lean:253 
/-- THEOREM (weighted structure smearing, continuum limit). Sample a
background weight profile `W`, a continuum lapse-Wronskian profile `Wr`
(the limit shape of `(N_j M_{j+1} - M_j N_{j+1}) / h`), and a closure-density
profile `S` (the limit shape of the point-split density
`pi_{j+1} (q_{j+1} - q_j) / h`, one factor of `h` absorbed by the gradient),
all continuous on `[0, 1]`. Then the h-scaled w-weighted structure sums of
`bracket_HamW_HamW` converge:
`(1/N) * sum_{k<N} W(k/N) * (Wr(k/N) * S(k/N)) -> integral_0^1 W * (Wr * S)`.

h-scaling convention (stated per panel preregistration): the explicit `1/N`
prefactor is the single factor of lattice spacing carried by the discrete
lapse Wronskian; the sampled profiles are all O(1). This is a limit of the
SMEARING SHAPE with continuum profiles sampled directly; it is not a proof
that the discrete Wronskian of sampled lapses converges at rate h (that needs
C^1 data and is left OPEN with the full Dirac continuum limit). Direct
application of `Analysis.weightedLatticeSum_tendsto`. -/
theorem weightedStructureSum_tendsto (W Wr S : ℝ → ℝ)
    (hW : ContinuousOn W (Set.Icc 0 1)) (hWr : ContinuousOn Wr (Set.Icc 0 1))
    (hS : ContinuousOn S (Set.Icc 0 1)) :
    Filter.Tendsto
      (fun N : ℕ => (1 / (N : ℝ)) * ∑ k ∈ Finset.range N,
        W ((k : ℝ) / (N : ℝ)) * (Wr ((k : ℝ) / (N : ℝ)) * S ((k : ℝ) / (N : ℝ))))
      Filter.atTop (nhds (∫ x in (0:ℝ)..1, W x * (Wr x * S x))) := by
  have h := Analysis.weightedLatticeSum_tendsto (fun x => Wr x * S x) W
    (hWr.mul hS) hW
  have hint : (∫ x in (0:ℝ)..1, (Wr x * S x) * W x)
      = ∫ x in (0:ℝ)..1, W x * (Wr x * S x) :=
    intervalIntegral.integral_congr fun x _ => mul_comm _ _
  rw [hint] at h
  refine h.congr fun N => ?_
  congr 1
  refine Finset.sum_congr rfl fun k _ => ?_
  show Wr ((k : ℝ) / (N : ℝ)) * S ((k : ℝ) / (N : ℝ)) * W ((k : ℝ) / (N : ℝ))
      = W ((k : ℝ) / (N : ℝ)) * (Wr ((k : ℝ) / (N : ℝ)) * S ((k : ℝ) / (N : ℝ)))
  ring

What this page does not claim

The weight w is a fixed background function, not a phase-space-dependent inverse metric. The theorem does not recover general relativity in the continuum limit. The theorem does not provide a Hojman-Kuchar-Teitelboim target instance.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND