Pith. sign in
module module moderate

IndisputableMonolith.Geometry.ReggeActionFirstVariation

show as:
view Lean formalization →

First-variation calculus for the nonlinear Regge action on finite 3D triangulations. The module differentiates conformal edge lengths, tetrahedral dihedral angles, and hinge measures along lines through the flat potential, so the linear term can cancel by Schläfli. Second-variation, Freudenthal-cube, and tensor/shear gravity modules import these directional derivatives. The work is chain-rule analysis on Cayley-Menger/arccos data plus single-edge Fréchet evaluations at the flat point.

claimFor the line $V_t=V_{\mathrm{flat}}+t\eta$ through the flat conformal potential, squared edge lengths, tetrahedral dihedral angles, and hinge measures admit directional derivatives at $t=0$. The first variation of the Regge action is the corresponding weighted sum of deficit angles times edge-length rates (discrete Schläfli form), under nondegeneracy of the tetrahedral cone and arccos arguments away from $\pm 1$.

background

Regge calculus replaces the Einstein-Hilbert action by a sum over hinges of deficit angle times hinge measure. In three dimensions hinges are edges; the first variation of the action is controlled by the Schläfli identity, which relates changes of dihedral angles to changes of edge lengths inside each tetrahedron and cancels globally on a closed triangulation.

This module sits in the Recognition geometry track that builds a nonlinear Regge action from a conformal edge chart (one scalar potential per vertex, edge lengths by endpoint averaging). Upstream, ReggeActionSmoothness supplies the analytic hypotheses that the chart stays in the nondegenerate tetrahedral cone and that the finite action is smooth at the flat potential. SchlaefliTetrahedronProof and SchlaefliTriangulation3D supply the local closed-form tetrahedral Schläfli package and its finite sum over top simplices.

Local objects include the line through the flat potential in direction $\eta$ (kept here so the first-variation module does not depend on the second-variation module), directional derivatives of conformal squared edges, $C^\infty$ regularity of dihedral cosine/angle maps off degeneracy, and the hinge-measure directional derivative.

proof idea

Definition-and-derivative module, not a single theorem. It introduces the flat-potential line, proves squared-edge maps are differentiable along that line at $t=0$ by updating one coordinate and applying the conformal edge chart, then lifts differentiability to dihedral data via contDiff of the Cayley-Menger/arccos expressions on the nondegenerate locus. Single-direction Fréchet derivatives of the dihedral-angle map are evaluated on basis updates; hinge-measure directional derivatives are assembled from those edge and angle rates. Global first-variation shape is the finite Schläfli sum imported from the triangulation package.

why it matters in Recognition Science

Supplies the linear layer that ReggeActionSecondVariation needs before stating nonlinear second-variation and cubic-remainder targets. FreudenthalCubeTriangulation imports the same incidence and derivative bookkeeping for the standard six-tetrahedron cube. Gravity.TensorShearSector sits downstream because the pure conformal (scalar-potential) ansatz treated here cannot represent shear or transverse-traceless modes; the first-variation identities are the baseline against which a fuller weak-field sector must be compared. In the RS geometry chain this is the step that turns smoothness plus local Schläfli into a usable vanishing (or sourced) linear term for the discrete action at flat space.

scope and limits

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (65)