Gravity Analysis Regge Flat4 Dhessian Assembly True Weight Zero Mom Bilinear Smu

The zero-momentum bilinear form

In the Recognition Science framework's study of gravity, researchers work with a discrete model of spacetime called Regge calculus. Here, spacetime is built from flat four-dimensional pieces glued together, and the central object is the Regge action, a sum over the "hinges" where pieces meet. The declaration trueWeightZeroMomBilinear_smul_left concerns a specific quadratic form, bilinear form, that arises when one examines how this action responds to small changes in the edge lengths of the pieces.

The theorem states that this bilinear form, called trueWeightZeroMomBilinear, is homogeneous in its first argument: scaling the first input by a real number scales the output by that same number. In symbols, for any real number c and any two matrices A and B representing edge-length variations, the form satisfies trueWeightZeroMomBilinear(cA, B) = c · trueWeightZeroMomBilinear(A, B). This property, known as left-linearity in the first slot, is a fundamental algebraic requirement for any object that aspires to be a genuine quadratic form, and it is a prerequisite for defining a well-behaved second variation of the action.

This result is part of a larger effort to assemble the full Hessian, the matrix of second derivatives, of the four-dimensional Regge action. The framework's machine-checked library of formal theorems has verified this left-linearity, along with the related property of bilinearity, meaning the form is linear in each of its two arguments separately. These algebraic properties are essential for the Hessian to be a meaningful object that can be used to study the stability of spacetime configurations and to compare the discrete Regge action with the continuous Einstein-Hilbert action from general relativity.

In Recognition Science, this work is framed as a step toward showing that its discrete model of gravity recovers the known physics of general relativity. The theorem about left-linearity is a small but necessary piece of that larger puzzle. This specific theorem does not establish that the Regge action converges to the Einstein-Hilbert action, a major open problem. It does not address the behavior of the system at non-zero momentum, where the mathematics becomes more complex. And it does not, by itself, determine the correct weights for the various terms in the action; those weights are chosen from the framework's geometric principles, not derived from this linearity property.

def trueWeightZeroMomBilinear (A B : Mat4) : ℝ :=
  ∑ ty : HingeOrbitType, orbitZeroMomBilinear ty A B

def trueWeightZeroMomBilinear (A B : Mat4) : ℝ :=
  ∑ ty : HingeOrbitType, orbitZeroMomBilinear ty A B

What this page does not claim

This theorem does not prove that the Regge action converges to the Einstein-Hilbert action. This theorem does not address finite-momentum Bloch phase folding. This theorem does not derive the orbit weights from Einstein-Hilbert action.

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/Analysis/ReggeFlat4DHessianAssembly.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: