IndisputableMonolith.Gravity.Analysis.ReggeExactMidpointM2TTIdentity4DM2NumChunk07

   1import Mathlib
   2import IndisputableMonolith.Gravity.Analysis.ReggeExactMidpointM2TTIdentity4DKernelCert
   3
   4/-! m2Num = 8·explicitZ, chunk 7 (256 kernel decides). -/
   5
   6namespace IndisputableMonolith
   7namespace Gravity
   8namespace Analysis
   9namespace ReggeExactMidpointM2TTIdentity4D
  10namespace M2NumChunk07
  11
  12open KernelCert
  13
  14set_option maxRecDepth 100000
  15set_option maxHeartbeats 200000000
  16
  17theorem e_130000 : m2Num 1 3 0 0 0 0 = 8 * explicitZ 1 3 0 0 0 0 := by decide
  18theorem e_130001 : m2Num 1 3 0 0 0 1 = 8 * explicitZ 1 3 0 0 0 1 := by decide
  19theorem e_130002 : m2Num 1 3 0 0 0 2 = 8 * explicitZ 1 3 0 0 0 2 := by decide
  20theorem e_130003 : m2Num 1 3 0 0 0 3 = 8 * explicitZ 1 3 0 0 0 3 := by decide
  21theorem e_130010 : m2Num 1 3 0 0 1 0 = 8 * explicitZ 1 3 0 0 1 0 := by decide
  22theorem e_130011 : m2Num 1 3 0 0 1 1 = 8 * explicitZ 1 3 0 0 1 1 := by decide
  23theorem e_130012 : m2Num 1 3 0 0 1 2 = 8 * explicitZ 1 3 0 0 1 2 := by decide
  24theorem e_130013 : m2Num 1 3 0 0 1 3 = 8 * explicitZ 1 3 0 0 1 3 := by decide
  25theorem e_130020 : m2Num 1 3 0 0 2 0 = 8 * explicitZ 1 3 0 0 2 0 := by decide
  26theorem e_130021 : m2Num 1 3 0 0 2 1 = 8 * explicitZ 1 3 0 0 2 1 := by decide
  27theorem e_130022 : m2Num 1 3 0 0 2 2 = 8 * explicitZ 1 3 0 0 2 2 := by decide
  28theorem e_130023 : m2Num 1 3 0 0 2 3 = 8 * explicitZ 1 3 0 0 2 3 := by decide
  29theorem e_130030 : m2Num 1 3 0 0 3 0 = 8 * explicitZ 1 3 0 0 3 0 := by decide
  30theorem e_130031 : m2Num 1 3 0 0 3 1 = 8 * explicitZ 1 3 0 0 3 1 := by decide
  31theorem e_130032 : m2Num 1 3 0 0 3 2 = 8 * explicitZ 1 3 0 0 3 2 := by decide
  32theorem e_130033 : m2Num 1 3 0 0 3 3 = 8 * explicitZ 1 3 0 0 3 3 := by decide
  33theorem e_130100 : m2Num 1 3 0 1 0 0 = 8 * explicitZ 1 3 0 1 0 0 := by decide
  34theorem e_130101 : m2Num 1 3 0 1 0 1 = 8 * explicitZ 1 3 0 1 0 1 := by decide
  35theorem e_130102 : m2Num 1 3 0 1 0 2 = 8 * explicitZ 1 3 0 1 0 2 := by decide
  36theorem e_130103 : m2Num 1 3 0 1 0 3 = 8 * explicitZ 1 3 0 1 0 3 := by decide
  37theorem e_130110 : m2Num 1 3 0 1 1 0 = 8 * explicitZ 1 3 0 1 1 0 := by decide
  38theorem e_130111 : m2Num 1 3 0 1 1 1 = 8 * explicitZ 1 3 0 1 1 1 := by decide
  39theorem e_130112 : m2Num 1 3 0 1 1 2 = 8 * explicitZ 1 3 0 1 1 2 := by decide
  40theorem e_130113 : m2Num 1 3 0 1 1 3 = 8 * explicitZ 1 3 0 1 1 3 := by decide
  41theorem e_130120 : m2Num 1 3 0 1 2 0 = 8 * explicitZ 1 3 0 1 2 0 := by decide
  42theorem e_130121 : m2Num 1 3 0 1 2 1 = 8 * explicitZ 1 3 0 1 2 1 := by decide
  43theorem e_130122 : m2Num 1 3 0 1 2 2 = 8 * explicitZ 1 3 0 1 2 2 := by decide
  44theorem e_130123 : m2Num 1 3 0 1 2 3 = 8 * explicitZ 1 3 0 1 2 3 := by decide
  45theorem e_130130 : m2Num 1 3 0 1 3 0 = 8 * explicitZ 1 3 0 1 3 0 := by decide
  46theorem e_130131 : m2Num 1 3 0 1 3 1 = 8 * explicitZ 1 3 0 1 3 1 := by decide
  47theorem e_130132 : m2Num 1 3 0 1 3 2 = 8 * explicitZ 1 3 0 1 3 2 := by decide
  48theorem e_130133 : m2Num 1 3 0 1 3 3 = 8 * explicitZ 1 3 0 1 3 3 := by decide
  49theorem e_130200 : m2Num 1 3 0 2 0 0 = 8 * explicitZ 1 3 0 2 0 0 := by decide
  50theorem e_130201 : m2Num 1 3 0 2 0 1 = 8 * explicitZ 1 3 0 2 0 1 := by decide
  51theorem e_130202 : m2Num 1 3 0 2 0 2 = 8 * explicitZ 1 3 0 2 0 2 := by decide
  52theorem e_130203 : m2Num 1 3 0 2 0 3 = 8 * explicitZ 1 3 0 2 0 3 := by decide
  53theorem e_130210 : m2Num 1 3 0 2 1 0 = 8 * explicitZ 1 3 0 2 1 0 := by decide
  54theorem e_130211 : m2Num 1 3 0 2 1 1 = 8 * explicitZ 1 3 0 2 1 1 := by decide
  55theorem e_130212 : m2Num 1 3 0 2 1 2 = 8 * explicitZ 1 3 0 2 1 2 := by decide
  56theorem e_130213 : m2Num 1 3 0 2 1 3 = 8 * explicitZ 1 3 0 2 1 3 := by decide
  57theorem e_130220 : m2Num 1 3 0 2 2 0 = 8 * explicitZ 1 3 0 2 2 0 := by decide
  58theorem e_130221 : m2Num 1 3 0 2 2 1 = 8 * explicitZ 1 3 0 2 2 1 := by decide
  59theorem e_130222 : m2Num 1 3 0 2 2 2 = 8 * explicitZ 1 3 0 2 2 2 := by decide
  60theorem e_130223 : m2Num 1 3 0 2 2 3 = 8 * explicitZ 1 3 0 2 2 3 := by decide
  61theorem e_130230 : m2Num 1 3 0 2 3 0 = 8 * explicitZ 1 3 0 2 3 0 := by decide
  62theorem e_130231 : m2Num 1 3 0 2 3 1 = 8 * explicitZ 1 3 0 2 3 1 := by decide
  63theorem e_130232 : m2Num 1 3 0 2 3 2 = 8 * explicitZ 1 3 0 2 3 2 := by decide
  64theorem e_130233 : m2Num 1 3 0 2 3 3 = 8 * explicitZ 1 3 0 2 3 3 := by decide
  65theorem e_130300 : m2Num 1 3 0 3 0 0 = 8 * explicitZ 1 3 0 3 0 0 := by decide
  66theorem e_130301 : m2Num 1 3 0 3 0 1 = 8 * explicitZ 1 3 0 3 0 1 := by decide
  67theorem e_130302 : m2Num 1 3 0 3 0 2 = 8 * explicitZ 1 3 0 3 0 2 := by decide
  68theorem e_130303 : m2Num 1 3 0 3 0 3 = 8 * explicitZ 1 3 0 3 0 3 := by decide
  69theorem e_130310 : m2Num 1 3 0 3 1 0 = 8 * explicitZ 1 3 0 3 1 0 := by decide
  70theorem e_130311 : m2Num 1 3 0 3 1 1 = 8 * explicitZ 1 3 0 3 1 1 := by decide
  71theorem e_130312 : m2Num 1 3 0 3 1 2 = 8 * explicitZ 1 3 0 3 1 2 := by decide
  72theorem e_130313 : m2Num 1 3 0 3 1 3 = 8 * explicitZ 1 3 0 3 1 3 := by decide
  73theorem e_130320 : m2Num 1 3 0 3 2 0 = 8 * explicitZ 1 3 0 3 2 0 := by decide
  74theorem e_130321 : m2Num 1 3 0 3 2 1 = 8 * explicitZ 1 3 0 3 2 1 := by decide
  75theorem e_130322 : m2Num 1 3 0 3 2 2 = 8 * explicitZ 1 3 0 3 2 2 := by decide
  76theorem e_130323 : m2Num 1 3 0 3 2 3 = 8 * explicitZ 1 3 0 3 2 3 := by decide
  77theorem e_130330 : m2Num 1 3 0 3 3 0 = 8 * explicitZ 1 3 0 3 3 0 := by decide
  78theorem e_130331 : m2Num 1 3 0 3 3 1 = 8 * explicitZ 1 3 0 3 3 1 := by decide
  79theorem e_130332 : m2Num 1 3 0 3 3 2 = 8 * explicitZ 1 3 0 3 3 2 := by decide
  80theorem e_130333 : m2Num 1 3 0 3 3 3 = 8 * explicitZ 1 3 0 3 3 3 := by decide
  81theorem e_131000 : m2Num 1 3 1 0 0 0 = 8 * explicitZ 1 3 1 0 0 0 := by decide
  82theorem e_131001 : m2Num 1 3 1 0 0 1 = 8 * explicitZ 1 3 1 0 0 1 := by decide
  83theorem e_131002 : m2Num 1 3 1 0 0 2 = 8 * explicitZ 1 3 1 0 0 2 := by decide
  84theorem e_131003 : m2Num 1 3 1 0 0 3 = 8 * explicitZ 1 3 1 0 0 3 := by decide
  85theorem e_131010 : m2Num 1 3 1 0 1 0 = 8 * explicitZ 1 3 1 0 1 0 := by decide
  86theorem e_131011 : m2Num 1 3 1 0 1 1 = 8 * explicitZ 1 3 1 0 1 1 := by decide
  87theorem e_131012 : m2Num 1 3 1 0 1 2 = 8 * explicitZ 1 3 1 0 1 2 := by decide
  88theorem e_131013 : m2Num 1 3 1 0 1 3 = 8 * explicitZ 1 3 1 0 1 3 := by decide
  89theorem e_131020 : m2Num 1 3 1 0 2 0 = 8 * explicitZ 1 3 1 0 2 0 := by decide
  90theorem e_131021 : m2Num 1 3 1 0 2 1 = 8 * explicitZ 1 3 1 0 2 1 := by decide
  91theorem e_131022 : m2Num 1 3 1 0 2 2 = 8 * explicitZ 1 3 1 0 2 2 := by decide
  92theorem e_131023 : m2Num 1 3 1 0 2 3 = 8 * explicitZ 1 3 1 0 2 3 := by decide
  93theorem e_131030 : m2Num 1 3 1 0 3 0 = 8 * explicitZ 1 3 1 0 3 0 := by decide
  94theorem e_131031 : m2Num 1 3 1 0 3 1 = 8 * explicitZ 1 3 1 0 3 1 := by decide
  95theorem e_131032 : m2Num 1 3 1 0 3 2 = 8 * explicitZ 1 3 1 0 3 2 := by decide
  96theorem e_131033 : m2Num 1 3 1 0 3 3 = 8 * explicitZ 1 3 1 0 3 3 := by decide
  97theorem e_131100 : m2Num 1 3 1 1 0 0 = 8 * explicitZ 1 3 1 1 0 0 := by decide
  98theorem e_131101 : m2Num 1 3 1 1 0 1 = 8 * explicitZ 1 3 1 1 0 1 := by decide
  99theorem e_131102 : m2Num 1 3 1 1 0 2 = 8 * explicitZ 1 3 1 1 0 2 := by decide
 100theorem e_131103 : m2Num 1 3 1 1 0 3 = 8 * explicitZ 1 3 1 1 0 3 := by decide
 101theorem e_131110 : m2Num 1 3 1 1 1 0 = 8 * explicitZ 1 3 1 1 1 0 := by decide
 102theorem e_131111 : m2Num 1 3 1 1 1 1 = 8 * explicitZ 1 3 1 1 1 1 := by decide
 103theorem e_131112 : m2Num 1 3 1 1 1 2 = 8 * explicitZ 1 3 1 1 1 2 := by decide
 104theorem e_131113 : m2Num 1 3 1 1 1 3 = 8 * explicitZ 1 3 1 1 1 3 := by decide
 105theorem e_131120 : m2Num 1 3 1 1 2 0 = 8 * explicitZ 1 3 1 1 2 0 := by decide
 106theorem e_131121 : m2Num 1 3 1 1 2 1 = 8 * explicitZ 1 3 1 1 2 1 := by decide
 107theorem e_131122 : m2Num 1 3 1 1 2 2 = 8 * explicitZ 1 3 1 1 2 2 := by decide
 108theorem e_131123 : m2Num 1 3 1 1 2 3 = 8 * explicitZ 1 3 1 1 2 3 := by decide
 109theorem e_131130 : m2Num 1 3 1 1 3 0 = 8 * explicitZ 1 3 1 1 3 0 := by decide
 110theorem e_131131 : m2Num 1 3 1 1 3 1 = 8 * explicitZ 1 3 1 1 3 1 := by decide
 111theorem e_131132 : m2Num 1 3 1 1 3 2 = 8 * explicitZ 1 3 1 1 3 2 := by decide
 112theorem e_131133 : m2Num 1 3 1 1 3 3 = 8 * explicitZ 1 3 1 1 3 3 := by decide
 113theorem e_131200 : m2Num 1 3 1 2 0 0 = 8 * explicitZ 1 3 1 2 0 0 := by decide
 114theorem e_131201 : m2Num 1 3 1 2 0 1 = 8 * explicitZ 1 3 1 2 0 1 := by decide
 115theorem e_131202 : m2Num 1 3 1 2 0 2 = 8 * explicitZ 1 3 1 2 0 2 := by decide
 116theorem e_131203 : m2Num 1 3 1 2 0 3 = 8 * explicitZ 1 3 1 2 0 3 := by decide
 117theorem e_131210 : m2Num 1 3 1 2 1 0 = 8 * explicitZ 1 3 1 2 1 0 := by decide
 118theorem e_131211 : m2Num 1 3 1 2 1 1 = 8 * explicitZ 1 3 1 2 1 1 := by decide
 119theorem e_131212 : m2Num 1 3 1 2 1 2 = 8 * explicitZ 1 3 1 2 1 2 := by decide
 120theorem e_131213 : m2Num 1 3 1 2 1 3 = 8 * explicitZ 1 3 1 2 1 3 := by decide
 121theorem e_131220 : m2Num 1 3 1 2 2 0 = 8 * explicitZ 1 3 1 2 2 0 := by decide
 122theorem e_131221 : m2Num 1 3 1 2 2 1 = 8 * explicitZ 1 3 1 2 2 1 := by decide
 123theorem e_131222 : m2Num 1 3 1 2 2 2 = 8 * explicitZ 1 3 1 2 2 2 := by decide
 124theorem e_131223 : m2Num 1 3 1 2 2 3 = 8 * explicitZ 1 3 1 2 2 3 := by decide
 125theorem e_131230 : m2Num 1 3 1 2 3 0 = 8 * explicitZ 1 3 1 2 3 0 := by decide
 126theorem e_131231 : m2Num 1 3 1 2 3 1 = 8 * explicitZ 1 3 1 2 3 1 := by decide
 127theorem e_131232 : m2Num 1 3 1 2 3 2 = 8 * explicitZ 1 3 1 2 3 2 := by decide
 128theorem e_131233 : m2Num 1 3 1 2 3 3 = 8 * explicitZ 1 3 1 2 3 3 := by decide
 129theorem e_131300 : m2Num 1 3 1 3 0 0 = 8 * explicitZ 1 3 1 3 0 0 := by decide
 130theorem e_131301 : m2Num 1 3 1 3 0 1 = 8 * explicitZ 1 3 1 3 0 1 := by decide
 131theorem e_131302 : m2Num 1 3 1 3 0 2 = 8 * explicitZ 1 3 1 3 0 2 := by decide
 132theorem e_131303 : m2Num 1 3 1 3 0 3 = 8 * explicitZ 1 3 1 3 0 3 := by decide
 133theorem e_131310 : m2Num 1 3 1 3 1 0 = 8 * explicitZ 1 3 1 3 1 0 := by decide
 134theorem e_131311 : m2Num 1 3 1 3 1 1 = 8 * explicitZ 1 3 1 3 1 1 := by decide
 135theorem e_131312 : m2Num 1 3 1 3 1 2 = 8 * explicitZ 1 3 1 3 1 2 := by decide
 136theorem e_131313 : m2Num 1 3 1 3 1 3 = 8 * explicitZ 1 3 1 3 1 3 := by decide
 137theorem e_131320 : m2Num 1 3 1 3 2 0 = 8 * explicitZ 1 3 1 3 2 0 := by decide
 138theorem e_131321 : m2Num 1 3 1 3 2 1 = 8 * explicitZ 1 3 1 3 2 1 := by decide
 139theorem e_131322 : m2Num 1 3 1 3 2 2 = 8 * explicitZ 1 3 1 3 2 2 := by decide
 140theorem e_131323 : m2Num 1 3 1 3 2 3 = 8 * explicitZ 1 3 1 3 2 3 := by decide
 141theorem e_131330 : m2Num 1 3 1 3 3 0 = 8 * explicitZ 1 3 1 3 3 0 := by decide
 142theorem e_131331 : m2Num 1 3 1 3 3 1 = 8 * explicitZ 1 3 1 3 3 1 := by decide
 143theorem e_131332 : m2Num 1 3 1 3 3 2 = 8 * explicitZ 1 3 1 3 3 2 := by decide
 144theorem e_131333 : m2Num 1 3 1 3 3 3 = 8 * explicitZ 1 3 1 3 3 3 := by decide
 145theorem e_132000 : m2Num 1 3 2 0 0 0 = 8 * explicitZ 1 3 2 0 0 0 := by decide
 146theorem e_132001 : m2Num 1 3 2 0 0 1 = 8 * explicitZ 1 3 2 0 0 1 := by decide
 147theorem e_132002 : m2Num 1 3 2 0 0 2 = 8 * explicitZ 1 3 2 0 0 2 := by decide
 148theorem e_132003 : m2Num 1 3 2 0 0 3 = 8 * explicitZ 1 3 2 0 0 3 := by decide
 149theorem e_132010 : m2Num 1 3 2 0 1 0 = 8 * explicitZ 1 3 2 0 1 0 := by decide
 150theorem e_132011 : m2Num 1 3 2 0 1 1 = 8 * explicitZ 1 3 2 0 1 1 := by decide
 151theorem e_132012 : m2Num 1 3 2 0 1 2 = 8 * explicitZ 1 3 2 0 1 2 := by decide
 152theorem e_132013 : m2Num 1 3 2 0 1 3 = 8 * explicitZ 1 3 2 0 1 3 := by decide
 153theorem e_132020 : m2Num 1 3 2 0 2 0 = 8 * explicitZ 1 3 2 0 2 0 := by decide
 154theorem e_132021 : m2Num 1 3 2 0 2 1 = 8 * explicitZ 1 3 2 0 2 1 := by decide
 155theorem e_132022 : m2Num 1 3 2 0 2 2 = 8 * explicitZ 1 3 2 0 2 2 := by decide
 156theorem e_132023 : m2Num 1 3 2 0 2 3 = 8 * explicitZ 1 3 2 0 2 3 := by decide
 157theorem e_132030 : m2Num 1 3 2 0 3 0 = 8 * explicitZ 1 3 2 0 3 0 := by decide
 158theorem e_132031 : m2Num 1 3 2 0 3 1 = 8 * explicitZ 1 3 2 0 3 1 := by decide
 159theorem e_132032 : m2Num 1 3 2 0 3 2 = 8 * explicitZ 1 3 2 0 3 2 := by decide
 160theorem e_132033 : m2Num 1 3 2 0 3 3 = 8 * explicitZ 1 3 2 0 3 3 := by decide
 161theorem e_132100 : m2Num 1 3 2 1 0 0 = 8 * explicitZ 1 3 2 1 0 0 := by decide
 162theorem e_132101 : m2Num 1 3 2 1 0 1 = 8 * explicitZ 1 3 2 1 0 1 := by decide
 163theorem e_132102 : m2Num 1 3 2 1 0 2 = 8 * explicitZ 1 3 2 1 0 2 := by decide
 164theorem e_132103 : m2Num 1 3 2 1 0 3 = 8 * explicitZ 1 3 2 1 0 3 := by decide
 165theorem e_132110 : m2Num 1 3 2 1 1 0 = 8 * explicitZ 1 3 2 1 1 0 := by decide
 166theorem e_132111 : m2Num 1 3 2 1 1 1 = 8 * explicitZ 1 3 2 1 1 1 := by decide
 167theorem e_132112 : m2Num 1 3 2 1 1 2 = 8 * explicitZ 1 3 2 1 1 2 := by decide
 168theorem e_132113 : m2Num 1 3 2 1 1 3 = 8 * explicitZ 1 3 2 1 1 3 := by decide
 169theorem e_132120 : m2Num 1 3 2 1 2 0 = 8 * explicitZ 1 3 2 1 2 0 := by decide
 170theorem e_132121 : m2Num 1 3 2 1 2 1 = 8 * explicitZ 1 3 2 1 2 1 := by decide
 171theorem e_132122 : m2Num 1 3 2 1 2 2 = 8 * explicitZ 1 3 2 1 2 2 := by decide
 172theorem e_132123 : m2Num 1 3 2 1 2 3 = 8 * explicitZ 1 3 2 1 2 3 := by decide
 173theorem e_132130 : m2Num 1 3 2 1 3 0 = 8 * explicitZ 1 3 2 1 3 0 := by decide
 174theorem e_132131 : m2Num 1 3 2 1 3 1 = 8 * explicitZ 1 3 2 1 3 1 := by decide
 175theorem e_132132 : m2Num 1 3 2 1 3 2 = 8 * explicitZ 1 3 2 1 3 2 := by decide
 176theorem e_132133 : m2Num 1 3 2 1 3 3 = 8 * explicitZ 1 3 2 1 3 3 := by decide
 177theorem e_132200 : m2Num 1 3 2 2 0 0 = 8 * explicitZ 1 3 2 2 0 0 := by decide
 178theorem e_132201 : m2Num 1 3 2 2 0 1 = 8 * explicitZ 1 3 2 2 0 1 := by decide
 179theorem e_132202 : m2Num 1 3 2 2 0 2 = 8 * explicitZ 1 3 2 2 0 2 := by decide
 180theorem e_132203 : m2Num 1 3 2 2 0 3 = 8 * explicitZ 1 3 2 2 0 3 := by decide
 181theorem e_132210 : m2Num 1 3 2 2 1 0 = 8 * explicitZ 1 3 2 2 1 0 := by decide
 182theorem e_132211 : m2Num 1 3 2 2 1 1 = 8 * explicitZ 1 3 2 2 1 1 := by decide
 183theorem e_132212 : m2Num 1 3 2 2 1 2 = 8 * explicitZ 1 3 2 2 1 2 := by decide
 184theorem e_132213 : m2Num 1 3 2 2 1 3 = 8 * explicitZ 1 3 2 2 1 3 := by decide
 185theorem e_132220 : m2Num 1 3 2 2 2 0 = 8 * explicitZ 1 3 2 2 2 0 := by decide
 186theorem e_132221 : m2Num 1 3 2 2 2 1 = 8 * explicitZ 1 3 2 2 2 1 := by decide
 187theorem e_132222 : m2Num 1 3 2 2 2 2 = 8 * explicitZ 1 3 2 2 2 2 := by decide
 188theorem e_132223 : m2Num 1 3 2 2 2 3 = 8 * explicitZ 1 3 2 2 2 3 := by decide
 189theorem e_132230 : m2Num 1 3 2 2 3 0 = 8 * explicitZ 1 3 2 2 3 0 := by decide
 190theorem e_132231 : m2Num 1 3 2 2 3 1 = 8 * explicitZ 1 3 2 2 3 1 := by decide
 191theorem e_132232 : m2Num 1 3 2 2 3 2 = 8 * explicitZ 1 3 2 2 3 2 := by decide
 192theorem e_132233 : m2Num 1 3 2 2 3 3 = 8 * explicitZ 1 3 2 2 3 3 := by decide
 193theorem e_132300 : m2Num 1 3 2 3 0 0 = 8 * explicitZ 1 3 2 3 0 0 := by decide
 194theorem e_132301 : m2Num 1 3 2 3 0 1 = 8 * explicitZ 1 3 2 3 0 1 := by decide
 195theorem e_132302 : m2Num 1 3 2 3 0 2 = 8 * explicitZ 1 3 2 3 0 2 := by decide
 196theorem e_132303 : m2Num 1 3 2 3 0 3 = 8 * explicitZ 1 3 2 3 0 3 := by decide
 197theorem e_132310 : m2Num 1 3 2 3 1 0 = 8 * explicitZ 1 3 2 3 1 0 := by decide
 198theorem e_132311 : m2Num 1 3 2 3 1 1 = 8 * explicitZ 1 3 2 3 1 1 := by decide
 199theorem e_132312 : m2Num 1 3 2 3 1 2 = 8 * explicitZ 1 3 2 3 1 2 := by decide
 200theorem e_132313 : m2Num 1 3 2 3 1 3 = 8 * explicitZ 1 3 2 3 1 3 := by decide
 201theorem e_132320 : m2Num 1 3 2 3 2 0 = 8 * explicitZ 1 3 2 3 2 0 := by decide
 202theorem e_132321 : m2Num 1 3 2 3 2 1 = 8 * explicitZ 1 3 2 3 2 1 := by decide
 203theorem e_132322 : m2Num 1 3 2 3 2 2 = 8 * explicitZ 1 3 2 3 2 2 := by decide
 204theorem e_132323 : m2Num 1 3 2 3 2 3 = 8 * explicitZ 1 3 2 3 2 3 := by decide
 205theorem e_132330 : m2Num 1 3 2 3 3 0 = 8 * explicitZ 1 3 2 3 3 0 := by decide
 206theorem e_132331 : m2Num 1 3 2 3 3 1 = 8 * explicitZ 1 3 2 3 3 1 := by decide
 207theorem e_132332 : m2Num 1 3 2 3 3 2 = 8 * explicitZ 1 3 2 3 3 2 := by decide
 208theorem e_132333 : m2Num 1 3 2 3 3 3 = 8 * explicitZ 1 3 2 3 3 3 := by decide
 209theorem e_133000 : m2Num 1 3 3 0 0 0 = 8 * explicitZ 1 3 3 0 0 0 := by decide
 210theorem e_133001 : m2Num 1 3 3 0 0 1 = 8 * explicitZ 1 3 3 0 0 1 := by decide
 211theorem e_133002 : m2Num 1 3 3 0 0 2 = 8 * explicitZ 1 3 3 0 0 2 := by decide
 212theorem e_133003 : m2Num 1 3 3 0 0 3 = 8 * explicitZ 1 3 3 0 0 3 := by decide
 213theorem e_133010 : m2Num 1 3 3 0 1 0 = 8 * explicitZ 1 3 3 0 1 0 := by decide
 214theorem e_133011 : m2Num 1 3 3 0 1 1 = 8 * explicitZ 1 3 3 0 1 1 := by decide
 215theorem e_133012 : m2Num 1 3 3 0 1 2 = 8 * explicitZ 1 3 3 0 1 2 := by decide
 216theorem e_133013 : m2Num 1 3 3 0 1 3 = 8 * explicitZ 1 3 3 0 1 3 := by decide
 217theorem e_133020 : m2Num 1 3 3 0 2 0 = 8 * explicitZ 1 3 3 0 2 0 := by decide
 218theorem e_133021 : m2Num 1 3 3 0 2 1 = 8 * explicitZ 1 3 3 0 2 1 := by decide
 219theorem e_133022 : m2Num 1 3 3 0 2 2 = 8 * explicitZ 1 3 3 0 2 2 := by decide
 220theorem e_133023 : m2Num 1 3 3 0 2 3 = 8 * explicitZ 1 3 3 0 2 3 := by decide
 221theorem e_133030 : m2Num 1 3 3 0 3 0 = 8 * explicitZ 1 3 3 0 3 0 := by decide
 222theorem e_133031 : m2Num 1 3 3 0 3 1 = 8 * explicitZ 1 3 3 0 3 1 := by decide
 223theorem e_133032 : m2Num 1 3 3 0 3 2 = 8 * explicitZ 1 3 3 0 3 2 := by decide
 224theorem e_133033 : m2Num 1 3 3 0 3 3 = 8 * explicitZ 1 3 3 0 3 3 := by decide
 225theorem e_133100 : m2Num 1 3 3 1 0 0 = 8 * explicitZ 1 3 3 1 0 0 := by decide
 226theorem e_133101 : m2Num 1 3 3 1 0 1 = 8 * explicitZ 1 3 3 1 0 1 := by decide
 227theorem e_133102 : m2Num 1 3 3 1 0 2 = 8 * explicitZ 1 3 3 1 0 2 := by decide
 228theorem e_133103 : m2Num 1 3 3 1 0 3 = 8 * explicitZ 1 3 3 1 0 3 := by decide
 229theorem e_133110 : m2Num 1 3 3 1 1 0 = 8 * explicitZ 1 3 3 1 1 0 := by decide
 230theorem e_133111 : m2Num 1 3 3 1 1 1 = 8 * explicitZ 1 3 3 1 1 1 := by decide
 231theorem e_133112 : m2Num 1 3 3 1 1 2 = 8 * explicitZ 1 3 3 1 1 2 := by decide
 232theorem e_133113 : m2Num 1 3 3 1 1 3 = 8 * explicitZ 1 3 3 1 1 3 := by decide
 233theorem e_133120 : m2Num 1 3 3 1 2 0 = 8 * explicitZ 1 3 3 1 2 0 := by decide
 234theorem e_133121 : m2Num 1 3 3 1 2 1 = 8 * explicitZ 1 3 3 1 2 1 := by decide
 235theorem e_133122 : m2Num 1 3 3 1 2 2 = 8 * explicitZ 1 3 3 1 2 2 := by decide
 236theorem e_133123 : m2Num 1 3 3 1 2 3 = 8 * explicitZ 1 3 3 1 2 3 := by decide
 237theorem e_133130 : m2Num 1 3 3 1 3 0 = 8 * explicitZ 1 3 3 1 3 0 := by decide
 238theorem e_133131 : m2Num 1 3 3 1 3 1 = 8 * explicitZ 1 3 3 1 3 1 := by decide
 239theorem e_133132 : m2Num 1 3 3 1 3 2 = 8 * explicitZ 1 3 3 1 3 2 := by decide
 240theorem e_133133 : m2Num 1 3 3 1 3 3 = 8 * explicitZ 1 3 3 1 3 3 := by decide
 241theorem e_133200 : m2Num 1 3 3 2 0 0 = 8 * explicitZ 1 3 3 2 0 0 := by decide
 242theorem e_133201 : m2Num 1 3 3 2 0 1 = 8 * explicitZ 1 3 3 2 0 1 := by decide
 243theorem e_133202 : m2Num 1 3 3 2 0 2 = 8 * explicitZ 1 3 3 2 0 2 := by decide
 244theorem e_133203 : m2Num 1 3 3 2 0 3 = 8 * explicitZ 1 3 3 2 0 3 := by decide
 245theorem e_133210 : m2Num 1 3 3 2 1 0 = 8 * explicitZ 1 3 3 2 1 0 := by decide
 246theorem e_133211 : m2Num 1 3 3 2 1 1 = 8 * explicitZ 1 3 3 2 1 1 := by decide
 247theorem e_133212 : m2Num 1 3 3 2 1 2 = 8 * explicitZ 1 3 3 2 1 2 := by decide
 248theorem e_133213 : m2Num 1 3 3 2 1 3 = 8 * explicitZ 1 3 3 2 1 3 := by decide
 249theorem e_133220 : m2Num 1 3 3 2 2 0 = 8 * explicitZ 1 3 3 2 2 0 := by decide
 250theorem e_133221 : m2Num 1 3 3 2 2 1 = 8 * explicitZ 1 3 3 2 2 1 := by decide
 251theorem e_133222 : m2Num 1 3 3 2 2 2 = 8 * explicitZ 1 3 3 2 2 2 := by decide
 252theorem e_133223 : m2Num 1 3 3 2 2 3 = 8 * explicitZ 1 3 3 2 2 3 := by decide
 253theorem e_133230 : m2Num 1 3 3 2 3 0 = 8 * explicitZ 1 3 3 2 3 0 := by decide
 254theorem e_133231 : m2Num 1 3 3 2 3 1 = 8 * explicitZ 1 3 3 2 3 1 := by decide
 255theorem e_133232 : m2Num 1 3 3 2 3 2 = 8 * explicitZ 1 3 3 2 3 2 := by decide
 256theorem e_133233 : m2Num 1 3 3 2 3 3 = 8 * explicitZ 1 3 3 2 3 3 := by decide
 257theorem e_133300 : m2Num 1 3 3 3 0 0 = 8 * explicitZ 1 3 3 3 0 0 := by decide
 258theorem e_133301 : m2Num 1 3 3 3 0 1 = 8 * explicitZ 1 3 3 3 0 1 := by decide
 259theorem e_133302 : m2Num 1 3 3 3 0 2 = 8 * explicitZ 1 3 3 3 0 2 := by decide
 260theorem e_133303 : m2Num 1 3 3 3 0 3 = 8 * explicitZ 1 3 3 3 0 3 := by decide
 261theorem e_133310 : m2Num 1 3 3 3 1 0 = 8 * explicitZ 1 3 3 3 1 0 := by decide
 262theorem e_133311 : m2Num 1 3 3 3 1 1 = 8 * explicitZ 1 3 3 3 1 1 := by decide
 263theorem e_133312 : m2Num 1 3 3 3 1 2 = 8 * explicitZ 1 3 3 3 1 2 := by decide
 264theorem e_133313 : m2Num 1 3 3 3 1 3 = 8 * explicitZ 1 3 3 3 1 3 := by decide
 265theorem e_133320 : m2Num 1 3 3 3 2 0 = 8 * explicitZ 1 3 3 3 2 0 := by decide
 266theorem e_133321 : m2Num 1 3 3 3 2 1 = 8 * explicitZ 1 3 3 3 2 1 := by decide
 267theorem e_133322 : m2Num 1 3 3 3 2 2 = 8 * explicitZ 1 3 3 3 2 2 := by decide
 268theorem e_133323 : m2Num 1 3 3 3 2 3 = 8 * explicitZ 1 3 3 3 2 3 := by decide
 269theorem e_133330 : m2Num 1 3 3 3 3 0 = 8 * explicitZ 1 3 3 3 3 0 := by decide
 270theorem e_133331 : m2Num 1 3 3 3 3 1 = 8 * explicitZ 1 3 3 3 3 1 := by decide
 271theorem e_133332 : m2Num 1 3 3 3 3 2 = 8 * explicitZ 1 3 3 3 3 2 := by decide
 272theorem e_133333 : m2Num 1 3 3 3 3 3 = 8 * explicitZ 1 3 3 3 3 3 := by decide
 273
 274end M2NumChunk07
 275end ReggeExactMidpointM2TTIdentity4D
 276end Analysis
 277end Gravity
 278end IndisputableMonolith
 279