IndisputableMonolith.Gravity.Analysis.RecognitionMeshExactJBridge4D

declarations in this module (33)

• abbrev Mat4 L64
• abbrev Wave4 L65
• theorem frobeniusNormSq_preflight_eq_identity L67
• theorem waveNormSq_preflight_eq_identity L72
• structure RecognitionFreudenthalMesh4D L82
• def canonicalRecognitionMesh L98
• theorem canonicalRecognitionMesh_side L101
• def meshWave L107
• def meshTrueReggeQuadraticHessian L115
• def trueReggeZeroMomHessian L121
• def exactJActionOnMesh L132
• theorem exactJActionOnMesh_eq L136
• theorem exactJActionOnMesh_at_zero L141
• def exactJSecondDiff L148
• theorem exactJSecondDiff_eq_meshHessian L156
• theorem exactJSecondDiff_independent_of_amplitude L167
• def ExactJAmplitudeHessianExists L178
• theorem exactJAmplitudeHessian_eq_mesh L185
• def ExactJEqualsTrueReggeHessian L199
• theorem exactJEqualsTrueReggeHessian_holds L209
• def RecognitionExactJConvergesEH L218
• theorem momentumNormSq_ne_zero_of_mode L231
• theorem torusSide_pos L254
• theorem recognitionExactJConvergesEH_of_normalized_mesh L264
• def RecognitionExactJConvergesGaugeZero L283
• theorem recognitionExactJConvergesEH_closed L295
• theorem recognitionExactJConvergesGaugeZero_closed L335
• def FactorizedMomentEqualsEH L356
• theorem decoy_pullback_excluded L364
• structure RecognitionMeshExactJBridge4DStatus L369
• def recognitionMeshExactJBridge4DStatus L381
• theorem recognitionMeshExactJBridge4DStatus_flags L390
• theorem recognition_iterated_eh_closed L401