IndisputableMonolith.Gravity.Analysis.ReggeExactMidpointM2TTIdentity4DM2NumChunk03

   1import Mathlib
   2import IndisputableMonolith.Gravity.Analysis.ReggeExactMidpointM2TTIdentity4DKernelCert
   3
   4/-! m2Num = 8·explicitZ, chunk 3 (256 kernel decides). -/
   5
   6namespace IndisputableMonolith
   7namespace Gravity
   8namespace Analysis
   9namespace ReggeExactMidpointM2TTIdentity4D
  10namespace M2NumChunk03
  11
  12open KernelCert
  13
  14set_option maxRecDepth 100000
  15set_option maxHeartbeats 200000000
  16
  17theorem e_030000 : m2Num 0 3 0 0 0 0 = 8 * explicitZ 0 3 0 0 0 0 := by decide
  18theorem e_030001 : m2Num 0 3 0 0 0 1 = 8 * explicitZ 0 3 0 0 0 1 := by decide
  19theorem e_030002 : m2Num 0 3 0 0 0 2 = 8 * explicitZ 0 3 0 0 0 2 := by decide
  20theorem e_030003 : m2Num 0 3 0 0 0 3 = 8 * explicitZ 0 3 0 0 0 3 := by decide
  21theorem e_030010 : m2Num 0 3 0 0 1 0 = 8 * explicitZ 0 3 0 0 1 0 := by decide
  22theorem e_030011 : m2Num 0 3 0 0 1 1 = 8 * explicitZ 0 3 0 0 1 1 := by decide
  23theorem e_030012 : m2Num 0 3 0 0 1 2 = 8 * explicitZ 0 3 0 0 1 2 := by decide
  24theorem e_030013 : m2Num 0 3 0 0 1 3 = 8 * explicitZ 0 3 0 0 1 3 := by decide
  25theorem e_030020 : m2Num 0 3 0 0 2 0 = 8 * explicitZ 0 3 0 0 2 0 := by decide
  26theorem e_030021 : m2Num 0 3 0 0 2 1 = 8 * explicitZ 0 3 0 0 2 1 := by decide
  27theorem e_030022 : m2Num 0 3 0 0 2 2 = 8 * explicitZ 0 3 0 0 2 2 := by decide
  28theorem e_030023 : m2Num 0 3 0 0 2 3 = 8 * explicitZ 0 3 0 0 2 3 := by decide
  29theorem e_030030 : m2Num 0 3 0 0 3 0 = 8 * explicitZ 0 3 0 0 3 0 := by decide
  30theorem e_030031 : m2Num 0 3 0 0 3 1 = 8 * explicitZ 0 3 0 0 3 1 := by decide
  31theorem e_030032 : m2Num 0 3 0 0 3 2 = 8 * explicitZ 0 3 0 0 3 2 := by decide
  32theorem e_030033 : m2Num 0 3 0 0 3 3 = 8 * explicitZ 0 3 0 0 3 3 := by decide
  33theorem e_030100 : m2Num 0 3 0 1 0 0 = 8 * explicitZ 0 3 0 1 0 0 := by decide
  34theorem e_030101 : m2Num 0 3 0 1 0 1 = 8 * explicitZ 0 3 0 1 0 1 := by decide
  35theorem e_030102 : m2Num 0 3 0 1 0 2 = 8 * explicitZ 0 3 0 1 0 2 := by decide
  36theorem e_030103 : m2Num 0 3 0 1 0 3 = 8 * explicitZ 0 3 0 1 0 3 := by decide
  37theorem e_030110 : m2Num 0 3 0 1 1 0 = 8 * explicitZ 0 3 0 1 1 0 := by decide
  38theorem e_030111 : m2Num 0 3 0 1 1 1 = 8 * explicitZ 0 3 0 1 1 1 := by decide
  39theorem e_030112 : m2Num 0 3 0 1 1 2 = 8 * explicitZ 0 3 0 1 1 2 := by decide
  40theorem e_030113 : m2Num 0 3 0 1 1 3 = 8 * explicitZ 0 3 0 1 1 3 := by decide
  41theorem e_030120 : m2Num 0 3 0 1 2 0 = 8 * explicitZ 0 3 0 1 2 0 := by decide
  42theorem e_030121 : m2Num 0 3 0 1 2 1 = 8 * explicitZ 0 3 0 1 2 1 := by decide
  43theorem e_030122 : m2Num 0 3 0 1 2 2 = 8 * explicitZ 0 3 0 1 2 2 := by decide
  44theorem e_030123 : m2Num 0 3 0 1 2 3 = 8 * explicitZ 0 3 0 1 2 3 := by decide
  45theorem e_030130 : m2Num 0 3 0 1 3 0 = 8 * explicitZ 0 3 0 1 3 0 := by decide
  46theorem e_030131 : m2Num 0 3 0 1 3 1 = 8 * explicitZ 0 3 0 1 3 1 := by decide
  47theorem e_030132 : m2Num 0 3 0 1 3 2 = 8 * explicitZ 0 3 0 1 3 2 := by decide
  48theorem e_030133 : m2Num 0 3 0 1 3 3 = 8 * explicitZ 0 3 0 1 3 3 := by decide
  49theorem e_030200 : m2Num 0 3 0 2 0 0 = 8 * explicitZ 0 3 0 2 0 0 := by decide
  50theorem e_030201 : m2Num 0 3 0 2 0 1 = 8 * explicitZ 0 3 0 2 0 1 := by decide
  51theorem e_030202 : m2Num 0 3 0 2 0 2 = 8 * explicitZ 0 3 0 2 0 2 := by decide
  52theorem e_030203 : m2Num 0 3 0 2 0 3 = 8 * explicitZ 0 3 0 2 0 3 := by decide
  53theorem e_030210 : m2Num 0 3 0 2 1 0 = 8 * explicitZ 0 3 0 2 1 0 := by decide
  54theorem e_030211 : m2Num 0 3 0 2 1 1 = 8 * explicitZ 0 3 0 2 1 1 := by decide
  55theorem e_030212 : m2Num 0 3 0 2 1 2 = 8 * explicitZ 0 3 0 2 1 2 := by decide
  56theorem e_030213 : m2Num 0 3 0 2 1 3 = 8 * explicitZ 0 3 0 2 1 3 := by decide
  57theorem e_030220 : m2Num 0 3 0 2 2 0 = 8 * explicitZ 0 3 0 2 2 0 := by decide
  58theorem e_030221 : m2Num 0 3 0 2 2 1 = 8 * explicitZ 0 3 0 2 2 1 := by decide
  59theorem e_030222 : m2Num 0 3 0 2 2 2 = 8 * explicitZ 0 3 0 2 2 2 := by decide
  60theorem e_030223 : m2Num 0 3 0 2 2 3 = 8 * explicitZ 0 3 0 2 2 3 := by decide
  61theorem e_030230 : m2Num 0 3 0 2 3 0 = 8 * explicitZ 0 3 0 2 3 0 := by decide
  62theorem e_030231 : m2Num 0 3 0 2 3 1 = 8 * explicitZ 0 3 0 2 3 1 := by decide
  63theorem e_030232 : m2Num 0 3 0 2 3 2 = 8 * explicitZ 0 3 0 2 3 2 := by decide
  64theorem e_030233 : m2Num 0 3 0 2 3 3 = 8 * explicitZ 0 3 0 2 3 3 := by decide
  65theorem e_030300 : m2Num 0 3 0 3 0 0 = 8 * explicitZ 0 3 0 3 0 0 := by decide
  66theorem e_030301 : m2Num 0 3 0 3 0 1 = 8 * explicitZ 0 3 0 3 0 1 := by decide
  67theorem e_030302 : m2Num 0 3 0 3 0 2 = 8 * explicitZ 0 3 0 3 0 2 := by decide
  68theorem e_030303 : m2Num 0 3 0 3 0 3 = 8 * explicitZ 0 3 0 3 0 3 := by decide
  69theorem e_030310 : m2Num 0 3 0 3 1 0 = 8 * explicitZ 0 3 0 3 1 0 := by decide
  70theorem e_030311 : m2Num 0 3 0 3 1 1 = 8 * explicitZ 0 3 0 3 1 1 := by decide
  71theorem e_030312 : m2Num 0 3 0 3 1 2 = 8 * explicitZ 0 3 0 3 1 2 := by decide
  72theorem e_030313 : m2Num 0 3 0 3 1 3 = 8 * explicitZ 0 3 0 3 1 3 := by decide
  73theorem e_030320 : m2Num 0 3 0 3 2 0 = 8 * explicitZ 0 3 0 3 2 0 := by decide
  74theorem e_030321 : m2Num 0 3 0 3 2 1 = 8 * explicitZ 0 3 0 3 2 1 := by decide
  75theorem e_030322 : m2Num 0 3 0 3 2 2 = 8 * explicitZ 0 3 0 3 2 2 := by decide
  76theorem e_030323 : m2Num 0 3 0 3 2 3 = 8 * explicitZ 0 3 0 3 2 3 := by decide
  77theorem e_030330 : m2Num 0 3 0 3 3 0 = 8 * explicitZ 0 3 0 3 3 0 := by decide
  78theorem e_030331 : m2Num 0 3 0 3 3 1 = 8 * explicitZ 0 3 0 3 3 1 := by decide
  79theorem e_030332 : m2Num 0 3 0 3 3 2 = 8 * explicitZ 0 3 0 3 3 2 := by decide
  80theorem e_030333 : m2Num 0 3 0 3 3 3 = 8 * explicitZ 0 3 0 3 3 3 := by decide
  81theorem e_031000 : m2Num 0 3 1 0 0 0 = 8 * explicitZ 0 3 1 0 0 0 := by decide
  82theorem e_031001 : m2Num 0 3 1 0 0 1 = 8 * explicitZ 0 3 1 0 0 1 := by decide
  83theorem e_031002 : m2Num 0 3 1 0 0 2 = 8 * explicitZ 0 3 1 0 0 2 := by decide
  84theorem e_031003 : m2Num 0 3 1 0 0 3 = 8 * explicitZ 0 3 1 0 0 3 := by decide
  85theorem e_031010 : m2Num 0 3 1 0 1 0 = 8 * explicitZ 0 3 1 0 1 0 := by decide
  86theorem e_031011 : m2Num 0 3 1 0 1 1 = 8 * explicitZ 0 3 1 0 1 1 := by decide
  87theorem e_031012 : m2Num 0 3 1 0 1 2 = 8 * explicitZ 0 3 1 0 1 2 := by decide
  88theorem e_031013 : m2Num 0 3 1 0 1 3 = 8 * explicitZ 0 3 1 0 1 3 := by decide
  89theorem e_031020 : m2Num 0 3 1 0 2 0 = 8 * explicitZ 0 3 1 0 2 0 := by decide
  90theorem e_031021 : m2Num 0 3 1 0 2 1 = 8 * explicitZ 0 3 1 0 2 1 := by decide
  91theorem e_031022 : m2Num 0 3 1 0 2 2 = 8 * explicitZ 0 3 1 0 2 2 := by decide
  92theorem e_031023 : m2Num 0 3 1 0 2 3 = 8 * explicitZ 0 3 1 0 2 3 := by decide
  93theorem e_031030 : m2Num 0 3 1 0 3 0 = 8 * explicitZ 0 3 1 0 3 0 := by decide
  94theorem e_031031 : m2Num 0 3 1 0 3 1 = 8 * explicitZ 0 3 1 0 3 1 := by decide
  95theorem e_031032 : m2Num 0 3 1 0 3 2 = 8 * explicitZ 0 3 1 0 3 2 := by decide
  96theorem e_031033 : m2Num 0 3 1 0 3 3 = 8 * explicitZ 0 3 1 0 3 3 := by decide
  97theorem e_031100 : m2Num 0 3 1 1 0 0 = 8 * explicitZ 0 3 1 1 0 0 := by decide
  98theorem e_031101 : m2Num 0 3 1 1 0 1 = 8 * explicitZ 0 3 1 1 0 1 := by decide
  99theorem e_031102 : m2Num 0 3 1 1 0 2 = 8 * explicitZ 0 3 1 1 0 2 := by decide
 100theorem e_031103 : m2Num 0 3 1 1 0 3 = 8 * explicitZ 0 3 1 1 0 3 := by decide
 101theorem e_031110 : m2Num 0 3 1 1 1 0 = 8 * explicitZ 0 3 1 1 1 0 := by decide
 102theorem e_031111 : m2Num 0 3 1 1 1 1 = 8 * explicitZ 0 3 1 1 1 1 := by decide
 103theorem e_031112 : m2Num 0 3 1 1 1 2 = 8 * explicitZ 0 3 1 1 1 2 := by decide
 104theorem e_031113 : m2Num 0 3 1 1 1 3 = 8 * explicitZ 0 3 1 1 1 3 := by decide
 105theorem e_031120 : m2Num 0 3 1 1 2 0 = 8 * explicitZ 0 3 1 1 2 0 := by decide
 106theorem e_031121 : m2Num 0 3 1 1 2 1 = 8 * explicitZ 0 3 1 1 2 1 := by decide
 107theorem e_031122 : m2Num 0 3 1 1 2 2 = 8 * explicitZ 0 3 1 1 2 2 := by decide
 108theorem e_031123 : m2Num 0 3 1 1 2 3 = 8 * explicitZ 0 3 1 1 2 3 := by decide
 109theorem e_031130 : m2Num 0 3 1 1 3 0 = 8 * explicitZ 0 3 1 1 3 0 := by decide
 110theorem e_031131 : m2Num 0 3 1 1 3 1 = 8 * explicitZ 0 3 1 1 3 1 := by decide
 111theorem e_031132 : m2Num 0 3 1 1 3 2 = 8 * explicitZ 0 3 1 1 3 2 := by decide
 112theorem e_031133 : m2Num 0 3 1 1 3 3 = 8 * explicitZ 0 3 1 1 3 3 := by decide
 113theorem e_031200 : m2Num 0 3 1 2 0 0 = 8 * explicitZ 0 3 1 2 0 0 := by decide
 114theorem e_031201 : m2Num 0 3 1 2 0 1 = 8 * explicitZ 0 3 1 2 0 1 := by decide
 115theorem e_031202 : m2Num 0 3 1 2 0 2 = 8 * explicitZ 0 3 1 2 0 2 := by decide
 116theorem e_031203 : m2Num 0 3 1 2 0 3 = 8 * explicitZ 0 3 1 2 0 3 := by decide
 117theorem e_031210 : m2Num 0 3 1 2 1 0 = 8 * explicitZ 0 3 1 2 1 0 := by decide
 118theorem e_031211 : m2Num 0 3 1 2 1 1 = 8 * explicitZ 0 3 1 2 1 1 := by decide
 119theorem e_031212 : m2Num 0 3 1 2 1 2 = 8 * explicitZ 0 3 1 2 1 2 := by decide
 120theorem e_031213 : m2Num 0 3 1 2 1 3 = 8 * explicitZ 0 3 1 2 1 3 := by decide
 121theorem e_031220 : m2Num 0 3 1 2 2 0 = 8 * explicitZ 0 3 1 2 2 0 := by decide
 122theorem e_031221 : m2Num 0 3 1 2 2 1 = 8 * explicitZ 0 3 1 2 2 1 := by decide
 123theorem e_031222 : m2Num 0 3 1 2 2 2 = 8 * explicitZ 0 3 1 2 2 2 := by decide
 124theorem e_031223 : m2Num 0 3 1 2 2 3 = 8 * explicitZ 0 3 1 2 2 3 := by decide
 125theorem e_031230 : m2Num 0 3 1 2 3 0 = 8 * explicitZ 0 3 1 2 3 0 := by decide
 126theorem e_031231 : m2Num 0 3 1 2 3 1 = 8 * explicitZ 0 3 1 2 3 1 := by decide
 127theorem e_031232 : m2Num 0 3 1 2 3 2 = 8 * explicitZ 0 3 1 2 3 2 := by decide
 128theorem e_031233 : m2Num 0 3 1 2 3 3 = 8 * explicitZ 0 3 1 2 3 3 := by decide
 129theorem e_031300 : m2Num 0 3 1 3 0 0 = 8 * explicitZ 0 3 1 3 0 0 := by decide
 130theorem e_031301 : m2Num 0 3 1 3 0 1 = 8 * explicitZ 0 3 1 3 0 1 := by decide
 131theorem e_031302 : m2Num 0 3 1 3 0 2 = 8 * explicitZ 0 3 1 3 0 2 := by decide
 132theorem e_031303 : m2Num 0 3 1 3 0 3 = 8 * explicitZ 0 3 1 3 0 3 := by decide
 133theorem e_031310 : m2Num 0 3 1 3 1 0 = 8 * explicitZ 0 3 1 3 1 0 := by decide
 134theorem e_031311 : m2Num 0 3 1 3 1 1 = 8 * explicitZ 0 3 1 3 1 1 := by decide
 135theorem e_031312 : m2Num 0 3 1 3 1 2 = 8 * explicitZ 0 3 1 3 1 2 := by decide
 136theorem e_031313 : m2Num 0 3 1 3 1 3 = 8 * explicitZ 0 3 1 3 1 3 := by decide
 137theorem e_031320 : m2Num 0 3 1 3 2 0 = 8 * explicitZ 0 3 1 3 2 0 := by decide
 138theorem e_031321 : m2Num 0 3 1 3 2 1 = 8 * explicitZ 0 3 1 3 2 1 := by decide
 139theorem e_031322 : m2Num 0 3 1 3 2 2 = 8 * explicitZ 0 3 1 3 2 2 := by decide
 140theorem e_031323 : m2Num 0 3 1 3 2 3 = 8 * explicitZ 0 3 1 3 2 3 := by decide
 141theorem e_031330 : m2Num 0 3 1 3 3 0 = 8 * explicitZ 0 3 1 3 3 0 := by decide
 142theorem e_031331 : m2Num 0 3 1 3 3 1 = 8 * explicitZ 0 3 1 3 3 1 := by decide
 143theorem e_031332 : m2Num 0 3 1 3 3 2 = 8 * explicitZ 0 3 1 3 3 2 := by decide
 144theorem e_031333 : m2Num 0 3 1 3 3 3 = 8 * explicitZ 0 3 1 3 3 3 := by decide
 145theorem e_032000 : m2Num 0 3 2 0 0 0 = 8 * explicitZ 0 3 2 0 0 0 := by decide
 146theorem e_032001 : m2Num 0 3 2 0 0 1 = 8 * explicitZ 0 3 2 0 0 1 := by decide
 147theorem e_032002 : m2Num 0 3 2 0 0 2 = 8 * explicitZ 0 3 2 0 0 2 := by decide
 148theorem e_032003 : m2Num 0 3 2 0 0 3 = 8 * explicitZ 0 3 2 0 0 3 := by decide
 149theorem e_032010 : m2Num 0 3 2 0 1 0 = 8 * explicitZ 0 3 2 0 1 0 := by decide
 150theorem e_032011 : m2Num 0 3 2 0 1 1 = 8 * explicitZ 0 3 2 0 1 1 := by decide
 151theorem e_032012 : m2Num 0 3 2 0 1 2 = 8 * explicitZ 0 3 2 0 1 2 := by decide
 152theorem e_032013 : m2Num 0 3 2 0 1 3 = 8 * explicitZ 0 3 2 0 1 3 := by decide
 153theorem e_032020 : m2Num 0 3 2 0 2 0 = 8 * explicitZ 0 3 2 0 2 0 := by decide
 154theorem e_032021 : m2Num 0 3 2 0 2 1 = 8 * explicitZ 0 3 2 0 2 1 := by decide
 155theorem e_032022 : m2Num 0 3 2 0 2 2 = 8 * explicitZ 0 3 2 0 2 2 := by decide
 156theorem e_032023 : m2Num 0 3 2 0 2 3 = 8 * explicitZ 0 3 2 0 2 3 := by decide
 157theorem e_032030 : m2Num 0 3 2 0 3 0 = 8 * explicitZ 0 3 2 0 3 0 := by decide
 158theorem e_032031 : m2Num 0 3 2 0 3 1 = 8 * explicitZ 0 3 2 0 3 1 := by decide
 159theorem e_032032 : m2Num 0 3 2 0 3 2 = 8 * explicitZ 0 3 2 0 3 2 := by decide
 160theorem e_032033 : m2Num 0 3 2 0 3 3 = 8 * explicitZ 0 3 2 0 3 3 := by decide
 161theorem e_032100 : m2Num 0 3 2 1 0 0 = 8 * explicitZ 0 3 2 1 0 0 := by decide
 162theorem e_032101 : m2Num 0 3 2 1 0 1 = 8 * explicitZ 0 3 2 1 0 1 := by decide
 163theorem e_032102 : m2Num 0 3 2 1 0 2 = 8 * explicitZ 0 3 2 1 0 2 := by decide
 164theorem e_032103 : m2Num 0 3 2 1 0 3 = 8 * explicitZ 0 3 2 1 0 3 := by decide
 165theorem e_032110 : m2Num 0 3 2 1 1 0 = 8 * explicitZ 0 3 2 1 1 0 := by decide
 166theorem e_032111 : m2Num 0 3 2 1 1 1 = 8 * explicitZ 0 3 2 1 1 1 := by decide
 167theorem e_032112 : m2Num 0 3 2 1 1 2 = 8 * explicitZ 0 3 2 1 1 2 := by decide
 168theorem e_032113 : m2Num 0 3 2 1 1 3 = 8 * explicitZ 0 3 2 1 1 3 := by decide
 169theorem e_032120 : m2Num 0 3 2 1 2 0 = 8 * explicitZ 0 3 2 1 2 0 := by decide
 170theorem e_032121 : m2Num 0 3 2 1 2 1 = 8 * explicitZ 0 3 2 1 2 1 := by decide
 171theorem e_032122 : m2Num 0 3 2 1 2 2 = 8 * explicitZ 0 3 2 1 2 2 := by decide
 172theorem e_032123 : m2Num 0 3 2 1 2 3 = 8 * explicitZ 0 3 2 1 2 3 := by decide
 173theorem e_032130 : m2Num 0 3 2 1 3 0 = 8 * explicitZ 0 3 2 1 3 0 := by decide
 174theorem e_032131 : m2Num 0 3 2 1 3 1 = 8 * explicitZ 0 3 2 1 3 1 := by decide
 175theorem e_032132 : m2Num 0 3 2 1 3 2 = 8 * explicitZ 0 3 2 1 3 2 := by decide
 176theorem e_032133 : m2Num 0 3 2 1 3 3 = 8 * explicitZ 0 3 2 1 3 3 := by decide
 177theorem e_032200 : m2Num 0 3 2 2 0 0 = 8 * explicitZ 0 3 2 2 0 0 := by decide
 178theorem e_032201 : m2Num 0 3 2 2 0 1 = 8 * explicitZ 0 3 2 2 0 1 := by decide
 179theorem e_032202 : m2Num 0 3 2 2 0 2 = 8 * explicitZ 0 3 2 2 0 2 := by decide
 180theorem e_032203 : m2Num 0 3 2 2 0 3 = 8 * explicitZ 0 3 2 2 0 3 := by decide
 181theorem e_032210 : m2Num 0 3 2 2 1 0 = 8 * explicitZ 0 3 2 2 1 0 := by decide
 182theorem e_032211 : m2Num 0 3 2 2 1 1 = 8 * explicitZ 0 3 2 2 1 1 := by decide
 183theorem e_032212 : m2Num 0 3 2 2 1 2 = 8 * explicitZ 0 3 2 2 1 2 := by decide
 184theorem e_032213 : m2Num 0 3 2 2 1 3 = 8 * explicitZ 0 3 2 2 1 3 := by decide
 185theorem e_032220 : m2Num 0 3 2 2 2 0 = 8 * explicitZ 0 3 2 2 2 0 := by decide
 186theorem e_032221 : m2Num 0 3 2 2 2 1 = 8 * explicitZ 0 3 2 2 2 1 := by decide
 187theorem e_032222 : m2Num 0 3 2 2 2 2 = 8 * explicitZ 0 3 2 2 2 2 := by decide
 188theorem e_032223 : m2Num 0 3 2 2 2 3 = 8 * explicitZ 0 3 2 2 2 3 := by decide
 189theorem e_032230 : m2Num 0 3 2 2 3 0 = 8 * explicitZ 0 3 2 2 3 0 := by decide
 190theorem e_032231 : m2Num 0 3 2 2 3 1 = 8 * explicitZ 0 3 2 2 3 1 := by decide
 191theorem e_032232 : m2Num 0 3 2 2 3 2 = 8 * explicitZ 0 3 2 2 3 2 := by decide
 192theorem e_032233 : m2Num 0 3 2 2 3 3 = 8 * explicitZ 0 3 2 2 3 3 := by decide
 193theorem e_032300 : m2Num 0 3 2 3 0 0 = 8 * explicitZ 0 3 2 3 0 0 := by decide
 194theorem e_032301 : m2Num 0 3 2 3 0 1 = 8 * explicitZ 0 3 2 3 0 1 := by decide
 195theorem e_032302 : m2Num 0 3 2 3 0 2 = 8 * explicitZ 0 3 2 3 0 2 := by decide
 196theorem e_032303 : m2Num 0 3 2 3 0 3 = 8 * explicitZ 0 3 2 3 0 3 := by decide
 197theorem e_032310 : m2Num 0 3 2 3 1 0 = 8 * explicitZ 0 3 2 3 1 0 := by decide
 198theorem e_032311 : m2Num 0 3 2 3 1 1 = 8 * explicitZ 0 3 2 3 1 1 := by decide
 199theorem e_032312 : m2Num 0 3 2 3 1 2 = 8 * explicitZ 0 3 2 3 1 2 := by decide
 200theorem e_032313 : m2Num 0 3 2 3 1 3 = 8 * explicitZ 0 3 2 3 1 3 := by decide
 201theorem e_032320 : m2Num 0 3 2 3 2 0 = 8 * explicitZ 0 3 2 3 2 0 := by decide
 202theorem e_032321 : m2Num 0 3 2 3 2 1 = 8 * explicitZ 0 3 2 3 2 1 := by decide
 203theorem e_032322 : m2Num 0 3 2 3 2 2 = 8 * explicitZ 0 3 2 3 2 2 := by decide
 204theorem e_032323 : m2Num 0 3 2 3 2 3 = 8 * explicitZ 0 3 2 3 2 3 := by decide
 205theorem e_032330 : m2Num 0 3 2 3 3 0 = 8 * explicitZ 0 3 2 3 3 0 := by decide
 206theorem e_032331 : m2Num 0 3 2 3 3 1 = 8 * explicitZ 0 3 2 3 3 1 := by decide
 207theorem e_032332 : m2Num 0 3 2 3 3 2 = 8 * explicitZ 0 3 2 3 3 2 := by decide
 208theorem e_032333 : m2Num 0 3 2 3 3 3 = 8 * explicitZ 0 3 2 3 3 3 := by decide
 209theorem e_033000 : m2Num 0 3 3 0 0 0 = 8 * explicitZ 0 3 3 0 0 0 := by decide
 210theorem e_033001 : m2Num 0 3 3 0 0 1 = 8 * explicitZ 0 3 3 0 0 1 := by decide
 211theorem e_033002 : m2Num 0 3 3 0 0 2 = 8 * explicitZ 0 3 3 0 0 2 := by decide
 212theorem e_033003 : m2Num 0 3 3 0 0 3 = 8 * explicitZ 0 3 3 0 0 3 := by decide
 213theorem e_033010 : m2Num 0 3 3 0 1 0 = 8 * explicitZ 0 3 3 0 1 0 := by decide
 214theorem e_033011 : m2Num 0 3 3 0 1 1 = 8 * explicitZ 0 3 3 0 1 1 := by decide
 215theorem e_033012 : m2Num 0 3 3 0 1 2 = 8 * explicitZ 0 3 3 0 1 2 := by decide
 216theorem e_033013 : m2Num 0 3 3 0 1 3 = 8 * explicitZ 0 3 3 0 1 3 := by decide
 217theorem e_033020 : m2Num 0 3 3 0 2 0 = 8 * explicitZ 0 3 3 0 2 0 := by decide
 218theorem e_033021 : m2Num 0 3 3 0 2 1 = 8 * explicitZ 0 3 3 0 2 1 := by decide
 219theorem e_033022 : m2Num 0 3 3 0 2 2 = 8 * explicitZ 0 3 3 0 2 2 := by decide
 220theorem e_033023 : m2Num 0 3 3 0 2 3 = 8 * explicitZ 0 3 3 0 2 3 := by decide
 221theorem e_033030 : m2Num 0 3 3 0 3 0 = 8 * explicitZ 0 3 3 0 3 0 := by decide
 222theorem e_033031 : m2Num 0 3 3 0 3 1 = 8 * explicitZ 0 3 3 0 3 1 := by decide
 223theorem e_033032 : m2Num 0 3 3 0 3 2 = 8 * explicitZ 0 3 3 0 3 2 := by decide
 224theorem e_033033 : m2Num 0 3 3 0 3 3 = 8 * explicitZ 0 3 3 0 3 3 := by decide
 225theorem e_033100 : m2Num 0 3 3 1 0 0 = 8 * explicitZ 0 3 3 1 0 0 := by decide
 226theorem e_033101 : m2Num 0 3 3 1 0 1 = 8 * explicitZ 0 3 3 1 0 1 := by decide
 227theorem e_033102 : m2Num 0 3 3 1 0 2 = 8 * explicitZ 0 3 3 1 0 2 := by decide
 228theorem e_033103 : m2Num 0 3 3 1 0 3 = 8 * explicitZ 0 3 3 1 0 3 := by decide
 229theorem e_033110 : m2Num 0 3 3 1 1 0 = 8 * explicitZ 0 3 3 1 1 0 := by decide
 230theorem e_033111 : m2Num 0 3 3 1 1 1 = 8 * explicitZ 0 3 3 1 1 1 := by decide
 231theorem e_033112 : m2Num 0 3 3 1 1 2 = 8 * explicitZ 0 3 3 1 1 2 := by decide
 232theorem e_033113 : m2Num 0 3 3 1 1 3 = 8 * explicitZ 0 3 3 1 1 3 := by decide
 233theorem e_033120 : m2Num 0 3 3 1 2 0 = 8 * explicitZ 0 3 3 1 2 0 := by decide
 234theorem e_033121 : m2Num 0 3 3 1 2 1 = 8 * explicitZ 0 3 3 1 2 1 := by decide
 235theorem e_033122 : m2Num 0 3 3 1 2 2 = 8 * explicitZ 0 3 3 1 2 2 := by decide
 236theorem e_033123 : m2Num 0 3 3 1 2 3 = 8 * explicitZ 0 3 3 1 2 3 := by decide
 237theorem e_033130 : m2Num 0 3 3 1 3 0 = 8 * explicitZ 0 3 3 1 3 0 := by decide
 238theorem e_033131 : m2Num 0 3 3 1 3 1 = 8 * explicitZ 0 3 3 1 3 1 := by decide
 239theorem e_033132 : m2Num 0 3 3 1 3 2 = 8 * explicitZ 0 3 3 1 3 2 := by decide
 240theorem e_033133 : m2Num 0 3 3 1 3 3 = 8 * explicitZ 0 3 3 1 3 3 := by decide
 241theorem e_033200 : m2Num 0 3 3 2 0 0 = 8 * explicitZ 0 3 3 2 0 0 := by decide
 242theorem e_033201 : m2Num 0 3 3 2 0 1 = 8 * explicitZ 0 3 3 2 0 1 := by decide
 243theorem e_033202 : m2Num 0 3 3 2 0 2 = 8 * explicitZ 0 3 3 2 0 2 := by decide
 244theorem e_033203 : m2Num 0 3 3 2 0 3 = 8 * explicitZ 0 3 3 2 0 3 := by decide
 245theorem e_033210 : m2Num 0 3 3 2 1 0 = 8 * explicitZ 0 3 3 2 1 0 := by decide
 246theorem e_033211 : m2Num 0 3 3 2 1 1 = 8 * explicitZ 0 3 3 2 1 1 := by decide
 247theorem e_033212 : m2Num 0 3 3 2 1 2 = 8 * explicitZ 0 3 3 2 1 2 := by decide
 248theorem e_033213 : m2Num 0 3 3 2 1 3 = 8 * explicitZ 0 3 3 2 1 3 := by decide
 249theorem e_033220 : m2Num 0 3 3 2 2 0 = 8 * explicitZ 0 3 3 2 2 0 := by decide
 250theorem e_033221 : m2Num 0 3 3 2 2 1 = 8 * explicitZ 0 3 3 2 2 1 := by decide
 251theorem e_033222 : m2Num 0 3 3 2 2 2 = 8 * explicitZ 0 3 3 2 2 2 := by decide
 252theorem e_033223 : m2Num 0 3 3 2 2 3 = 8 * explicitZ 0 3 3 2 2 3 := by decide
 253theorem e_033230 : m2Num 0 3 3 2 3 0 = 8 * explicitZ 0 3 3 2 3 0 := by decide
 254theorem e_033231 : m2Num 0 3 3 2 3 1 = 8 * explicitZ 0 3 3 2 3 1 := by decide
 255theorem e_033232 : m2Num 0 3 3 2 3 2 = 8 * explicitZ 0 3 3 2 3 2 := by decide
 256theorem e_033233 : m2Num 0 3 3 2 3 3 = 8 * explicitZ 0 3 3 2 3 3 := by decide
 257theorem e_033300 : m2Num 0 3 3 3 0 0 = 8 * explicitZ 0 3 3 3 0 0 := by decide
 258theorem e_033301 : m2Num 0 3 3 3 0 1 = 8 * explicitZ 0 3 3 3 0 1 := by decide
 259theorem e_033302 : m2Num 0 3 3 3 0 2 = 8 * explicitZ 0 3 3 3 0 2 := by decide
 260theorem e_033303 : m2Num 0 3 3 3 0 3 = 8 * explicitZ 0 3 3 3 0 3 := by decide
 261theorem e_033310 : m2Num 0 3 3 3 1 0 = 8 * explicitZ 0 3 3 3 1 0 := by decide
 262theorem e_033311 : m2Num 0 3 3 3 1 1 = 8 * explicitZ 0 3 3 3 1 1 := by decide
 263theorem e_033312 : m2Num 0 3 3 3 1 2 = 8 * explicitZ 0 3 3 3 1 2 := by decide
 264theorem e_033313 : m2Num 0 3 3 3 1 3 = 8 * explicitZ 0 3 3 3 1 3 := by decide
 265theorem e_033320 : m2Num 0 3 3 3 2 0 = 8 * explicitZ 0 3 3 3 2 0 := by decide
 266theorem e_033321 : m2Num 0 3 3 3 2 1 = 8 * explicitZ 0 3 3 3 2 1 := by decide
 267theorem e_033322 : m2Num 0 3 3 3 2 2 = 8 * explicitZ 0 3 3 3 2 2 := by decide
 268theorem e_033323 : m2Num 0 3 3 3 2 3 = 8 * explicitZ 0 3 3 3 2 3 := by decide
 269theorem e_033330 : m2Num 0 3 3 3 3 0 = 8 * explicitZ 0 3 3 3 3 0 := by decide
 270theorem e_033331 : m2Num 0 3 3 3 3 1 = 8 * explicitZ 0 3 3 3 3 1 := by decide
 271theorem e_033332 : m2Num 0 3 3 3 3 2 = 8 * explicitZ 0 3 3 3 3 2 := by decide
 272theorem e_033333 : m2Num 0 3 3 3 3 3 = 8 * explicitZ 0 3 3 3 3 3 := by decide
 273
 274end M2NumChunk03
 275end ReggeExactMidpointM2TTIdentity4D
 276end Analysis
 277end Gravity
 278end IndisputableMonolith
 279