module module moderate

`IndisputableMonolith.Gravity.Analysis.ReggeTTDerivativeGate`

First-derivative gate for the Regge TT continuum symbol on the flat background. It packages unit-Frobenius TT polarizations, their existence from transverse frames, elementary 3-vector sum identities, and the plane-wave profile identification with the true nonlinear Regge action. Gate A1 and Gate A2 import the module and never re-prove the first-jet structure.

claimOn the flat Regge background, the first variation of the true nonlinear action along TT plane-wave profiles is gated; every TT polarization $H$ satisfies $\|H\|_F^2=1$; and for every nonzero wavevector there exist orthonormal transverse pairs realizing such an $H$.

background

Part of the QG full-theory campaign under the ReggeTTContinuumSymbol program (Stage 1). Upstream preflight fixes the true nonlinear Regge action, its flat point, the frozen-model identification, and the TT Bloch symbol object.

A TT polarization is a symmetric traceless transverse tensor mode for a wavevector $k$. The fourth conjunct of that predicate is unit Frobenius norm: $|H|_F^2=1$. The module also records planar and axial transverse frame constructors and the elementary $\mathbb{R}^3$ sum identities (squared norms, orthogonality, dots) used to check those frames.

The plane-wave action profile is identified with the true Regge action so that later continuum-symbol work can differentiate a single concrete functional rather than a family of discrete approximations.

proof idea

Not a single theorem: a small library of audit lemmas. Frobenius-square unity is a direct expansion of the TT predicate. Existence of TT polarizations is obtained by building planar or axial orthonormal transverse pairs and invoking the constructor that turns such a pair into an IsTTPolarization. The three-vector sum lemmas are short algebraic reductions. The plane-wave profile equality is a definitional or one-line identification with the true Regge action supplied by preflight. No second-variation or continuum-limit argument lives here.

why it matters in Recognition Science

Supplies the reusable first-derivative structure at flat for the panel-locked protocol "Normalization-Gated Schläfli Two-Jet". Downstream Gate A1 (ReggeTTLocalSymbolExistence) and Gate A2 (ReggeTTFlatSecondVariation) both import this module and, per their docs, reuse the first-derivative gate and never re-prove it. Without unit-norm TT frames and the action-profile identification, the Schläfli-reduced two-jet and local symbol existence claims have no normalized linearization to expand. Sits after symbol preflight and before any second-variation or continuum-symbol existence work.

scope and limits

Does not compute or sign the second variation (Gate A2).
Does not prove local continuum-symbol existence (Gate A1).
Does not treat curved backgrounds or non-TT modes.
Does not derive the true nonlinear Regge action (preflight).
Does not address continuum $N\to\infty$ limits or dispersion relations.

used by (2)

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

IndisputableMonolith.Gravity.Analysis.ReggeTTFlatSecondVariation module_import
IndisputableMonolith.Gravity.Analysis.ReggeTTLocalSymbolExistence module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.Analysis.ReggeTTSymbolPreflight module_import

declarations in this module (39)

theorem planeWaveActionProfile_eq_trueReggeAction L108
theorem ttPolarization_frobeniusSq_eq_one L124
theorem sum3_div_sq L128
theorem sum3_div_orth L137
theorem sum3_dot_div L143
theorem isTTPolarization_of_orthonormal_transverse_pair L153
def planarTransverse1 L187
def planarTransverse2 L195
def axialTransverse1 L207
def axialTransverse2 L213
theorem exists_isTTPolarization L223
theorem exists_isTTPolarization_of_ne_zero L258
def flatAngleJacobian L277
def flatSqrtEdgeDeriv L282
structure FlatReggeStencil L288
def flatReggeStencilMoment L298
theorem stencil_ordering_grounded L307
theorem hasDerivAt_sqrt_flatEdge L317
theorem flatCos L328
theorem flatCos_value_cases L352
theorem flatCos_bounds L365
theorem flatCos_ne_endpoints L374
theorem flat_cofactorProduct_pos L382
theorem flat_denom_ne_zero L393
theorem flat_nondegeneracy_eventually L410
theorem flatAngleJacobian_eq_dihedralClosedDerivSq L480
theorem flatAngleJacobian_schlaefli L489
theorem hasDerivAt_flatAngle_directional L498
theorem hasDerivAt_flatSqrtEdge_directional L541
theorem hasDerivAt_flatWeightedAngleSum L568
def flatArccosFactor L639
theorem inv_sqrt_half L647
theorem inv_sqrt_three_quarters L652
theorem arccosFactor L659
theorem flatArccosFactor_spec L687
theorem flatAngleJacobian_cofactor_form L702
theorem flatAngleJacobian_row0_norm L715
def flatAngleJacobianRow0 L738
theorem flatAngleJacobian_row0_eval L750