Geometry Regge Hessian3 D Hessian Quadratic Sum Comm

A commutative summation

The declaration hessianQuadratic_sum_comm is a theorem about a double sum. It states that for any matrix H and any vector ξ, the sum over all pairs of indices of H(i,j) * ξ(i) * ξ(j) does not depend on the order in which you add the terms. Summing over i first and then j gives the same result as summing over j first and then i. This is a standard property of finite sums, proved here in the machine-checked library of formal theorems for the framework's geometry module.

In the context of the Regge action, a discrete approximation to Einstein's theory of gravity on a triangulated space, this theorem is a technical convenience. The framework models the second variation of the action as a quadratic form built from a Hessian matrix. The theorem confirms that when you compute this quadratic form, you may rearrange the summation order freely. It is a lemma that supports the larger structure of the Regge Hessian data, which packages the action, its Hessian matrix, and the proof that the quadratic Taylor coefficient is represented by that matrix.

The theorem does not claim anything about the physical content of the Regge action. It does not say that the action is stable, that the Hessian is positive definite, or that any particular triangulation is preferred. It only asserts a formal identity about finite sums. The theorem also does not depend on the specific entries of the matrix H; it holds for any real-valued matrix of any finite size. This generality is what makes it a reusable building block in the framework's formal development.

What this means for the reader is that the framework's geometry code has a verified foundation for one small step in its calculations. When the framework later proves properties of the Regge action, it can rely on this summation identity without rechecking it. The theorem is a piece of the formal scaffolding, not a claim about the physics of gravity itself.

/-- Swap the order of summation in the Hessian quadratic form. -/
theorem hessianQuadratic_sum_comm {n : ℕ} (H : Fin n → Fin n → ℝ)
    (ξ : Fin n → ℝ) :
    hessianQuadratic H ξ =
      ∑ j : Fin n, ∑ i : Fin n, H i j * ξ i * ξ j := by
  unfold hessianQuadratic
  rw [Finset.sum_comm]

/-- Swap the order of summation in the Hessian quadratic form. -/
theorem hessianQuadratic_sum_comm {n : ℕ} (H : Fin n → Fin n → ℝ)
    (ξ : Fin n → ℝ) :
    hessianQuadratic H ξ =
      ∑ j : Fin n, ∑ i : Fin n, H i j * ξ i * ξ j := by
  unfold hessianQuadratic
  rw [Finset.sum_comm]

What this page does not claim

The theorem does not claim the Regge action is stable or that its Hessian is positive definite. The theorem does not claim any specific triangulation is preferred or physically meaningful. The theorem does not assert any property of the Regge action beyond the formal summation identity.

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/Geometry/ReggeHessian3D.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: