module module

`IndisputableMonolith.Gravity.Analysis.ReggeExactMidpointM2TTIdentity4DKernelGlue`

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.ReggeExactMidpointM2TTIdentity4D module_import

depends on (4)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.Analysis.ReggeExactFlatHessianBlochData4D module_import
IndisputableMonolith.Gravity.Analysis.ReggeExactFlatHessianBlochSymbol4D module_import
IndisputableMonolith.Gravity.Analysis.ReggeExactMidpointM2TTIdentity4DKernelCert module_import
IndisputableMonolith.Gravity.Analysis.ReggeExactMidpointM2TTIdentity4DM2NumAssemble module_import

declarations in this module (17)

def m2CoeffSum L28
def explicitM2CoeffZ L37
def closedCoeffZ L41
theorem toCZ_De L44
theorem toCZ_Dep L47
theorem toCZ_D2 L50
theorem termQ_eq_contrib_div L54
theorem cz_den_dvd_sixteen L70
theorem coupling_den_dvd_sixteen L75
theorem sum_map_contrib_eq_m2Num L83
theorem toList_sum_eq_finset_sum L93
theorem m2CoeffSum_eq_m2Num_div L108
theorem m2CoeffSum_eq_explicitM2CoeffZ L145
theorem closedCoeff_eq_closedCoeffZ L154
theorem sym4_scale L166
theorem symFull_scale L177
theorem symFullZ_rat_explicit_eq_closed L190