IndisputableMonolith.Gravity.Analysis.ReggeExactMidpointM2TTIdentity4DKernelCert

declarations in this module (46)

• structure CZ L22
• def toCZ L39
• def De L44
• def Dep L46
• def D2 L48
• def contrib L51
• def czChunk0 L55
• def czChunk1 L137
• def czChunk2 L219
• def czChunk3 L301
• def czChunk4 L383
• def czChunk5 L465
• def czChunk6 L547
• def czChunk7 L629
• def czChunk8 L711
• def czChunk9 L793
• def czChunk10 L875
• def czChunk11 L957
• def czChunk12 L1039
• def czChunk13 L1121
• def czChunk14 L1203
• def czChunk15 L1285
• theorem czChunk0_bridge L1295
• theorem czChunk1_bridge L1299
• theorem czChunk2_bridge L1303
• theorem czChunk3_bridge L1307
• theorem czChunk4_bridge L1311
• theorem czChunk5_bridge L1315
• theorem czChunk6_bridge L1319
• theorem czChunk7_bridge L1323
• theorem czChunk8_bridge L1327
• theorem czChunk9_bridge L1331
• theorem czChunk10_bridge L1335
• theorem czChunk11_bridge L1339
• theorem czChunk12_bridge L1343
• theorem czChunk13_bridge L1347
• theorem czChunk14_bridge L1351
• theorem czChunk15_bridge L1355
• def couplingZList L1359
• theorem couplingZList_bridge L1364
• def m2Num L1374
• def explicitZ L1377
• def closedZ L1740
• def sym4Z L1746
• def symFullZ L1750
• theorem symFullZ_explicit_eq_closed L1754