Geometry Regge Hessian3 D Hessian Quadratic

The quadratic form

A quadratic form is a rule that takes a vector and returns a number by multiplying each pair of entries with a fixed matrix. The declaration hessianQuadratic defines this rule in full: for a matrix H and a vector ξ, it sums H[i][j] times ξ[i] times ξ[j] over all pairs of indices. Written out, the formula is Σᵢ Σⱼ Hᵢⱼ ξᵢ ξⱼ. This is the standard bilinear form from linear algebra, the same object that appears in calculus when you expand a smooth function to second order around a point.

The definition belongs to a module about the Regge action, a discrete version of Einstein's theory of gravity that works on a triangulated space instead of a smooth manifold. In this setting, a conformal potential (a real number attached to each vertex of a 3D triangulation) represents a local scaling of the geometry. The Hessian matrix collects the second derivatives of the action with respect to these vertex potentials. The quadratic form then evaluates that second-order curvature: given a small perturbation ξ of the vertex potentials, the number hessianQuadratic H ξ measures how the action bends away from its value at the flat, zero-potential configuration.

The module also records a structural fact about the action. A structure called ReggeHessianData packages the action, its Hessian matrix, a symmetry condition, and a theorem stating that the difference between the action at any perturbation and the action at zero potential equals one half times the quadratic form. A separate theorem, regge_secondVariation_eq_hessian, extracts this second-variation formula from any concrete implementation. These are formal statements in a machine-checked library of mathematical theorems, meaning the algebra of the expansion is verified by computer rather than assumed by hand.

In Recognition Science, this declaration plays a supporting role. The framework derives physical structure from a single cost function, and the Regge Hessian module provides the analytic machinery to study how that structure responds to small geometric changes. The quadratic form is the tool that turns a matrix of second derivatives into a single number, the quantity that tells you whether a configuration sits at a minimum, maximum, or saddle point of the action. It is a piece of standard mathematics, made precise in the framework's library, that lets the larger derivation talk about stability and curvature in a controlled way.

What the declaration does not claim is just as important. It does not assert that the Regge action is the correct theory of gravity, nor that the conformal ansatz is physically realized. It does not prove that any particular triangulation minimizes the action. The quadratic form is a definition, not a theorem about the world. The theorems in the module only guarantee that the algebraic identity holds: the action difference equals the quadratic form under the stated assumptions. Whether that identity describes actual spacetime is a separate question, one the module does not address.

/-- Quadratic form associated to a Hessian matrix. -/
def hessianQuadratic {n : ℕ} (H : Fin n → Fin n → ℝ) (ξ : Fin n → ℝ) : ℝ :=
  ∑ i : Fin n, ∑ j : Fin n, H i j * ξ i * ξ j

/-- Genuine Regge Hessian data for a triangulation.  `action` is the
Regge action under the conformal ansatz, and `hessian` is the matrix of
its second variation at `ξ = 0`. -/
structure ReggeHessianData (K : Triangulation3D) where
  action : VertexPotential K → ℝ
  hessian : Fin K.nV → Fin K.nV → ℝ
  hessian_symm : ∀ i j, hessian i j = hessian j i
  flat_firstVariation_zero : Prop
  secondVariation :
    ∀ ξ : VertexPotential K,
      action ξ - action (zeroPotential K) =
        (1 / 2) * hessianQuadratic hessian ξ

/-- Extract the second-variation formula from a concrete Hessian package. -/
theorem regge_secondVariation_eq_hessian
    (K : Triangulation3D) (D : ReggeHessianData K) (ξ : VertexPotential K) :
    D.action ξ - D.action (zeroPotential K) =
      (1 / 2) * hessianQuadratic D.hessian ξ :=
  D.secondVariation ξ

/-- 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 module does not prove that the Regge action is the correct theory of gravity. The module does not claim that any particular triangulation minimizes the action. The quadratic form is a definition, not a theorem about physical spacetime.

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: