Encyclopedia Gravity Gravity Seven Gaps Weighted Hypersurface Bracket

ARTICLE 3 claims 3 theorems

Gravity Seven Gaps Weighted Hypersurface Bracket

A machine-checked proof shows how a fixed background weight enters the algebra of spacetime deformations on a lattice, a step toward recovering general relativity from a discrete ledger.

Verify this page

The weighted bracket

In classical mechanics, the Poisson bracket measures how two quantities change together. For gravity, the bracket of two deformations of a spatial slice produces a new deformation, and the coefficients in that relation are called structure functions. In general relativity, the structure function is the inverse spatial metric, which depends on the gravitational field itself. The module here studies a simpler, discrete version of this problem on a periodic lattice of points.

The framework's machine-checked library of formal theorems proves an exact identity for a recognition cost, a discrete record of events on a lattice. The Hamiltonian, the energy generator, has a kinetic part from momenta and a stiffness part from field gradients. The new result inserts a fixed background weight w into the stiffness slot. The theorem states that the bracket of two such weighted deformations closes on a shift generator, with the weight appearing linearly in the structure function, exactly where the Dirac structure function sits in the continuum theory.

The proof is unconditional and axiom-clean. At unit weight, the weighted generator reduces to the previously proved frozen-1 case, confirming the new theorem is a genuine generalization. The weight is a function of the lattice site only, not of the phase-space point, so this is a background structure function, not the fully general inverse metric.

A further theorem shows the weighted sums converge to the continuum integral for continuous profiles. This is a limit of the smearing shape, not a proof that the discrete Wronskian converges at a rate, which remains open. The phase-space-dependent structure function required for full general relativity recovery also remains open and is not approximated here.

In plain language, the module proves that a fixed background weight enters the deformation algebra in the right place, linearly, and that the discrete result has the correct continuum limit. It is a precise, limited step. It does not claim to recover general relativity, and it does not touch the rigidity theorem that would be needed for that claim.

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 · 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
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

This module does not recover general relativity or provide a phase-space-dependent inverse metric. The continuum limit theorem does not prove convergence of the discrete Wronskian at a specific rate. No HKT rigidity instance is provided or implied.

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