Pith. sign in
module module moderate

IndisputableMonolith.Geometry.ReggeActionFirstVariation

show as:
view Lean formalization →

First-variation calculus for the nonlinear Regge action along affine lines through the flat conformal potential. Supplies directional derivatives of squared edge lengths, dihedral angles, and hinge measures at the flat background, under tetrahedral nondegeneracy. Second-variation, Freudenthal-cube, and gravity shear-sector modules import this layer. Arguments are chain-rule and Fréchet reductions on the conformal edge chart plus local Schläfli input.

claimDevelops the first variation of the Regge action along the line $t\mapsto\phi_0+t\eta$ through the flat vertex potential $\phi_0$ in direction $\eta$. Records directional derivatives at $t=0$ of conformal squared edge lengths, tetrahedral dihedral angles (via cosine and arccos charts), and hinge measures, assuming the configuration stays in the nondegenerate tetrahedral cone.

background

In discrete gravity the Regge action sums deficit angle times hinge measure over codimension-2 hinges. Recognition Science induces edge lengths from a conformal chart on a scalar vertex potential: each edge length is fixed by averaging the potentials at its endpoints. The flat potential is the curvature-free background about which one expands.

Upstream, smoothness inputs require the conformal edge chart to remain inside the nondegenerate tetrahedral cone, arccos arguments away from $\pm 1$, and the finite Regge action smooth at flatness. Local tetrahedral Schläfli identities (Cayley-Menger and dihedral derivatives in closed form) and their sum over a finite 3D triangulation supply the cancellation structure that first variation must respect.

The module keeps a local copy of the line through the flat potential so the first-variation development does not depend on second-variation scaffolding. Sibling material covers single-coordinate updates, Fréchet derivatives of multi-edge maps, and $C^\infty$ regularity of dihedral denominator, cosine-squared, and angle maps at nondegenerate points.

proof idea

Toolkit module, not one monolithic theorem. It defines the affine line through the flat potential and proves conformal squared-edge maps are differentiable along that line at zero. Derivatives are pushed through the dihedral chain (denominator, cosine-squared, angle) by contDiff and HasDerivAt lemmas under nondegeneracy. Multi-edge Fréchet derivatives reduce to single-edge updates via continuous-linear-map sum identities. Hinge-measure directional derivatives assemble from the edge and angle pieces. Upstream Schläfli modules feed the closed-form local identities; smoothness modules feed the cone hypotheses that keep every intermediate map smooth at the flat point.

why it matters in Recognition Science

The linear term is required before any second-variation or cubic-remainder analysis of the nonlinear Regge action. ReggeActionSecondVariation imports this module to state those higher-order targets in usable form while the full Cayley-Menger/arccos expansion is still being materialized. Gravity.TensorShearSector reuses the conformal-potential calculus when leaving the pure scalar Track 1.B ansatz toward shear and transverse-traceless modes. FreudenthalCubeTriangulation consumes the incidence and derivative bookkeeping on the standard six-tetrahedron cube.

In the RS geometry stack these derivatives sit under the discrete Einstein-Hilbert sector that must match continuum weak-field GR in three spatial dimensions (forcing step T8). They do not by themselves close the continuum limit or the full metric sector.

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)