Pith. sign in
module module moderate

IndisputableMonolith.Gravity.Analysis.Regge4DFlatSecondVariation

show as:
view Lean formalization →

Assembly point for the second variation of the 4D Regge action on a flat Freudenthal triangulation. It packages the Schläfli identity on the 4-simplex, the transverse-traceless edge decomposition, and candidate quadratic forms that vanish on pure gauge and on the axis TT mode. Gravity continuum-limit workers cite it when matching the discrete Hessian to the weak-field Einstein-Hilbert symbol. The argument is algebraic: pathwise Schläfli plus frozen preflight data, not a continuum existence proof.

claimOn the flat Freudenthal 4-complex, the second variation of the Regge action is assembled from the 4-simplex Schläfli identity $\sum_h A_h\,d\theta_h + \sum_e \ell_e\,d\alpha_e = 0$ (and its directional form), together with candidate zero-momentum and fold quadratic forms on symmetric $4\times 4$ edge data that vanish on the pure-gauge family and on the axis transverse-traceless mode.

background

Regge calculus replaces the continuum Einstein-Hilbert action by a sum of hinge areas times deficit angles on a simplicial complex. In 4D the elementary cell is the Freudenthal 4-simplex (ten edges, ten triangular hinges). The classical Schläfli identity relates first variations of those areas and dihedral angles; its pathwise flat and directional forms are imported from the 4-simplex Schläfli module, mirroring the closed 3D six-edge identity.

The continuum preflight freezes the weak-field EH target, the canonical mesh carrier, normalized TT data, the pure-gauge family, and honesty decoys before any Hessian computation. Edge data are symmetric $4\times 4$ real matrices; the edge TT decomposition splits them against a nonzero Euclidean wave covector into transverse-traceless, trace, and longitudinal pieces. Local alias Mat4 is that matrix type.

Upstream torus and Bloch-symbol modules supply the action-to-symbol dictionary on the periodic lattice of side $N=j+3$ with density weight $N^{-4}$. The tensor and transported algebraic closers bank $m^2$ as a quadratic form on the TT variety; full adjugate-style closed form remains open.

proof idea

This is an analysis assembly module, not a single theorem. It re-exports the flat and directional Freudenthal Schläfli identities (presence lemmas plus equalities), records differentiability of the seed angle, and defines two Schläfli-derived candidate quadratic forms (zero-momentum and fold). Equalities identify those candidates with the assembled expressions. Vanishing lemmas then check that both candidates are zero on the axis TT-plus ray and on the decoy pure-gauge family, using the edge TT decomposition and preflight normalizations. No continuum limit is proved here; the module only prepares the discrete second-variation ingredients.

why it matters in Recognition Science

Second variation on flat space is the discrete stand-in for the linearized Einstein operator. Matching its TT symbol to the weak-field EH continuum target is the binding step of the 4D continuum closure plan (preflight explicitly states that nothing there proves recovery). This module sits between pathwise Schläfli, edge TT decomposition, and the torus/Bloch symbol pipeline: it turns geometric identities into Hessian candidates that the algebraic closers and continuum-limit modules can evaluate ray by ray.

In the broader Recognition Science gravity stack the same pattern already closed in 3D (TT algebraic closer to continuum limit). The 4D lane still has an open full tensor contraction; the vanishing lemmas here are the honesty checks that decoys and pure gauge do not pollute the TT quadratic form. No downstream consumers are wired in the graph yet; the intended parents are the 4D continuum-limit and symbol-matching theorems.

scope and limits

depends on (11)

Lean names referenced from this declaration's body.

declarations in this module (30)