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

The weighted bracket at unit weight

In classical mechanics, the Poisson bracket measures how two quantities change with respect to each other's phase-space coordinates. For a system on a periodic lattice of n sites, the Recognition Science framework defines a Hamiltonian generator HamW that includes a fixed background weight w at each site, multiplying only the gradient-squared (stiffness) term, not the kinetic term. The bracket of two such weighted generators, bracket_HamW_HamW, is an exact identity: it equals a sum over sites of a discrete Wronskian (N_j M_{j+1} - M_j N_{j+1}) times the weight w_j times a momentum-gradient product. This is the weighted analogue of the standard hypersurface deformation algebra.

The declaration bracket_HamW_HamW_one is the specialization of that identity to the case where the weight w is identically 1 at every site. It states that the bracket of two unit-weight generators equals exactly the same sum but without the weight factor: sum_j (N_j M_{j+1} - M_j N_{j+1}) * (pi_{j+1} (q_{j+1} - q_j)). This is not a new or parallel result; the proof proceeds by rewriting the unit-weight generator into the frozen-1 generator via the theorem HamW_one, and then applying the previously proved bracket_Ham_Ham. The declaration therefore establishes that the weighted construction is a genuine generalization that reduces correctly to the known unweighted case.

In Recognition Science, this identity is a sanity anchor within a larger program to recover general relativity's constraint algebra from a discrete lattice. The weight w is interpreted, in the continuum limit, as the sampled inverse spatial metric or local sound speed squared of a static background line element; that interpretation is commentary, not a theorem. The bracket's structure function, where the weight appears linearly, mirrors the position of the Dirac structure function in the continuum relation {H(N), H(M)} = D(g^{xx} (N M' - M N')). The declaration bracket_HamW_HamW_one confirms that at unit weight, the weighted bracket collapses to the frozen-1 statement, preserving the framework's internal consistency.

What the declaration does not claim is as important as what it proves. The weight w is a fixed function of the lattice site, never of the phase-space point (q, pi). The framework explicitly states that the phase-space-dependent structure function g^{ab}[q] demanded by the full Dirac algebra remains open and is not approximated or inhabited here. No Hojman-Kuchar-Teitelboim target instance is provided, and the HKT rigidity statement is not touched. The continuum limit of the full Dirac algebra, and the rate of convergence of the discrete Wronskian, are also left open. The declaration is a precise algebraic identity, not a step toward recovering general relativity's full constraint structure.

/-- 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 (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]

/-- 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)))

What this page does not claim

The declaration does not prove that the weighted bracket recovers general relativity's constraint algebra in the continuum limit. The declaration does not provide a phase-space-dependent structure function g^{ab}[q]. The declaration does not inhabit the Hojman-Kuchar-Teitelboim target or address the HKT rigidity statement.

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: