module module

`IndisputableMonolith.Gravity.Analysis.SRSTTFirstVariation4D`

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 (1)

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

IndisputableMonolith.Gravity.Analysis.SRSTTFirstVariation4DAudit module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.Analysis.SRSConvergesEH4D module_import

declarations in this module (36)

abbrev Mat4 L46
abbrev Wave4 L47
abbrev CouplingIdx L48
def frobeniusPairing4D L53
theorem frobeniusNormSq_eq_pairing_self L56
theorem edgeStrain_add L59
theorem edgeStrain_smul L79
theorem edgeStrain_neg L94
theorem edgeStrain_sub L98
def couplingWeightCross L105
def couplingWeightCrossIdx L110
def exactMidpointBlochFirstVariation L119
theorem exactMidpointBlochSymbol_eq_irred L123
theorem exactMidpointBlochFirstVariation_eq_irred L129
theorem couplingWeight_line L137
theorem couplingWeightIdx_line L154
theorem weightFn_line L162
theorem exactMidpointBlochSymbol_line L169
theorem hasDerivAt_affine_quad L205
theorem hasDerivAt_exactMidpointBlochSymbol_line L225
theorem exactMidpointBlochFirstVariation_polarization L243
theorem IsSymmetric_add L269
theorem IsSymmetric_sub L274
theorem IsTraceless_add L279
theorem IsTraceless_sub L285
theorem IsTransverse_add L291
theorem IsTransverse_sub L298
theorem IsTT_add L305
theorem IsTT_sub L310
theorem frobeniusPairing4D_polarization L317
theorem continuumFace_polarization_eq_neg_quarter_frobenius L343
theorem momentumNormSq_torus_ne_zero L352
theorem hasDerivAt_finiteExactMidpointBlochSymbol_normalized L363
theorem continuumTTFirstVariation_closed L379
def SRSTTFirstVariation4DCert L451
theorem srsTTFirstVariation4D_cert L471