module module moderate

`IndisputableMonolith.Gravity.Analysis.ReggeTTFlatSecondVariation`

Analytic second-variation toolkit for the Regge action at a flat background under transverse-traceless plane-wave edge data. It packages directional derivatives of edge lengths, dihedral angles, hinge contributions, and deficit angles along affine paths that stay good at the flat point. Continuum-symbol and Bloch-interface audits cite it when they need Gate-level differentiability rather than formal stencil algebra. The development is mostly HasDerivAt chaining from elementary sqrt and cosine slopes.

claimAt a flat Regge background, for each edge $e$ with plane-wave coefficient $c_e = a_e\cos(k\cdot x_{\mathrm{mid}}(e))$, the module supplies the affine slopes of $\sqrt{\ell_e}$, of slot dihedral angles, of hinge contributions, and of deficit angles along admissible paths $\gamma$, together with a predicate $\mathrm{PathGoodAt}(\gamma,0)$ ensuring those derivatives exist at the flat point $t=0$.

background

This file sits in the QG full-theory campaign's ReggeTTContinuumSymbol program, after Stage-1 preflight (true nonlinear action, flat point, frozen-model identification, TT Bloch symbol object) and beside the Stage-2 derivative gate and the Gate-A1 local-symbol existence lane.

Regge calculus replaces the Einstein-Hilbert integrand by edge lengths and deficit angles on a triangulation. The second variation at a flat configuration is the discrete analogue of the Lichnerowicz operator on TT tensors; continuum-symbol extraction needs those derivatives under plane-wave edge data, not merely formal stencils.

Upstream modules lock the nonlinear action and the gates that authorize differentiation. Here the local objects are edge coefficients, sqrt-edge slopes, directional angle derivatives, contribution derivatives, deficit derivatives, and the PathGoodAt predicate that certifies a path is admissible at the flat point.

proof idea

The module is a layered derivative library, not a single theorem. Elementary pieces record the affine slope of a plane-wave edge value and the chain rule through square root. Angle and slot-angle derivatives are obtained by directional HasDerivAt along the path. Contribution and deficit derivatives compose those angle slopes with the Regge hinge weights. PathGoodAt packages the open conditions needed at $t=0$; pathGoodAt_zero discharges the flat basepoint. Most claims are short HasDerivAt wrappers or algebraic identifications with the frozen plane-wave velocity on matched slots.

why it matters in Recognition Science

Continuum TT symbol extraction for Regge gravity needs a justified second jet at the flat point before any Bloch or stencil audit can be non-tautological. This module supplies that jet: edge, angle, contribution, and deficit derivatives under plane-wave data.

It is imported by the Regge TT Bloch interface audit (panel-locked C11 surface), which deliberately keeps the first gate narrow so raw cell stencils are not definitionally wired to the objects they audit. Together with the derivative gate and local-symbol existence modules, it closes the analytic half of the Normalization-Gated Schläfli two-jet protocol used in the continuum-symbol program.

scope and limits

Does not prove continuum limit of the discrete TT symbol, only flat-point derivatives.
Does not treat curved backgrounds or non-plane-wave edge data.
Does not discharge Bloch-interface or stencil audits; those import this module.
Does not claim global path existence beyond the PathGoodAt predicate at t=0.
Does not fix normalization constants of the continuum symbol by itself.

used by (1)

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

IndisputableMonolith.Gravity.Analysis.ReggeTTBlochInterfaceAudit module_import

depends on (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.Analysis.ReggeTTDerivativeGate module_import
IndisputableMonolith.Gravity.Analysis.ReggeTTLocalSymbolExistence module_import
IndisputableMonolith.Gravity.Analysis.ReggeTTSymbolPreflight module_import

declarations in this module (37)

def edgeCoeff L110
def edgeSqrtDeriv L116
theorem hasDerivAt_edgeValue L122
theorem hasDerivAt_sqrtEdge L137
theorem hasDerivAt_angle_directional L161
def slotAngleDeriv L206
theorem hasDerivAt_slotAngle L217
def contribDeriv L263
theorem hasDerivAt_contrib L270
def deficitDeriv L291
def PathGoodAt L297
theorem pathGoodAt_zero L311
theorem eventually_pathGoodAt L329
theorem hasDerivAt_deficit L369
def firstVariationIntegrand L392
theorem hasDerivAt_planeWaveActionProfile L402
theorem slotMatch_mul L430
theorem sum_edges_slotMatch L441
theorem sum_sqrt_slotAngleDeriv_eq_zero L504
theorem sum_sqrt_deficitDeriv_eq_zero L544
theorem deficit_planeWave_zero L602
theorem firstVariationIntegrand_zero L611
theorem trueReggeAction_firstVariation_flat_eq_zero L632
def flatSlotSqrtDeriv L642
def flatSlotAngleDeriv L648
theorem edgeSqrtDeriv_localEdge_zero L655
theorem slotAngleDeriv_zero L666
theorem sum_edgeSqrtDeriv_deficitDeriv_flat L675
def reducedFirstVariation L733
theorem firstVariationIntegrand_eq_reduced L741
theorem deriv_actionProfile_eventuallyEq_reduced L750
theorem edgeSqrtDeriv_differentiableAt L761
theorem hasDerivAt_reducedFirstVariation_flat L780
theorem trueReggeAction_secondVariation_flat_schlaefli L825
def axisReducedSecondVariation L846
theorem axisReducedSecondVariation_applies L856
theorem planeWave_TTBlochSymbolIs_reduced L870