IndisputableMonolith.Gravity.Analysis.ReggeExactMidpointM2TTIdentity4DM2NumChunk14

   1import Mathlib
   2import IndisputableMonolith.Gravity.Analysis.ReggeExactMidpointM2TTIdentity4DKernelCert
   3
   4/-! m2Num = 8·explicitZ, chunk 14 (256 kernel decides). -/
   5
   6namespace IndisputableMonolith
   7namespace Gravity
   8namespace Analysis
   9namespace ReggeExactMidpointM2TTIdentity4D
  10namespace M2NumChunk14
  11
  12open KernelCert
  13
  14set_option maxRecDepth 100000
  15set_option maxHeartbeats 200000000
  16
  17theorem e_320000 : m2Num 3 2 0 0 0 0 = 8 * explicitZ 3 2 0 0 0 0 := by decide
  18theorem e_320001 : m2Num 3 2 0 0 0 1 = 8 * explicitZ 3 2 0 0 0 1 := by decide
  19theorem e_320002 : m2Num 3 2 0 0 0 2 = 8 * explicitZ 3 2 0 0 0 2 := by decide
  20theorem e_320003 : m2Num 3 2 0 0 0 3 = 8 * explicitZ 3 2 0 0 0 3 := by decide
  21theorem e_320010 : m2Num 3 2 0 0 1 0 = 8 * explicitZ 3 2 0 0 1 0 := by decide
  22theorem e_320011 : m2Num 3 2 0 0 1 1 = 8 * explicitZ 3 2 0 0 1 1 := by decide
  23theorem e_320012 : m2Num 3 2 0 0 1 2 = 8 * explicitZ 3 2 0 0 1 2 := by decide
  24theorem e_320013 : m2Num 3 2 0 0 1 3 = 8 * explicitZ 3 2 0 0 1 3 := by decide
  25theorem e_320020 : m2Num 3 2 0 0 2 0 = 8 * explicitZ 3 2 0 0 2 0 := by decide
  26theorem e_320021 : m2Num 3 2 0 0 2 1 = 8 * explicitZ 3 2 0 0 2 1 := by decide
  27theorem e_320022 : m2Num 3 2 0 0 2 2 = 8 * explicitZ 3 2 0 0 2 2 := by decide
  28theorem e_320023 : m2Num 3 2 0 0 2 3 = 8 * explicitZ 3 2 0 0 2 3 := by decide
  29theorem e_320030 : m2Num 3 2 0 0 3 0 = 8 * explicitZ 3 2 0 0 3 0 := by decide
  30theorem e_320031 : m2Num 3 2 0 0 3 1 = 8 * explicitZ 3 2 0 0 3 1 := by decide
  31theorem e_320032 : m2Num 3 2 0 0 3 2 = 8 * explicitZ 3 2 0 0 3 2 := by decide
  32theorem e_320033 : m2Num 3 2 0 0 3 3 = 8 * explicitZ 3 2 0 0 3 3 := by decide
  33theorem e_320100 : m2Num 3 2 0 1 0 0 = 8 * explicitZ 3 2 0 1 0 0 := by decide
  34theorem e_320101 : m2Num 3 2 0 1 0 1 = 8 * explicitZ 3 2 0 1 0 1 := by decide
  35theorem e_320102 : m2Num 3 2 0 1 0 2 = 8 * explicitZ 3 2 0 1 0 2 := by decide
  36theorem e_320103 : m2Num 3 2 0 1 0 3 = 8 * explicitZ 3 2 0 1 0 3 := by decide
  37theorem e_320110 : m2Num 3 2 0 1 1 0 = 8 * explicitZ 3 2 0 1 1 0 := by decide
  38theorem e_320111 : m2Num 3 2 0 1 1 1 = 8 * explicitZ 3 2 0 1 1 1 := by decide
  39theorem e_320112 : m2Num 3 2 0 1 1 2 = 8 * explicitZ 3 2 0 1 1 2 := by decide
  40theorem e_320113 : m2Num 3 2 0 1 1 3 = 8 * explicitZ 3 2 0 1 1 3 := by decide
  41theorem e_320120 : m2Num 3 2 0 1 2 0 = 8 * explicitZ 3 2 0 1 2 0 := by decide
  42theorem e_320121 : m2Num 3 2 0 1 2 1 = 8 * explicitZ 3 2 0 1 2 1 := by decide
  43theorem e_320122 : m2Num 3 2 0 1 2 2 = 8 * explicitZ 3 2 0 1 2 2 := by decide
  44theorem e_320123 : m2Num 3 2 0 1 2 3 = 8 * explicitZ 3 2 0 1 2 3 := by decide
  45theorem e_320130 : m2Num 3 2 0 1 3 0 = 8 * explicitZ 3 2 0 1 3 0 := by decide
  46theorem e_320131 : m2Num 3 2 0 1 3 1 = 8 * explicitZ 3 2 0 1 3 1 := by decide
  47theorem e_320132 : m2Num 3 2 0 1 3 2 = 8 * explicitZ 3 2 0 1 3 2 := by decide
  48theorem e_320133 : m2Num 3 2 0 1 3 3 = 8 * explicitZ 3 2 0 1 3 3 := by decide
  49theorem e_320200 : m2Num 3 2 0 2 0 0 = 8 * explicitZ 3 2 0 2 0 0 := by decide
  50theorem e_320201 : m2Num 3 2 0 2 0 1 = 8 * explicitZ 3 2 0 2 0 1 := by decide
  51theorem e_320202 : m2Num 3 2 0 2 0 2 = 8 * explicitZ 3 2 0 2 0 2 := by decide
  52theorem e_320203 : m2Num 3 2 0 2 0 3 = 8 * explicitZ 3 2 0 2 0 3 := by decide
  53theorem e_320210 : m2Num 3 2 0 2 1 0 = 8 * explicitZ 3 2 0 2 1 0 := by decide
  54theorem e_320211 : m2Num 3 2 0 2 1 1 = 8 * explicitZ 3 2 0 2 1 1 := by decide
  55theorem e_320212 : m2Num 3 2 0 2 1 2 = 8 * explicitZ 3 2 0 2 1 2 := by decide
  56theorem e_320213 : m2Num 3 2 0 2 1 3 = 8 * explicitZ 3 2 0 2 1 3 := by decide
  57theorem e_320220 : m2Num 3 2 0 2 2 0 = 8 * explicitZ 3 2 0 2 2 0 := by decide
  58theorem e_320221 : m2Num 3 2 0 2 2 1 = 8 * explicitZ 3 2 0 2 2 1 := by decide
  59theorem e_320222 : m2Num 3 2 0 2 2 2 = 8 * explicitZ 3 2 0 2 2 2 := by decide
  60theorem e_320223 : m2Num 3 2 0 2 2 3 = 8 * explicitZ 3 2 0 2 2 3 := by decide
  61theorem e_320230 : m2Num 3 2 0 2 3 0 = 8 * explicitZ 3 2 0 2 3 0 := by decide
  62theorem e_320231 : m2Num 3 2 0 2 3 1 = 8 * explicitZ 3 2 0 2 3 1 := by decide
  63theorem e_320232 : m2Num 3 2 0 2 3 2 = 8 * explicitZ 3 2 0 2 3 2 := by decide
  64theorem e_320233 : m2Num 3 2 0 2 3 3 = 8 * explicitZ 3 2 0 2 3 3 := by decide
  65theorem e_320300 : m2Num 3 2 0 3 0 0 = 8 * explicitZ 3 2 0 3 0 0 := by decide
  66theorem e_320301 : m2Num 3 2 0 3 0 1 = 8 * explicitZ 3 2 0 3 0 1 := by decide
  67theorem e_320302 : m2Num 3 2 0 3 0 2 = 8 * explicitZ 3 2 0 3 0 2 := by decide
  68theorem e_320303 : m2Num 3 2 0 3 0 3 = 8 * explicitZ 3 2 0 3 0 3 := by decide
  69theorem e_320310 : m2Num 3 2 0 3 1 0 = 8 * explicitZ 3 2 0 3 1 0 := by decide
  70theorem e_320311 : m2Num 3 2 0 3 1 1 = 8 * explicitZ 3 2 0 3 1 1 := by decide
  71theorem e_320312 : m2Num 3 2 0 3 1 2 = 8 * explicitZ 3 2 0 3 1 2 := by decide
  72theorem e_320313 : m2Num 3 2 0 3 1 3 = 8 * explicitZ 3 2 0 3 1 3 := by decide
  73theorem e_320320 : m2Num 3 2 0 3 2 0 = 8 * explicitZ 3 2 0 3 2 0 := by decide
  74theorem e_320321 : m2Num 3 2 0 3 2 1 = 8 * explicitZ 3 2 0 3 2 1 := by decide
  75theorem e_320322 : m2Num 3 2 0 3 2 2 = 8 * explicitZ 3 2 0 3 2 2 := by decide
  76theorem e_320323 : m2Num 3 2 0 3 2 3 = 8 * explicitZ 3 2 0 3 2 3 := by decide
  77theorem e_320330 : m2Num 3 2 0 3 3 0 = 8 * explicitZ 3 2 0 3 3 0 := by decide
  78theorem e_320331 : m2Num 3 2 0 3 3 1 = 8 * explicitZ 3 2 0 3 3 1 := by decide
  79theorem e_320332 : m2Num 3 2 0 3 3 2 = 8 * explicitZ 3 2 0 3 3 2 := by decide
  80theorem e_320333 : m2Num 3 2 0 3 3 3 = 8 * explicitZ 3 2 0 3 3 3 := by decide
  81theorem e_321000 : m2Num 3 2 1 0 0 0 = 8 * explicitZ 3 2 1 0 0 0 := by decide
  82theorem e_321001 : m2Num 3 2 1 0 0 1 = 8 * explicitZ 3 2 1 0 0 1 := by decide
  83theorem e_321002 : m2Num 3 2 1 0 0 2 = 8 * explicitZ 3 2 1 0 0 2 := by decide
  84theorem e_321003 : m2Num 3 2 1 0 0 3 = 8 * explicitZ 3 2 1 0 0 3 := by decide
  85theorem e_321010 : m2Num 3 2 1 0 1 0 = 8 * explicitZ 3 2 1 0 1 0 := by decide
  86theorem e_321011 : m2Num 3 2 1 0 1 1 = 8 * explicitZ 3 2 1 0 1 1 := by decide
  87theorem e_321012 : m2Num 3 2 1 0 1 2 = 8 * explicitZ 3 2 1 0 1 2 := by decide
  88theorem e_321013 : m2Num 3 2 1 0 1 3 = 8 * explicitZ 3 2 1 0 1 3 := by decide
  89theorem e_321020 : m2Num 3 2 1 0 2 0 = 8 * explicitZ 3 2 1 0 2 0 := by decide
  90theorem e_321021 : m2Num 3 2 1 0 2 1 = 8 * explicitZ 3 2 1 0 2 1 := by decide
  91theorem e_321022 : m2Num 3 2 1 0 2 2 = 8 * explicitZ 3 2 1 0 2 2 := by decide
  92theorem e_321023 : m2Num 3 2 1 0 2 3 = 8 * explicitZ 3 2 1 0 2 3 := by decide
  93theorem e_321030 : m2Num 3 2 1 0 3 0 = 8 * explicitZ 3 2 1 0 3 0 := by decide
  94theorem e_321031 : m2Num 3 2 1 0 3 1 = 8 * explicitZ 3 2 1 0 3 1 := by decide
  95theorem e_321032 : m2Num 3 2 1 0 3 2 = 8 * explicitZ 3 2 1 0 3 2 := by decide
  96theorem e_321033 : m2Num 3 2 1 0 3 3 = 8 * explicitZ 3 2 1 0 3 3 := by decide
  97theorem e_321100 : m2Num 3 2 1 1 0 0 = 8 * explicitZ 3 2 1 1 0 0 := by decide
  98theorem e_321101 : m2Num 3 2 1 1 0 1 = 8 * explicitZ 3 2 1 1 0 1 := by decide
  99theorem e_321102 : m2Num 3 2 1 1 0 2 = 8 * explicitZ 3 2 1 1 0 2 := by decide
 100theorem e_321103 : m2Num 3 2 1 1 0 3 = 8 * explicitZ 3 2 1 1 0 3 := by decide
 101theorem e_321110 : m2Num 3 2 1 1 1 0 = 8 * explicitZ 3 2 1 1 1 0 := by decide
 102theorem e_321111 : m2Num 3 2 1 1 1 1 = 8 * explicitZ 3 2 1 1 1 1 := by decide
 103theorem e_321112 : m2Num 3 2 1 1 1 2 = 8 * explicitZ 3 2 1 1 1 2 := by decide
 104theorem e_321113 : m2Num 3 2 1 1 1 3 = 8 * explicitZ 3 2 1 1 1 3 := by decide
 105theorem e_321120 : m2Num 3 2 1 1 2 0 = 8 * explicitZ 3 2 1 1 2 0 := by decide
 106theorem e_321121 : m2Num 3 2 1 1 2 1 = 8 * explicitZ 3 2 1 1 2 1 := by decide
 107theorem e_321122 : m2Num 3 2 1 1 2 2 = 8 * explicitZ 3 2 1 1 2 2 := by decide
 108theorem e_321123 : m2Num 3 2 1 1 2 3 = 8 * explicitZ 3 2 1 1 2 3 := by decide
 109theorem e_321130 : m2Num 3 2 1 1 3 0 = 8 * explicitZ 3 2 1 1 3 0 := by decide
 110theorem e_321131 : m2Num 3 2 1 1 3 1 = 8 * explicitZ 3 2 1 1 3 1 := by decide
 111theorem e_321132 : m2Num 3 2 1 1 3 2 = 8 * explicitZ 3 2 1 1 3 2 := by decide
 112theorem e_321133 : m2Num 3 2 1 1 3 3 = 8 * explicitZ 3 2 1 1 3 3 := by decide
 113theorem e_321200 : m2Num 3 2 1 2 0 0 = 8 * explicitZ 3 2 1 2 0 0 := by decide
 114theorem e_321201 : m2Num 3 2 1 2 0 1 = 8 * explicitZ 3 2 1 2 0 1 := by decide
 115theorem e_321202 : m2Num 3 2 1 2 0 2 = 8 * explicitZ 3 2 1 2 0 2 := by decide
 116theorem e_321203 : m2Num 3 2 1 2 0 3 = 8 * explicitZ 3 2 1 2 0 3 := by decide
 117theorem e_321210 : m2Num 3 2 1 2 1 0 = 8 * explicitZ 3 2 1 2 1 0 := by decide
 118theorem e_321211 : m2Num 3 2 1 2 1 1 = 8 * explicitZ 3 2 1 2 1 1 := by decide
 119theorem e_321212 : m2Num 3 2 1 2 1 2 = 8 * explicitZ 3 2 1 2 1 2 := by decide
 120theorem e_321213 : m2Num 3 2 1 2 1 3 = 8 * explicitZ 3 2 1 2 1 3 := by decide
 121theorem e_321220 : m2Num 3 2 1 2 2 0 = 8 * explicitZ 3 2 1 2 2 0 := by decide
 122theorem e_321221 : m2Num 3 2 1 2 2 1 = 8 * explicitZ 3 2 1 2 2 1 := by decide
 123theorem e_321222 : m2Num 3 2 1 2 2 2 = 8 * explicitZ 3 2 1 2 2 2 := by decide
 124theorem e_321223 : m2Num 3 2 1 2 2 3 = 8 * explicitZ 3 2 1 2 2 3 := by decide
 125theorem e_321230 : m2Num 3 2 1 2 3 0 = 8 * explicitZ 3 2 1 2 3 0 := by decide
 126theorem e_321231 : m2Num 3 2 1 2 3 1 = 8 * explicitZ 3 2 1 2 3 1 := by decide
 127theorem e_321232 : m2Num 3 2 1 2 3 2 = 8 * explicitZ 3 2 1 2 3 2 := by decide
 128theorem e_321233 : m2Num 3 2 1 2 3 3 = 8 * explicitZ 3 2 1 2 3 3 := by decide
 129theorem e_321300 : m2Num 3 2 1 3 0 0 = 8 * explicitZ 3 2 1 3 0 0 := by decide
 130theorem e_321301 : m2Num 3 2 1 3 0 1 = 8 * explicitZ 3 2 1 3 0 1 := by decide
 131theorem e_321302 : m2Num 3 2 1 3 0 2 = 8 * explicitZ 3 2 1 3 0 2 := by decide
 132theorem e_321303 : m2Num 3 2 1 3 0 3 = 8 * explicitZ 3 2 1 3 0 3 := by decide
 133theorem e_321310 : m2Num 3 2 1 3 1 0 = 8 * explicitZ 3 2 1 3 1 0 := by decide
 134theorem e_321311 : m2Num 3 2 1 3 1 1 = 8 * explicitZ 3 2 1 3 1 1 := by decide
 135theorem e_321312 : m2Num 3 2 1 3 1 2 = 8 * explicitZ 3 2 1 3 1 2 := by decide
 136theorem e_321313 : m2Num 3 2 1 3 1 3 = 8 * explicitZ 3 2 1 3 1 3 := by decide
 137theorem e_321320 : m2Num 3 2 1 3 2 0 = 8 * explicitZ 3 2 1 3 2 0 := by decide
 138theorem e_321321 : m2Num 3 2 1 3 2 1 = 8 * explicitZ 3 2 1 3 2 1 := by decide
 139theorem e_321322 : m2Num 3 2 1 3 2 2 = 8 * explicitZ 3 2 1 3 2 2 := by decide
 140theorem e_321323 : m2Num 3 2 1 3 2 3 = 8 * explicitZ 3 2 1 3 2 3 := by decide
 141theorem e_321330 : m2Num 3 2 1 3 3 0 = 8 * explicitZ 3 2 1 3 3 0 := by decide
 142theorem e_321331 : m2Num 3 2 1 3 3 1 = 8 * explicitZ 3 2 1 3 3 1 := by decide
 143theorem e_321332 : m2Num 3 2 1 3 3 2 = 8 * explicitZ 3 2 1 3 3 2 := by decide
 144theorem e_321333 : m2Num 3 2 1 3 3 3 = 8 * explicitZ 3 2 1 3 3 3 := by decide
 145theorem e_322000 : m2Num 3 2 2 0 0 0 = 8 * explicitZ 3 2 2 0 0 0 := by decide
 146theorem e_322001 : m2Num 3 2 2 0 0 1 = 8 * explicitZ 3 2 2 0 0 1 := by decide
 147theorem e_322002 : m2Num 3 2 2 0 0 2 = 8 * explicitZ 3 2 2 0 0 2 := by decide
 148theorem e_322003 : m2Num 3 2 2 0 0 3 = 8 * explicitZ 3 2 2 0 0 3 := by decide
 149theorem e_322010 : m2Num 3 2 2 0 1 0 = 8 * explicitZ 3 2 2 0 1 0 := by decide
 150theorem e_322011 : m2Num 3 2 2 0 1 1 = 8 * explicitZ 3 2 2 0 1 1 := by decide
 151theorem e_322012 : m2Num 3 2 2 0 1 2 = 8 * explicitZ 3 2 2 0 1 2 := by decide
 152theorem e_322013 : m2Num 3 2 2 0 1 3 = 8 * explicitZ 3 2 2 0 1 3 := by decide
 153theorem e_322020 : m2Num 3 2 2 0 2 0 = 8 * explicitZ 3 2 2 0 2 0 := by decide
 154theorem e_322021 : m2Num 3 2 2 0 2 1 = 8 * explicitZ 3 2 2 0 2 1 := by decide
 155theorem e_322022 : m2Num 3 2 2 0 2 2 = 8 * explicitZ 3 2 2 0 2 2 := by decide
 156theorem e_322023 : m2Num 3 2 2 0 2 3 = 8 * explicitZ 3 2 2 0 2 3 := by decide
 157theorem e_322030 : m2Num 3 2 2 0 3 0 = 8 * explicitZ 3 2 2 0 3 0 := by decide
 158theorem e_322031 : m2Num 3 2 2 0 3 1 = 8 * explicitZ 3 2 2 0 3 1 := by decide
 159theorem e_322032 : m2Num 3 2 2 0 3 2 = 8 * explicitZ 3 2 2 0 3 2 := by decide
 160theorem e_322033 : m2Num 3 2 2 0 3 3 = 8 * explicitZ 3 2 2 0 3 3 := by decide
 161theorem e_322100 : m2Num 3 2 2 1 0 0 = 8 * explicitZ 3 2 2 1 0 0 := by decide
 162theorem e_322101 : m2Num 3 2 2 1 0 1 = 8 * explicitZ 3 2 2 1 0 1 := by decide
 163theorem e_322102 : m2Num 3 2 2 1 0 2 = 8 * explicitZ 3 2 2 1 0 2 := by decide
 164theorem e_322103 : m2Num 3 2 2 1 0 3 = 8 * explicitZ 3 2 2 1 0 3 := by decide
 165theorem e_322110 : m2Num 3 2 2 1 1 0 = 8 * explicitZ 3 2 2 1 1 0 := by decide
 166theorem e_322111 : m2Num 3 2 2 1 1 1 = 8 * explicitZ 3 2 2 1 1 1 := by decide
 167theorem e_322112 : m2Num 3 2 2 1 1 2 = 8 * explicitZ 3 2 2 1 1 2 := by decide
 168theorem e_322113 : m2Num 3 2 2 1 1 3 = 8 * explicitZ 3 2 2 1 1 3 := by decide
 169theorem e_322120 : m2Num 3 2 2 1 2 0 = 8 * explicitZ 3 2 2 1 2 0 := by decide
 170theorem e_322121 : m2Num 3 2 2 1 2 1 = 8 * explicitZ 3 2 2 1 2 1 := by decide
 171theorem e_322122 : m2Num 3 2 2 1 2 2 = 8 * explicitZ 3 2 2 1 2 2 := by decide
 172theorem e_322123 : m2Num 3 2 2 1 2 3 = 8 * explicitZ 3 2 2 1 2 3 := by decide
 173theorem e_322130 : m2Num 3 2 2 1 3 0 = 8 * explicitZ 3 2 2 1 3 0 := by decide
 174theorem e_322131 : m2Num 3 2 2 1 3 1 = 8 * explicitZ 3 2 2 1 3 1 := by decide
 175theorem e_322132 : m2Num 3 2 2 1 3 2 = 8 * explicitZ 3 2 2 1 3 2 := by decide
 176theorem e_322133 : m2Num 3 2 2 1 3 3 = 8 * explicitZ 3 2 2 1 3 3 := by decide
 177theorem e_322200 : m2Num 3 2 2 2 0 0 = 8 * explicitZ 3 2 2 2 0 0 := by decide
 178theorem e_322201 : m2Num 3 2 2 2 0 1 = 8 * explicitZ 3 2 2 2 0 1 := by decide
 179theorem e_322202 : m2Num 3 2 2 2 0 2 = 8 * explicitZ 3 2 2 2 0 2 := by decide
 180theorem e_322203 : m2Num 3 2 2 2 0 3 = 8 * explicitZ 3 2 2 2 0 3 := by decide
 181theorem e_322210 : m2Num 3 2 2 2 1 0 = 8 * explicitZ 3 2 2 2 1 0 := by decide
 182theorem e_322211 : m2Num 3 2 2 2 1 1 = 8 * explicitZ 3 2 2 2 1 1 := by decide
 183theorem e_322212 : m2Num 3 2 2 2 1 2 = 8 * explicitZ 3 2 2 2 1 2 := by decide
 184theorem e_322213 : m2Num 3 2 2 2 1 3 = 8 * explicitZ 3 2 2 2 1 3 := by decide
 185theorem e_322220 : m2Num 3 2 2 2 2 0 = 8 * explicitZ 3 2 2 2 2 0 := by decide
 186theorem e_322221 : m2Num 3 2 2 2 2 1 = 8 * explicitZ 3 2 2 2 2 1 := by decide
 187theorem e_322222 : m2Num 3 2 2 2 2 2 = 8 * explicitZ 3 2 2 2 2 2 := by decide
 188theorem e_322223 : m2Num 3 2 2 2 2 3 = 8 * explicitZ 3 2 2 2 2 3 := by decide
 189theorem e_322230 : m2Num 3 2 2 2 3 0 = 8 * explicitZ 3 2 2 2 3 0 := by decide
 190theorem e_322231 : m2Num 3 2 2 2 3 1 = 8 * explicitZ 3 2 2 2 3 1 := by decide
 191theorem e_322232 : m2Num 3 2 2 2 3 2 = 8 * explicitZ 3 2 2 2 3 2 := by decide
 192theorem e_322233 : m2Num 3 2 2 2 3 3 = 8 * explicitZ 3 2 2 2 3 3 := by decide
 193theorem e_322300 : m2Num 3 2 2 3 0 0 = 8 * explicitZ 3 2 2 3 0 0 := by decide
 194theorem e_322301 : m2Num 3 2 2 3 0 1 = 8 * explicitZ 3 2 2 3 0 1 := by decide
 195theorem e_322302 : m2Num 3 2 2 3 0 2 = 8 * explicitZ 3 2 2 3 0 2 := by decide
 196theorem e_322303 : m2Num 3 2 2 3 0 3 = 8 * explicitZ 3 2 2 3 0 3 := by decide
 197theorem e_322310 : m2Num 3 2 2 3 1 0 = 8 * explicitZ 3 2 2 3 1 0 := by decide
 198theorem e_322311 : m2Num 3 2 2 3 1 1 = 8 * explicitZ 3 2 2 3 1 1 := by decide
 199theorem e_322312 : m2Num 3 2 2 3 1 2 = 8 * explicitZ 3 2 2 3 1 2 := by decide
 200theorem e_322313 : m2Num 3 2 2 3 1 3 = 8 * explicitZ 3 2 2 3 1 3 := by decide
 201theorem e_322320 : m2Num 3 2 2 3 2 0 = 8 * explicitZ 3 2 2 3 2 0 := by decide
 202theorem e_322321 : m2Num 3 2 2 3 2 1 = 8 * explicitZ 3 2 2 3 2 1 := by decide
 203theorem e_322322 : m2Num 3 2 2 3 2 2 = 8 * explicitZ 3 2 2 3 2 2 := by decide
 204theorem e_322323 : m2Num 3 2 2 3 2 3 = 8 * explicitZ 3 2 2 3 2 3 := by decide
 205theorem e_322330 : m2Num 3 2 2 3 3 0 = 8 * explicitZ 3 2 2 3 3 0 := by decide
 206theorem e_322331 : m2Num 3 2 2 3 3 1 = 8 * explicitZ 3 2 2 3 3 1 := by decide
 207theorem e_322332 : m2Num 3 2 2 3 3 2 = 8 * explicitZ 3 2 2 3 3 2 := by decide
 208theorem e_322333 : m2Num 3 2 2 3 3 3 = 8 * explicitZ 3 2 2 3 3 3 := by decide
 209theorem e_323000 : m2Num 3 2 3 0 0 0 = 8 * explicitZ 3 2 3 0 0 0 := by decide
 210theorem e_323001 : m2Num 3 2 3 0 0 1 = 8 * explicitZ 3 2 3 0 0 1 := by decide
 211theorem e_323002 : m2Num 3 2 3 0 0 2 = 8 * explicitZ 3 2 3 0 0 2 := by decide
 212theorem e_323003 : m2Num 3 2 3 0 0 3 = 8 * explicitZ 3 2 3 0 0 3 := by decide
 213theorem e_323010 : m2Num 3 2 3 0 1 0 = 8 * explicitZ 3 2 3 0 1 0 := by decide
 214theorem e_323011 : m2Num 3 2 3 0 1 1 = 8 * explicitZ 3 2 3 0 1 1 := by decide
 215theorem e_323012 : m2Num 3 2 3 0 1 2 = 8 * explicitZ 3 2 3 0 1 2 := by decide
 216theorem e_323013 : m2Num 3 2 3 0 1 3 = 8 * explicitZ 3 2 3 0 1 3 := by decide
 217theorem e_323020 : m2Num 3 2 3 0 2 0 = 8 * explicitZ 3 2 3 0 2 0 := by decide
 218theorem e_323021 : m2Num 3 2 3 0 2 1 = 8 * explicitZ 3 2 3 0 2 1 := by decide
 219theorem e_323022 : m2Num 3 2 3 0 2 2 = 8 * explicitZ 3 2 3 0 2 2 := by decide
 220theorem e_323023 : m2Num 3 2 3 0 2 3 = 8 * explicitZ 3 2 3 0 2 3 := by decide
 221theorem e_323030 : m2Num 3 2 3 0 3 0 = 8 * explicitZ 3 2 3 0 3 0 := by decide
 222theorem e_323031 : m2Num 3 2 3 0 3 1 = 8 * explicitZ 3 2 3 0 3 1 := by decide
 223theorem e_323032 : m2Num 3 2 3 0 3 2 = 8 * explicitZ 3 2 3 0 3 2 := by decide
 224theorem e_323033 : m2Num 3 2 3 0 3 3 = 8 * explicitZ 3 2 3 0 3 3 := by decide
 225theorem e_323100 : m2Num 3 2 3 1 0 0 = 8 * explicitZ 3 2 3 1 0 0 := by decide
 226theorem e_323101 : m2Num 3 2 3 1 0 1 = 8 * explicitZ 3 2 3 1 0 1 := by decide
 227theorem e_323102 : m2Num 3 2 3 1 0 2 = 8 * explicitZ 3 2 3 1 0 2 := by decide
 228theorem e_323103 : m2Num 3 2 3 1 0 3 = 8 * explicitZ 3 2 3 1 0 3 := by decide
 229theorem e_323110 : m2Num 3 2 3 1 1 0 = 8 * explicitZ 3 2 3 1 1 0 := by decide
 230theorem e_323111 : m2Num 3 2 3 1 1 1 = 8 * explicitZ 3 2 3 1 1 1 := by decide
 231theorem e_323112 : m2Num 3 2 3 1 1 2 = 8 * explicitZ 3 2 3 1 1 2 := by decide
 232theorem e_323113 : m2Num 3 2 3 1 1 3 = 8 * explicitZ 3 2 3 1 1 3 := by decide
 233theorem e_323120 : m2Num 3 2 3 1 2 0 = 8 * explicitZ 3 2 3 1 2 0 := by decide
 234theorem e_323121 : m2Num 3 2 3 1 2 1 = 8 * explicitZ 3 2 3 1 2 1 := by decide
 235theorem e_323122 : m2Num 3 2 3 1 2 2 = 8 * explicitZ 3 2 3 1 2 2 := by decide
 236theorem e_323123 : m2Num 3 2 3 1 2 3 = 8 * explicitZ 3 2 3 1 2 3 := by decide
 237theorem e_323130 : m2Num 3 2 3 1 3 0 = 8 * explicitZ 3 2 3 1 3 0 := by decide
 238theorem e_323131 : m2Num 3 2 3 1 3 1 = 8 * explicitZ 3 2 3 1 3 1 := by decide
 239theorem e_323132 : m2Num 3 2 3 1 3 2 = 8 * explicitZ 3 2 3 1 3 2 := by decide
 240theorem e_323133 : m2Num 3 2 3 1 3 3 = 8 * explicitZ 3 2 3 1 3 3 := by decide
 241theorem e_323200 : m2Num 3 2 3 2 0 0 = 8 * explicitZ 3 2 3 2 0 0 := by decide
 242theorem e_323201 : m2Num 3 2 3 2 0 1 = 8 * explicitZ 3 2 3 2 0 1 := by decide
 243theorem e_323202 : m2Num 3 2 3 2 0 2 = 8 * explicitZ 3 2 3 2 0 2 := by decide
 244theorem e_323203 : m2Num 3 2 3 2 0 3 = 8 * explicitZ 3 2 3 2 0 3 := by decide
 245theorem e_323210 : m2Num 3 2 3 2 1 0 = 8 * explicitZ 3 2 3 2 1 0 := by decide
 246theorem e_323211 : m2Num 3 2 3 2 1 1 = 8 * explicitZ 3 2 3 2 1 1 := by decide
 247theorem e_323212 : m2Num 3 2 3 2 1 2 = 8 * explicitZ 3 2 3 2 1 2 := by decide
 248theorem e_323213 : m2Num 3 2 3 2 1 3 = 8 * explicitZ 3 2 3 2 1 3 := by decide
 249theorem e_323220 : m2Num 3 2 3 2 2 0 = 8 * explicitZ 3 2 3 2 2 0 := by decide
 250theorem e_323221 : m2Num 3 2 3 2 2 1 = 8 * explicitZ 3 2 3 2 2 1 := by decide
 251theorem e_323222 : m2Num 3 2 3 2 2 2 = 8 * explicitZ 3 2 3 2 2 2 := by decide
 252theorem e_323223 : m2Num 3 2 3 2 2 3 = 8 * explicitZ 3 2 3 2 2 3 := by decide
 253theorem e_323230 : m2Num 3 2 3 2 3 0 = 8 * explicitZ 3 2 3 2 3 0 := by decide
 254theorem e_323231 : m2Num 3 2 3 2 3 1 = 8 * explicitZ 3 2 3 2 3 1 := by decide
 255theorem e_323232 : m2Num 3 2 3 2 3 2 = 8 * explicitZ 3 2 3 2 3 2 := by decide
 256theorem e_323233 : m2Num 3 2 3 2 3 3 = 8 * explicitZ 3 2 3 2 3 3 := by decide
 257theorem e_323300 : m2Num 3 2 3 3 0 0 = 8 * explicitZ 3 2 3 3 0 0 := by decide
 258theorem e_323301 : m2Num 3 2 3 3 0 1 = 8 * explicitZ 3 2 3 3 0 1 := by decide
 259theorem e_323302 : m2Num 3 2 3 3 0 2 = 8 * explicitZ 3 2 3 3 0 2 := by decide
 260theorem e_323303 : m2Num 3 2 3 3 0 3 = 8 * explicitZ 3 2 3 3 0 3 := by decide
 261theorem e_323310 : m2Num 3 2 3 3 1 0 = 8 * explicitZ 3 2 3 3 1 0 := by decide
 262theorem e_323311 : m2Num 3 2 3 3 1 1 = 8 * explicitZ 3 2 3 3 1 1 := by decide
 263theorem e_323312 : m2Num 3 2 3 3 1 2 = 8 * explicitZ 3 2 3 3 1 2 := by decide
 264theorem e_323313 : m2Num 3 2 3 3 1 3 = 8 * explicitZ 3 2 3 3 1 3 := by decide
 265theorem e_323320 : m2Num 3 2 3 3 2 0 = 8 * explicitZ 3 2 3 3 2 0 := by decide
 266theorem e_323321 : m2Num 3 2 3 3 2 1 = 8 * explicitZ 3 2 3 3 2 1 := by decide
 267theorem e_323322 : m2Num 3 2 3 3 2 2 = 8 * explicitZ 3 2 3 3 2 2 := by decide
 268theorem e_323323 : m2Num 3 2 3 3 2 3 = 8 * explicitZ 3 2 3 3 2 3 := by decide
 269theorem e_323330 : m2Num 3 2 3 3 3 0 = 8 * explicitZ 3 2 3 3 3 0 := by decide
 270theorem e_323331 : m2Num 3 2 3 3 3 1 = 8 * explicitZ 3 2 3 3 3 1 := by decide
 271theorem e_323332 : m2Num 3 2 3 3 3 2 = 8 * explicitZ 3 2 3 3 3 2 := by decide
 272theorem e_323333 : m2Num 3 2 3 3 3 3 = 8 * explicitZ 3 2 3 3 3 3 := by decide
 273
 274end M2NumChunk14
 275end ReggeExactMidpointM2TTIdentity4D
 276end Analysis
 277end Gravity
 278end IndisputableMonolith
 279