Pith. sign in
module module moderate

IndisputableMonolith.Geometry.ReggeActionSecondVariation

show as:
view Lean formalization →

Records the second variation of the nonlinear Regge action along affine lines through the flat conformal potential. It identifies the directional second derivative at the flat point with the canonical incidence Hessian and packages the named analytic inputs that make that equality hold. Geometry and gravity modules cite it when closing the Hessian chain and the discrete vacuum Einstein equivalence. The module is mostly definitions and interface theorems, not a full expanded derivative calculation.

claimAlong the line $t \mapsto \phi_0 + t\xi$ through the flat conformal potential $\phi_0$, the second directional derivative of the nonlinear Regge action at $t=0$ equals the canonical Hessian quadratic form $H(\xi,\xi)$. Remainder contributions are required to have vanishing second variation at zero. The equality is stated under a named second-variation input assembled from directional data.

background

Regge calculus replaces smooth curvature by deficit angles on hinges of a simplicial complex, with edge lengths (or a conformal potential on edges) as the dynamical variables. The nonlinear Regge action is the full deficit-weighted area functional, not its linearized weak-field truncation.

The upstream first-variation module states that the first variation of this action vanishes at the flat conformal potential: the geometric content is Schläfli cancellation together with zero deficit on every hinge. That module records the exact analytic claim and the named input needed until local Schläfli identities are fully expanded.

This second-variation module works in the same conformal setting. It introduces the affine line through the flat potential in a direction $\xi$, the restriction of the action to that line, a canonical Hessian quadratic form built from incidence data, and predicate packages that assert existence of the second derivative at $t=0$ and match it to that quadratic form.

proof idea

Definition-and-interface module rather than a long tactic proof. It defines the line through the flat potential, the action restricted to that line, and the canonical Hessian quadratic evaluated on the direction. It records HasSecondDerivAt-style predicates and shows the Hessian quadratic along the line has second derivative zero at the base point when the direction is varied in the expected way.

Named input structures bundle the directional second-variation hypotheses. Constructor lemmas turn a directional second-variation assumption into that input package. The main interface theorem equates the Regge action's second variation at the flat point with the canonical Hessian, and a parallel package handles remainder terms whose second variation vanishes at zero. No full chain-rule expansion of the nonlinear action is performed here; that is deferred downstream.

why it matters in Recognition Science

Closes the second rung of the Regge variational ladder after first-variation vanishing. Downstream, the nonlinear Hessian proof interface isolates the hard claim that the second directional derivative at the flat potential equals the canonical incidence Hessian; this module supplies the exact endpoint language and input shape for that calculation.

Discrete vacuum Einstein for the nonlinear action uses the same conformal edge-incidence derivative: forward vacuum (zero deficit) follows from Schläfli plus flatness, while the reverse needs rank or nondegeneracy of that derivative. Second-variation control feeds that nondegeneracy story.

The cubic-lattice limit module isolates the regular weak-field $O(a^2)$ action estimate for the canonical second-order Regge action; the Hessian identification here is the continuum-facing quadratic form that limit compares against. In the broader Recognition geometry stack, this is infrastructure for discrete Einstein and continuum recovery, not a forcing-chain (T0–T8) step.

scope and limits

used by (3)

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

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (18)