IndisputableMonolith.Geometry.ReggeActionNonlinearHessianProof
Exact second directional variation of the full nonlinear Regge action along a line in vertex-potential space. Discrete-gravity and Regge-calculus workers cite it when the Hessian of the action, not just its linearization, is needed. The argument splits the action along a line into a canonical quadratic piece plus remainder, then discharges the Hessian identity from first-order tangency or near-zero linearization hypotheses.
claimAlong a line $t \mapsto q + t\,v$ in vertex-potential space, the nonlinear Regge action admits the exact second-directional-variation identity $S(q+tv)=S(q)+t\,DS_q(v)+\tfrac12 t^2 H_S(q)(v,v)+R(t)$, where the quadratic term is the directional Hessian and $R$ is the cubic-scale remainder. Equivalent formulations package the same fact as first-order tangency of the action derivative or as linearization of that derivative near zero.
background
Regge calculus replaces smooth spacetime by a simplicial complex whose geometry is carried by edge lengths (or dual vertex potentials). The nonlinear Regge action $S$ is built from deficit angles and volumes; both depend on the Cayley–Menger determinants and on $\arccos$ of dihedral data, so second derivatives are a long chain-rule expansion.
The parent module ReggeActionSecondVariation records the usable targets: a nonlinear second-variation identity and a cubic-remainder bound, with the heavy Cayley–Menger/$\arccos$ calculus left in named input structures until fully expanded. The present module supplies the exact directional-Hessian statement those targets presuppose.
Working objects are the restriction of $S$ to an affine line, its canonical quadratic part (the directional Hessian form), and the residual remainder along that line. Auxiliary calculus facts (eventual differentiability from $C^\infty$, second derivative of a constant shift) support the 1D reductions.
proof idea
The module is organized around a 1D split and two equivalent analytic interfaces.
First, actionAlongLine_canonical_split decomposes the restricted action into canonicalQuadraticAlongLine plus canonicalRemainderAlongLine. Differentiability lemmas (differentiableAt_eventually_of_contDiffAt_top, deriv_differentiableAt_of_contDiffAt_top, hasSecondDerivAt_const_add) justify passing derivatives through that split.
Two named targets then encode the same Hessian claim: ActionDerivativeFirstOrderTangencyTarget (the derivative of $S$ is tangent to its linear part at first order) and ActionDerivativeLinearizationNearZeroTarget (linearization of the action derivative near the base point). Bridge lemmas show each target implies the nonlinear directional Hessian, and that near-zero linearization yields first-order tangency. The headline NonlinearReggeDirectionalHessianTheorem packages the resulting exact second-variation identity.
why it matters in Recognition Science
Without an exact directional Hessian for the full nonlinear action, cubic remainder estimates cannot be stated cleanly. Downstream, ReggeActionCubicTaylorBound isolates the final local third-order Taylor bound in finite-dimensional vertex-potential space; its doc-comment says that bound is needed "after the nonlinear Hessian has been identified." This module is that identification step.
In the broader Recognition geometry stack, controlling the second variation of the discrete action is the bridge from kinematic simplex data to dynamical stability and to continuum limits. The module does not itself close the Cayley–Menger expansion; it freezes the Hessian claim so the cubic Taylor work can proceed against a fixed interface.
scope and limits
- Does not expand the Cayley–Menger or arccos chain rule; those remain named analytic inputs.
- Does not prove a global Hessian on the full edge-length manifold, only directional second variation along affine lines.
- Does not supply the cubic remainder bound; that is deferred to ReggeActionCubicTaylorBound.
- Does not address continuum or smooth-limit recovery of the Einstein–Hilbert second variation.
- Does not claim uniqueness of the quadratic form beyond the directional identity along lines.
used by (1)
depends on (1)
declarations in this module (142)
-
theorem
differentiableAt_eventually_of_contDiffAt_top -
theorem
deriv_differentiableAt_of_contDiffAt_top -
theorem
hasSecondDerivAt_const_add -
def
NonlinearReggeDirectionalHessianTheorem -
def
ActionDerivativeLinearizationNearZeroTarget -
def
ActionDerivativeFirstOrderTangencyTarget -
theorem
nonlinearDirectionalHessian_of_actionDerivativeFirstOrderTangency -
theorem
nonlinearDirectionalHessian_of_actionDerivativeLinearizationNearZero -
theorem
actionDerivativeFirstOrderTangency_of_linearizationNearZero -
def
canonicalQuadraticAlongLine -
def
canonicalRemainderAlongLine -
theorem
actionAlongLine_canonical_split -
theorem
canonicalRemainderAlongLine_eq_action_sub_quadratic -
theorem
canonicalQuadraticAlongLine_hasSecondDerivAt_zero -
theorem
canonicalQuadraticAlongLine_differentiableAt -
theorem
canonicalQuadraticAlongLine_hasDerivAt -
theorem
deriv_canonicalQuadraticAlongLine -
def
ActionDerivativeTangencyToQuadraticTarget -
theorem
actionDerivativeFirstOrderTangency_of_quadraticTangency -
def
hingeLineDeriv -
def
deficitLineDeriv -
def
hingeLineSecondDeriv -
def
deficitLineSecondDeriv -
def
reggeActionProductRuleDerivative -
def
reggeActionSecondProductRuleDerivative -
def
ActionDerivativeProductRuleNearZeroTarget -
def
HingeDeficitLineDifferentiabilityNearZeroTarget -
def
HingeDeficitSecondLineDifferentiabilityAtZeroTarget -
theorem
hingeLineDeriv_differentiableAt_zero -
def
DeficitSecondLineDifferentiabilityAtZeroTarget -
theorem
hingeDeficitSecondLineDifferentiability_of_deficit -
theorem
hingeLine_contDiffAt_zero -
theorem
deficitLine_contDiffAt_zero_of_flatConfiguration -
theorem
deficitLineDeriv_differentiableAt_zero_of_flatConfiguration -
theorem
hingeDeficitSecondLineDifferentiabilityAtZero_of_flatConfiguration -
theorem
hingeDeficitLineDifferentiabilityNearZero_of_flatConfiguration -
theorem
actionDerivativeProductRuleNearZero_of_factorDifferentiability -
theorem
actionDerivativeProductRuleNearZero_of_flatConfiguration -
theorem
productRule_hasDerivAt_secondProduct -
def
SecondProductRuleEqualsCanonicalHessianTarget -
def
SecondSchlaefliAlongLineTarget -
def
MixedHingeDeficitCanonicalHessianTarget -
theorem
hingeLineDeriv_zero_eq_directional -
theorem
deficitLineDeriv_zero_eq_deficitPackage -
def
MixedHingeDeficitFromDeficitPackageTarget -
def
MixedHingeDeficitDirichletTarget -
theorem
mixedHingeDeficitFromDeficitPackage_of_dirichlet -
def
MixedHingeDeficitEdgeStencilTarget -
theorem
mixedHingeDeficitDirichlet_of_edgeStencil -
theorem
mixedHingeDeficitFromDeficitPackage_of_edgeStencil -
theorem
mixedHingeDeficitCanonicalHessian_of_deficitPackage -
theorem
mixedHingeDeficitCanonicalHessian_of_edgeStencil -
def
WeightedDeficitDerivativeStationaryTarget -
def
WeightedDeficitDerivativeEventuallyZeroTarget -
theorem
weightedDeficitDerivativeStationary_of_eventuallyZero -
def
ConformalSchlaefliAlongLineTarget -
def
LocalConformalSchlaefliAlongLineTarget -
def
ConformalSchlaefliAlongLineExpansionTarget -
def
LocalConformalSchlaefliNearZeroTarget -
def
LocalConformalSchlaefliAngleSqEdgeChainRuleNearZeroTarget -
def
LocalConformalSchlaefliClosedFormZeroNearZeroTarget -
theorem
conformalLocalSqEdge_line_pos -
theorem
cm3_conformalTetSqEdges_line_pos_eventually -
theorem
localConformalSchlaefliClosedFormZeroNearZero -
theorem
dihedralCos3Sq_conformalTetSqEdges_line_endpoint_free_eventually -
theorem
conformalTetSqEdges_hasDerivAt_line -
theorem
localConformalSchlaefliAngleSqEdgeChainRuleNearZero_of_flatConfiguration -
theorem
localConformalSchlaefliNearZero_of_sqEdgeChainRule_and_closedFormZero -
def
ConformalSchlaefliNearZeroExpansionTarget -
def
LocalDihedralAngleLineDifferentiabilityNearZeroTarget -
theorem
tetDihedralAngleUnderConformal_line_contDiffAt_zero_of_flatConfiguration -
theorem
localDihedralAngleLineDifferentiabilityNearZero_of_flatConfiguration -
theorem
hingeMeasureUnderConformal_eq_local_sqrt_of_incident -
theorem
incidenceEdgeSlotPartition_edge_sum_for_tet_conformal -
theorem
incidenceEdgeSlotPartition_sum_match_conformal -
theorem
deficitLineDeriv_eq_neg_sum_local_nearZero -
theorem
conformalSchlaefliNearZeroExpansion_of_angleDiff_and_partition -
theorem
weightedDeficitDerivativeEventuallyZero_of_nearZeroExpansion_and_local -
theorem
weightedDeficitDerivativeStationary_of_nearZeroExpansion_and_local -
theorem
conformalSchlaefliAlongLine_of_expansion_and_local