Gravity Analysis Regge Ttderivative Gate Flat Angle Jacobian Cofactor Form

The flat angle Jacobian

A tetrahedron is a solid with four triangular faces, six edges, and six dihedral angles, the angles between pairs of faces. In the Recognition Science framework, a discrete model of gravity builds spacetime from such tetrahedra, and the action, a quantity whose minimization gives the equations of motion, is a sum over edges of the square root of edge length times a deficit angle. The declaration flatAngleJacobian_cofactor_form concerns the derivative of those dihedral angles with respect to changes in the squared edge lengths, evaluated at a special configuration called the flat tuple.

The flat tuple is the set of squared edge lengths for a regular tetrahedron, one where all six edges are equal. At this configuration, the derivative of each dihedral angle with respect to each squared edge length, the flat angle Jacobian, takes a strikingly simple form. The declaration proves that every entry of this 6 by 6 matrix is the product of a purely algebraic cofactor term and an arccosine factor that evaluates exactly to one of five constants: the square root of 2, 1, 2 over the square root of 3, 1, 1, or the square root of 2. No arccosine value remains unevaluated; every factor is a closed-form constant.

The result goes further for the first row, corresponding to the first dihedral angle. The declaration proves that this row, after the cofactor algebra, evaluates to the exact rational tuple (0, 0, 0, 0, -1/4, 1/2). This means the derivative of the first dihedral angle with respect to the first four squared edge lengths is zero, and with respect to the fifth and sixth it is exactly minus one quarter and one half. These are not numerical approximations; they are exact rational numbers proved by algebraic manipulation.

In Recognition Science, this declaration is a step in a larger program to analyze the behavior of gravitational waves on a discrete spacetime lattice. The flat angle Jacobian is a piece of the derivative structure needed to compute how the action responds to small perturbations. The declaration establishes this derivative structure cleanly at the flat point, providing a shared stencil that later stages of the program can reference. It proves the first-derivative structure exists and is exactly this cofactor form.

The declaration does not claim anything about second derivatives. It does not compute any lattice sum over many tetrahedra; it concerns a single tetrahedron at the flat point. It does not prove any statement about the continuum limit of the theory, and it does not establish the value of the continuum transverse-traceless symbol, which remains an open target with a status flag of false. The declaration is a precise, local, algebraic result, not a global physical conclusion.

/-- THE SHARED STENCIL JACOBIAN: closed-form derivative of the `f`-th local
dihedral angle with respect to the `k`-th local squared-edge coordinate,
evaluated at the flat Freudenthal tuple, in the action's local six-edge
ordering.  `flatAngleJacobian f k = ∂θ_f/∂a_k (freudenthalTetSqEdges)`. -/
def flatAngleJacobian (f k : Fin 6) : ℝ :=
  dihedralAngle3SqClosedFormDeriv freudenthalTetSqEdges f k

/-- The exact `f = 0` Jacobian row values at the flat tuple. -/
def flatAngleJacobianRow0 : Fin 6 → ℝ
  | 0 => 0
  | 1 => 0
  | 2 => 0
  | 3 => 0
  | 4 => -(1 / 4)
  | 5 => 1 / 2

What this page does not claim

No second derivatives of the action profile are proved here. No lattice sum over many tetrahedra is computed. The continuum value of the TT symbol is not established; it remains an open target.

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/ReggeTTDerivativeGate.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: