module module

`IndisputableMonolith.Gravity.Analysis.ReggeTTDerivativeGate`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

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