`IndisputableMonolith.Gravity.Analysis.ReggeExactMidpointM2TTIdentity4DM2NumChunk01`

IndisputableMonolith/Gravity/Analysis/ReggeExactMidpointM2TTIdentity4DM2NumChunk01.lean · 279 lines · 256 declarations
Explainer status: ready · generated 2026-08-13 19:52:16.166879+00:00
   1import Mathlib
   2import IndisputableMonolith.Gravity.Analysis.ReggeExactMidpointM2TTIdentity4DKernelCert
   3
   4/-! m2Num = 8·explicitZ, chunk 1 (256 kernel decides). -/
   5
   6namespace IndisputableMonolith
   7namespace Gravity
   8namespace Analysis
   9namespace ReggeExactMidpointM2TTIdentity4D
  10namespace M2NumChunk01
  11
  12open KernelCert
  13
  14set_option maxRecDepth 100000
  15set_option maxHeartbeats 200000000
  16
  17theorem e_010000 : m2Num 0 1 0 0 0 0 = 8 * explicitZ 0 1 0 0 0 0 := by decide
  18theorem e_010001 : m2Num 0 1 0 0 0 1 = 8 * explicitZ 0 1 0 0 0 1 := by decide
  19theorem e_010002 : m2Num 0 1 0 0 0 2 = 8 * explicitZ 0 1 0 0 0 2 := by decide
  20theorem e_010003 : m2Num 0 1 0 0 0 3 = 8 * explicitZ 0 1 0 0 0 3 := by decide
  21theorem e_010010 : m2Num 0 1 0 0 1 0 = 8 * explicitZ 0 1 0 0 1 0 := by decide
  22theorem e_010011 : m2Num 0 1 0 0 1 1 = 8 * explicitZ 0 1 0 0 1 1 := by decide
  23theorem e_010012 : m2Num 0 1 0 0 1 2 = 8 * explicitZ 0 1 0 0 1 2 := by decide
  24theorem e_010013 : m2Num 0 1 0 0 1 3 = 8 * explicitZ 0 1 0 0 1 3 := by decide
  25theorem e_010020 : m2Num 0 1 0 0 2 0 = 8 * explicitZ 0 1 0 0 2 0 := by decide
  26theorem e_010021 : m2Num 0 1 0 0 2 1 = 8 * explicitZ 0 1 0 0 2 1 := by decide
  27theorem e_010022 : m2Num 0 1 0 0 2 2 = 8 * explicitZ 0 1 0 0 2 2 := by decide
  28theorem e_010023 : m2Num 0 1 0 0 2 3 = 8 * explicitZ 0 1 0 0 2 3 := by decide
  29theorem e_010030 : m2Num 0 1 0 0 3 0 = 8 * explicitZ 0 1 0 0 3 0 := by decide
  30theorem e_010031 : m2Num 0 1 0 0 3 1 = 8 * explicitZ 0 1 0 0 3 1 := by decide
  31theorem e_010032 : m2Num 0 1 0 0 3 2 = 8 * explicitZ 0 1 0 0 3 2 := by decide
  32theorem e_010033 : m2Num 0 1 0 0 3 3 = 8 * explicitZ 0 1 0 0 3 3 := by decide
  33theorem e_010100 : m2Num 0 1 0 1 0 0 = 8 * explicitZ 0 1 0 1 0 0 := by decide
  34theorem e_010101 : m2Num 0 1 0 1 0 1 = 8 * explicitZ 0 1 0 1 0 1 := by decide
  35theorem e_010102 : m2Num 0 1 0 1 0 2 = 8 * explicitZ 0 1 0 1 0 2 := by decide
  36theorem e_010103 : m2Num 0 1 0 1 0 3 = 8 * explicitZ 0 1 0 1 0 3 := by decide
  37theorem e_010110 : m2Num 0 1 0 1 1 0 = 8 * explicitZ 0 1 0 1 1 0 := by decide
  38theorem e_010111 : m2Num 0 1 0 1 1 1 = 8 * explicitZ 0 1 0 1 1 1 := by decide
  39theorem e_010112 : m2Num 0 1 0 1 1 2 = 8 * explicitZ 0 1 0 1 1 2 := by decide
  40theorem e_010113 : m2Num 0 1 0 1 1 3 = 8 * explicitZ 0 1 0 1 1 3 := by decide
  41theorem e_010120 : m2Num 0 1 0 1 2 0 = 8 * explicitZ 0 1 0 1 2 0 := by decide
  42theorem e_010121 : m2Num 0 1 0 1 2 1 = 8 * explicitZ 0 1 0 1 2 1 := by decide
  43theorem e_010122 : m2Num 0 1 0 1 2 2 = 8 * explicitZ 0 1 0 1 2 2 := by decide
  44theorem e_010123 : m2Num 0 1 0 1 2 3 = 8 * explicitZ 0 1 0 1 2 3 := by decide
  45theorem e_010130 : m2Num 0 1 0 1 3 0 = 8 * explicitZ 0 1 0 1 3 0 := by decide
  46theorem e_010131 : m2Num 0 1 0 1 3 1 = 8 * explicitZ 0 1 0 1 3 1 := by decide
  47theorem e_010132 : m2Num 0 1 0 1 3 2 = 8 * explicitZ 0 1 0 1 3 2 := by decide
  48theorem e_010133 : m2Num 0 1 0 1 3 3 = 8 * explicitZ 0 1 0 1 3 3 := by decide
  49theorem e_010200 : m2Num 0 1 0 2 0 0 = 8 * explicitZ 0 1 0 2 0 0 := by decide
  50theorem e_010201 : m2Num 0 1 0 2 0 1 = 8 * explicitZ 0 1 0 2 0 1 := by decide
  51theorem e_010202 : m2Num 0 1 0 2 0 2 = 8 * explicitZ 0 1 0 2 0 2 := by decide
  52theorem e_010203 : m2Num 0 1 0 2 0 3 = 8 * explicitZ 0 1 0 2 0 3 := by decide
  53theorem e_010210 : m2Num 0 1 0 2 1 0 = 8 * explicitZ 0 1 0 2 1 0 := by decide
  54theorem e_010211 : m2Num 0 1 0 2 1 1 = 8 * explicitZ 0 1 0 2 1 1 := by decide
  55theorem e_010212 : m2Num 0 1 0 2 1 2 = 8 * explicitZ 0 1 0 2 1 2 := by decide
  56theorem e_010213 : m2Num 0 1 0 2 1 3 = 8 * explicitZ 0 1 0 2 1 3 := by decide
  57theorem e_010220 : m2Num 0 1 0 2 2 0 = 8 * explicitZ 0 1 0 2 2 0 := by decide
  58theorem e_010221 : m2Num 0 1 0 2 2 1 = 8 * explicitZ 0 1 0 2 2 1 := by decide
  59theorem e_010222 : m2Num 0 1 0 2 2 2 = 8 * explicitZ 0 1 0 2 2 2 := by decide
  60theorem e_010223 : m2Num 0 1 0 2 2 3 = 8 * explicitZ 0 1 0 2 2 3 := by decide
  61theorem e_010230 : m2Num 0 1 0 2 3 0 = 8 * explicitZ 0 1 0 2 3 0 := by decide
  62theorem e_010231 : m2Num 0 1 0 2 3 1 = 8 * explicitZ 0 1 0 2 3 1 := by decide
  63theorem e_010232 : m2Num 0 1 0 2 3 2 = 8 * explicitZ 0 1 0 2 3 2 := by decide
  64theorem e_010233 : m2Num 0 1 0 2 3 3 = 8 * explicitZ 0 1 0 2 3 3 := by decide
  65theorem e_010300 : m2Num 0 1 0 3 0 0 = 8 * explicitZ 0 1 0 3 0 0 := by decide
  66theorem e_010301 : m2Num 0 1 0 3 0 1 = 8 * explicitZ 0 1 0 3 0 1 := by decide
  67theorem e_010302 : m2Num 0 1 0 3 0 2 = 8 * explicitZ 0 1 0 3 0 2 := by decide
  68theorem e_010303 : m2Num 0 1 0 3 0 3 = 8 * explicitZ 0 1 0 3 0 3 := by decide
  69theorem e_010310 : m2Num 0 1 0 3 1 0 = 8 * explicitZ 0 1 0 3 1 0 := by decide
  70theorem e_010311 : m2Num 0 1 0 3 1 1 = 8 * explicitZ 0 1 0 3 1 1 := by decide
  71theorem e_010312 : m2Num 0 1 0 3 1 2 = 8 * explicitZ 0 1 0 3 1 2 := by decide
  72theorem e_010313 : m2Num 0 1 0 3 1 3 = 8 * explicitZ 0 1 0 3 1 3 := by decide
  73theorem e_010320 : m2Num 0 1 0 3 2 0 = 8 * explicitZ 0 1 0 3 2 0 := by decide
  74theorem e_010321 : m2Num 0 1 0 3 2 1 = 8 * explicitZ 0 1 0 3 2 1 := by decide
  75theorem e_010322 : m2Num 0 1 0 3 2 2 = 8 * explicitZ 0 1 0 3 2 2 := by decide
  76theorem e_010323 : m2Num 0 1 0 3 2 3 = 8 * explicitZ 0 1 0 3 2 3 := by decide
  77theorem e_010330 : m2Num 0 1 0 3 3 0 = 8 * explicitZ 0 1 0 3 3 0 := by decide
  78theorem e_010331 : m2Num 0 1 0 3 3 1 = 8 * explicitZ 0 1 0 3 3 1 := by decide
  79theorem e_010332 : m2Num 0 1 0 3 3 2 = 8 * explicitZ 0 1 0 3 3 2 := by decide
  80theorem e_010333 : m2Num 0 1 0 3 3 3 = 8 * explicitZ 0 1 0 3 3 3 := by decide
  81theorem e_011000 : m2Num 0 1 1 0 0 0 = 8 * explicitZ 0 1 1 0 0 0 := by decide
  82theorem e_011001 : m2Num 0 1 1 0 0 1 = 8 * explicitZ 0 1 1 0 0 1 := by decide
  83theorem e_011002 : m2Num 0 1 1 0 0 2 = 8 * explicitZ 0 1 1 0 0 2 := by decide
  84theorem e_011003 : m2Num 0 1 1 0 0 3 = 8 * explicitZ 0 1 1 0 0 3 := by decide
  85theorem e_011010 : m2Num 0 1 1 0 1 0 = 8 * explicitZ 0 1 1 0 1 0 := by decide
  86theorem e_011011 : m2Num 0 1 1 0 1 1 = 8 * explicitZ 0 1 1 0 1 1 := by decide
  87theorem e_011012 : m2Num 0 1 1 0 1 2 = 8 * explicitZ 0 1 1 0 1 2 := by decide
  88theorem e_011013 : m2Num 0 1 1 0 1 3 = 8 * explicitZ 0 1 1 0 1 3 := by decide
  89theorem e_011020 : m2Num 0 1 1 0 2 0 = 8 * explicitZ 0 1 1 0 2 0 := by decide
  90theorem e_011021 : m2Num 0 1 1 0 2 1 = 8 * explicitZ 0 1 1 0 2 1 := by decide
  91theorem e_011022 : m2Num 0 1 1 0 2 2 = 8 * explicitZ 0 1 1 0 2 2 := by decide
  92theorem e_011023 : m2Num 0 1 1 0 2 3 = 8 * explicitZ 0 1 1 0 2 3 := by decide
  93theorem e_011030 : m2Num 0 1 1 0 3 0 = 8 * explicitZ 0 1 1 0 3 0 := by decide
  94theorem e_011031 : m2Num 0 1 1 0 3 1 = 8 * explicitZ 0 1 1 0 3 1 := by decide
  95theorem e_011032 : m2Num 0 1 1 0 3 2 = 8 * explicitZ 0 1 1 0 3 2 := by decide
  96theorem e_011033 : m2Num 0 1 1 0 3 3 = 8 * explicitZ 0 1 1 0 3 3 := by decide
  97theorem e_011100 : m2Num 0 1 1 1 0 0 = 8 * explicitZ 0 1 1 1 0 0 := by decide
  98theorem e_011101 : m2Num 0 1 1 1 0 1 = 8 * explicitZ 0 1 1 1 0 1 := by decide
  99theorem e_011102 : m2Num 0 1 1 1 0 2 = 8 * explicitZ 0 1 1 1 0 2 := by decide
 100theorem e_011103 : m2Num 0 1 1 1 0 3 = 8 * explicitZ 0 1 1 1 0 3 := by decide
 101theorem e_011110 : m2Num 0 1 1 1 1 0 = 8 * explicitZ 0 1 1 1 1 0 := by decide
 102theorem e_011111 : m2Num 0 1 1 1 1 1 = 8 * explicitZ 0 1 1 1 1 1 := by decide
 103theorem e_011112 : m2Num 0 1 1 1 1 2 = 8 * explicitZ 0 1 1 1 1 2 := by decide
 104theorem e_011113 : m2Num 0 1 1 1 1 3 = 8 * explicitZ 0 1 1 1 1 3 := by decide
 105theorem e_011120 : m2Num 0 1 1 1 2 0 = 8 * explicitZ 0 1 1 1 2 0 := by decide
 106theorem e_011121 : m2Num 0 1 1 1 2 1 = 8 * explicitZ 0 1 1 1 2 1 := by decide
 107theorem e_011122 : m2Num 0 1 1 1 2 2 = 8 * explicitZ 0 1 1 1 2 2 := by decide
 108theorem e_011123 : m2Num 0 1 1 1 2 3 = 8 * explicitZ 0 1 1 1 2 3 := by decide
 109theorem e_011130 : m2Num 0 1 1 1 3 0 = 8 * explicitZ 0 1 1 1 3 0 := by decide
 110theorem e_011131 : m2Num 0 1 1 1 3 1 = 8 * explicitZ 0 1 1 1 3 1 := by decide
 111theorem e_011132 : m2Num 0 1 1 1 3 2 = 8 * explicitZ 0 1 1 1 3 2 := by decide
 112theorem e_011133 : m2Num 0 1 1 1 3 3 = 8 * explicitZ 0 1 1 1 3 3 := by decide
 113theorem e_011200 : m2Num 0 1 1 2 0 0 = 8 * explicitZ 0 1 1 2 0 0 := by decide
 114theorem e_011201 : m2Num 0 1 1 2 0 1 = 8 * explicitZ 0 1 1 2 0 1 := by decide
 115theorem e_011202 : m2Num 0 1 1 2 0 2 = 8 * explicitZ 0 1 1 2 0 2 := by decide
 116theorem e_011203 : m2Num 0 1 1 2 0 3 = 8 * explicitZ 0 1 1 2 0 3 := by decide
 117theorem e_011210 : m2Num 0 1 1 2 1 0 = 8 * explicitZ 0 1 1 2 1 0 := by decide
 118theorem e_011211 : m2Num 0 1 1 2 1 1 = 8 * explicitZ 0 1 1 2 1 1 := by decide
 119theorem e_011212 : m2Num 0 1 1 2 1 2 = 8 * explicitZ 0 1 1 2 1 2 := by decide
 120theorem e_011213 : m2Num 0 1 1 2 1 3 = 8 * explicitZ 0 1 1 2 1 3 := by decide
 121theorem e_011220 : m2Num 0 1 1 2 2 0 = 8 * explicitZ 0 1 1 2 2 0 := by decide
 122theorem e_011221 : m2Num 0 1 1 2 2 1 = 8 * explicitZ 0 1 1 2 2 1 := by decide
 123theorem e_011222 : m2Num 0 1 1 2 2 2 = 8 * explicitZ 0 1 1 2 2 2 := by decide
 124theorem e_011223 : m2Num 0 1 1 2 2 3 = 8 * explicitZ 0 1 1 2 2 3 := by decide
 125theorem e_011230 : m2Num 0 1 1 2 3 0 = 8 * explicitZ 0 1 1 2 3 0 := by decide
 126theorem e_011231 : m2Num 0 1 1 2 3 1 = 8 * explicitZ 0 1 1 2 3 1 := by decide
 127theorem e_011232 : m2Num 0 1 1 2 3 2 = 8 * explicitZ 0 1 1 2 3 2 := by decide
 128theorem e_011233 : m2Num 0 1 1 2 3 3 = 8 * explicitZ 0 1 1 2 3 3 := by decide
 129theorem e_011300 : m2Num 0 1 1 3 0 0 = 8 * explicitZ 0 1 1 3 0 0 := by decide
 130theorem e_011301 : m2Num 0 1 1 3 0 1 = 8 * explicitZ 0 1 1 3 0 1 := by decide
 131theorem e_011302 : m2Num 0 1 1 3 0 2 = 8 * explicitZ 0 1 1 3 0 2 := by decide
 132theorem e_011303 : m2Num 0 1 1 3 0 3 = 8 * explicitZ 0 1 1 3 0 3 := by decide
 133theorem e_011310 : m2Num 0 1 1 3 1 0 = 8 * explicitZ 0 1 1 3 1 0 := by decide
 134theorem e_011311 : m2Num 0 1 1 3 1 1 = 8 * explicitZ 0 1 1 3 1 1 := by decide
 135theorem e_011312 : m2Num 0 1 1 3 1 2 = 8 * explicitZ 0 1 1 3 1 2 := by decide
 136theorem e_011313 : m2Num 0 1 1 3 1 3 = 8 * explicitZ 0 1 1 3 1 3 := by decide
 137theorem e_011320 : m2Num 0 1 1 3 2 0 = 8 * explicitZ 0 1 1 3 2 0 := by decide
 138theorem e_011321 : m2Num 0 1 1 3 2 1 = 8 * explicitZ 0 1 1 3 2 1 := by decide
 139theorem e_011322 : m2Num 0 1 1 3 2 2 = 8 * explicitZ 0 1 1 3 2 2 := by decide
 140theorem e_011323 : m2Num 0 1 1 3 2 3 = 8 * explicitZ 0 1 1 3 2 3 := by decide
 141theorem e_011330 : m2Num 0 1 1 3 3 0 = 8 * explicitZ 0 1 1 3 3 0 := by decide
 142theorem e_011331 : m2Num 0 1 1 3 3 1 = 8 * explicitZ 0 1 1 3 3 1 := by decide
 143theorem e_011332 : m2Num 0 1 1 3 3 2 = 8 * explicitZ 0 1 1 3 3 2 := by decide
 144theorem e_011333 : m2Num 0 1 1 3 3 3 = 8 * explicitZ 0 1 1 3 3 3 := by decide
 145theorem e_012000 : m2Num 0 1 2 0 0 0 = 8 * explicitZ 0 1 2 0 0 0 := by decide
 146theorem e_012001 : m2Num 0 1 2 0 0 1 = 8 * explicitZ 0 1 2 0 0 1 := by decide
 147theorem e_012002 : m2Num 0 1 2 0 0 2 = 8 * explicitZ 0 1 2 0 0 2 := by decide
 148theorem e_012003 : m2Num 0 1 2 0 0 3 = 8 * explicitZ 0 1 2 0 0 3 := by decide
 149theorem e_012010 : m2Num 0 1 2 0 1 0 = 8 * explicitZ 0 1 2 0 1 0 := by decide
 150theorem e_012011 : m2Num 0 1 2 0 1 1 = 8 * explicitZ 0 1 2 0 1 1 := by decide
 151theorem e_012012 : m2Num 0 1 2 0 1 2 = 8 * explicitZ 0 1 2 0 1 2 := by decide
 152theorem e_012013 : m2Num 0 1 2 0 1 3 = 8 * explicitZ 0 1 2 0 1 3 := by decide
 153theorem e_012020 : m2Num 0 1 2 0 2 0 = 8 * explicitZ 0 1 2 0 2 0 := by decide
 154theorem e_012021 : m2Num 0 1 2 0 2 1 = 8 * explicitZ 0 1 2 0 2 1 := by decide
 155theorem e_012022 : m2Num 0 1 2 0 2 2 = 8 * explicitZ 0 1 2 0 2 2 := by decide
 156theorem e_012023 : m2Num 0 1 2 0 2 3 = 8 * explicitZ 0 1 2 0 2 3 := by decide
 157theorem e_012030 : m2Num 0 1 2 0 3 0 = 8 * explicitZ 0 1 2 0 3 0 := by decide
 158theorem e_012031 : m2Num 0 1 2 0 3 1 = 8 * explicitZ 0 1 2 0 3 1 := by decide
 159theorem e_012032 : m2Num 0 1 2 0 3 2 = 8 * explicitZ 0 1 2 0 3 2 := by decide
 160theorem e_012033 : m2Num 0 1 2 0 3 3 = 8 * explicitZ 0 1 2 0 3 3 := by decide
 161theorem e_012100 : m2Num 0 1 2 1 0 0 = 8 * explicitZ 0 1 2 1 0 0 := by decide
 162theorem e_012101 : m2Num 0 1 2 1 0 1 = 8 * explicitZ 0 1 2 1 0 1 := by decide
 163theorem e_012102 : m2Num 0 1 2 1 0 2 = 8 * explicitZ 0 1 2 1 0 2 := by decide
 164theorem e_012103 : m2Num 0 1 2 1 0 3 = 8 * explicitZ 0 1 2 1 0 3 := by decide
 165theorem e_012110 : m2Num 0 1 2 1 1 0 = 8 * explicitZ 0 1 2 1 1 0 := by decide
 166theorem e_012111 : m2Num 0 1 2 1 1 1 = 8 * explicitZ 0 1 2 1 1 1 := by decide
 167theorem e_012112 : m2Num 0 1 2 1 1 2 = 8 * explicitZ 0 1 2 1 1 2 := by decide
 168theorem e_012113 : m2Num 0 1 2 1 1 3 = 8 * explicitZ 0 1 2 1 1 3 := by decide
 169theorem e_012120 : m2Num 0 1 2 1 2 0 = 8 * explicitZ 0 1 2 1 2 0 := by decide
 170theorem e_012121 : m2Num 0 1 2 1 2 1 = 8 * explicitZ 0 1 2 1 2 1 := by decide
 171theorem e_012122 : m2Num 0 1 2 1 2 2 = 8 * explicitZ 0 1 2 1 2 2 := by decide
 172theorem e_012123 : m2Num 0 1 2 1 2 3 = 8 * explicitZ 0 1 2 1 2 3 := by decide
 173theorem e_012130 : m2Num 0 1 2 1 3 0 = 8 * explicitZ 0 1 2 1 3 0 := by decide
 174theorem e_012131 : m2Num 0 1 2 1 3 1 = 8 * explicitZ 0 1 2 1 3 1 := by decide
 175theorem e_012132 : m2Num 0 1 2 1 3 2 = 8 * explicitZ 0 1 2 1 3 2 := by decide
 176theorem e_012133 : m2Num 0 1 2 1 3 3 = 8 * explicitZ 0 1 2 1 3 3 := by decide
 177theorem e_012200 : m2Num 0 1 2 2 0 0 = 8 * explicitZ 0 1 2 2 0 0 := by decide
 178theorem e_012201 : m2Num 0 1 2 2 0 1 = 8 * explicitZ 0 1 2 2 0 1 := by decide
 179theorem e_012202 : m2Num 0 1 2 2 0 2 = 8 * explicitZ 0 1 2 2 0 2 := by decide
 180theorem e_012203 : m2Num 0 1 2 2 0 3 = 8 * explicitZ 0 1 2 2 0 3 := by decide
 181theorem e_012210 : m2Num 0 1 2 2 1 0 = 8 * explicitZ 0 1 2 2 1 0 := by decide
 182theorem e_012211 : m2Num 0 1 2 2 1 1 = 8 * explicitZ 0 1 2 2 1 1 := by decide
 183theorem e_012212 : m2Num 0 1 2 2 1 2 = 8 * explicitZ 0 1 2 2 1 2 := by decide
 184theorem e_012213 : m2Num 0 1 2 2 1 3 = 8 * explicitZ 0 1 2 2 1 3 := by decide
 185theorem e_012220 : m2Num 0 1 2 2 2 0 = 8 * explicitZ 0 1 2 2 2 0 := by decide
 186theorem e_012221 : m2Num 0 1 2 2 2 1 = 8 * explicitZ 0 1 2 2 2 1 := by decide
 187theorem e_012222 : m2Num 0 1 2 2 2 2 = 8 * explicitZ 0 1 2 2 2 2 := by decide
 188theorem e_012223 : m2Num 0 1 2 2 2 3 = 8 * explicitZ 0 1 2 2 2 3 := by decide
 189theorem e_012230 : m2Num 0 1 2 2 3 0 = 8 * explicitZ 0 1 2 2 3 0 := by decide
 190theorem e_012231 : m2Num 0 1 2 2 3 1 = 8 * explicitZ 0 1 2 2 3 1 := by decide
 191theorem e_012232 : m2Num 0 1 2 2 3 2 = 8 * explicitZ 0 1 2 2 3 2 := by decide
 192theorem e_012233 : m2Num 0 1 2 2 3 3 = 8 * explicitZ 0 1 2 2 3 3 := by decide
 193theorem e_012300 : m2Num 0 1 2 3 0 0 = 8 * explicitZ 0 1 2 3 0 0 := by decide
 194theorem e_012301 : m2Num 0 1 2 3 0 1 = 8 * explicitZ 0 1 2 3 0 1 := by decide
 195theorem e_012302 : m2Num 0 1 2 3 0 2 = 8 * explicitZ 0 1 2 3 0 2 := by decide
 196theorem e_012303 : m2Num 0 1 2 3 0 3 = 8 * explicitZ 0 1 2 3 0 3 := by decide
 197theorem e_012310 : m2Num 0 1 2 3 1 0 = 8 * explicitZ 0 1 2 3 1 0 := by decide
 198theorem e_012311 : m2Num 0 1 2 3 1 1 = 8 * explicitZ 0 1 2 3 1 1 := by decide
 199theorem e_012312 : m2Num 0 1 2 3 1 2 = 8 * explicitZ 0 1 2 3 1 2 := by decide
 200theorem e_012313 : m2Num 0 1 2 3 1 3 = 8 * explicitZ 0 1 2 3 1 3 := by decide
 201theorem e_012320 : m2Num 0 1 2 3 2 0 = 8 * explicitZ 0 1 2 3 2 0 := by decide
 202theorem e_012321 : m2Num 0 1 2 3 2 1 = 8 * explicitZ 0 1 2 3 2 1 := by decide
 203theorem e_012322 : m2Num 0 1 2 3 2 2 = 8 * explicitZ 0 1 2 3 2 2 := by decide
 204theorem e_012323 : m2Num 0 1 2 3 2 3 = 8 * explicitZ 0 1 2 3 2 3 := by decide
 205theorem e_012330 : m2Num 0 1 2 3 3 0 = 8 * explicitZ 0 1 2 3 3 0 := by decide
 206theorem e_012331 : m2Num 0 1 2 3 3 1 = 8 * explicitZ 0 1 2 3 3 1 := by decide
 207theorem e_012332 : m2Num 0 1 2 3 3 2 = 8 * explicitZ 0 1 2 3 3 2 := by decide
 208theorem e_012333 : m2Num 0 1 2 3 3 3 = 8 * explicitZ 0 1 2 3 3 3 := by decide
 209theorem e_013000 : m2Num 0 1 3 0 0 0 = 8 * explicitZ 0 1 3 0 0 0 := by decide
 210theorem e_013001 : m2Num 0 1 3 0 0 1 = 8 * explicitZ 0 1 3 0 0 1 := by decide
 211theorem e_013002 : m2Num 0 1 3 0 0 2 = 8 * explicitZ 0 1 3 0 0 2 := by decide
 212theorem e_013003 : m2Num 0 1 3 0 0 3 = 8 * explicitZ 0 1 3 0 0 3 := by decide
 213theorem e_013010 : m2Num 0 1 3 0 1 0 = 8 * explicitZ 0 1 3 0 1 0 := by decide
 214theorem e_013011 : m2Num 0 1 3 0 1 1 = 8 * explicitZ 0 1 3 0 1 1 := by decide
 215theorem e_013012 : m2Num 0 1 3 0 1 2 = 8 * explicitZ 0 1 3 0 1 2 := by decide
 216theorem e_013013 : m2Num 0 1 3 0 1 3 = 8 * explicitZ 0 1 3 0 1 3 := by decide
 217theorem e_013020 : m2Num 0 1 3 0 2 0 = 8 * explicitZ 0 1 3 0 2 0 := by decide
 218theorem e_013021 : m2Num 0 1 3 0 2 1 = 8 * explicitZ 0 1 3 0 2 1 := by decide
 219theorem e_013022 : m2Num 0 1 3 0 2 2 = 8 * explicitZ 0 1 3 0 2 2 := by decide
 220theorem e_013023 : m2Num 0 1 3 0 2 3 = 8 * explicitZ 0 1 3 0 2 3 := by decide
 221theorem e_013030 : m2Num 0 1 3 0 3 0 = 8 * explicitZ 0 1 3 0 3 0 := by decide
 222theorem e_013031 : m2Num 0 1 3 0 3 1 = 8 * explicitZ 0 1 3 0 3 1 := by decide
 223theorem e_013032 : m2Num 0 1 3 0 3 2 = 8 * explicitZ 0 1 3 0 3 2 := by decide
 224theorem e_013033 : m2Num 0 1 3 0 3 3 = 8 * explicitZ 0 1 3 0 3 3 := by decide
 225theorem e_013100 : m2Num 0 1 3 1 0 0 = 8 * explicitZ 0 1 3 1 0 0 := by decide
 226theorem e_013101 : m2Num 0 1 3 1 0 1 = 8 * explicitZ 0 1 3 1 0 1 := by decide
 227theorem e_013102 : m2Num 0 1 3 1 0 2 = 8 * explicitZ 0 1 3 1 0 2 := by decide
 228theorem e_013103 : m2Num 0 1 3 1 0 3 = 8 * explicitZ 0 1 3 1 0 3 := by decide
 229theorem e_013110 : m2Num 0 1 3 1 1 0 = 8 * explicitZ 0 1 3 1 1 0 := by decide
 230theorem e_013111 : m2Num 0 1 3 1 1 1 = 8 * explicitZ 0 1 3 1 1 1 := by decide
 231theorem e_013112 : m2Num 0 1 3 1 1 2 = 8 * explicitZ 0 1 3 1 1 2 := by decide
 232theorem e_013113 : m2Num 0 1 3 1 1 3 = 8 * explicitZ 0 1 3 1 1 3 := by decide
 233theorem e_013120 : m2Num 0 1 3 1 2 0 = 8 * explicitZ 0 1 3 1 2 0 := by decide
 234theorem e_013121 : m2Num 0 1 3 1 2 1 = 8 * explicitZ 0 1 3 1 2 1 := by decide
 235theorem e_013122 : m2Num 0 1 3 1 2 2 = 8 * explicitZ 0 1 3 1 2 2 := by decide
 236theorem e_013123 : m2Num 0 1 3 1 2 3 = 8 * explicitZ 0 1 3 1 2 3 := by decide
 237theorem e_013130 : m2Num 0 1 3 1 3 0 = 8 * explicitZ 0 1 3 1 3 0 := by decide
 238theorem e_013131 : m2Num 0 1 3 1 3 1 = 8 * explicitZ 0 1 3 1 3 1 := by decide
 239theorem e_013132 : m2Num 0 1 3 1 3 2 = 8 * explicitZ 0 1 3 1 3 2 := by decide
 240theorem e_013133 : m2Num 0 1 3 1 3 3 = 8 * explicitZ 0 1 3 1 3 3 := by decide
 241theorem e_013200 : m2Num 0 1 3 2 0 0 = 8 * explicitZ 0 1 3 2 0 0 := by decide
 242theorem e_013201 : m2Num 0 1 3 2 0 1 = 8 * explicitZ 0 1 3 2 0 1 := by decide
 243theorem e_013202 : m2Num 0 1 3 2 0 2 = 8 * explicitZ 0 1 3 2 0 2 := by decide
 244theorem e_013203 : m2Num 0 1 3 2 0 3 = 8 * explicitZ 0 1 3 2 0 3 := by decide
 245theorem e_013210 : m2Num 0 1 3 2 1 0 = 8 * explicitZ 0 1 3 2 1 0 := by decide
 246theorem e_013211 : m2Num 0 1 3 2 1 1 = 8 * explicitZ 0 1 3 2 1 1 := by decide
 247theorem e_013212 : m2Num 0 1 3 2 1 2 = 8 * explicitZ 0 1 3 2 1 2 := by decide
 248theorem e_013213 : m2Num 0 1 3 2 1 3 = 8 * explicitZ 0 1 3 2 1 3 := by decide
 249theorem e_013220 : m2Num 0 1 3 2 2 0 = 8 * explicitZ 0 1 3 2 2 0 := by decide
 250theorem e_013221 : m2Num 0 1 3 2 2 1 = 8 * explicitZ 0 1 3 2 2 1 := by decide
 251theorem e_013222 : m2Num 0 1 3 2 2 2 = 8 * explicitZ 0 1 3 2 2 2 := by decide
 252theorem e_013223 : m2Num 0 1 3 2 2 3 = 8 * explicitZ 0 1 3 2 2 3 := by decide
 253theorem e_013230 : m2Num 0 1 3 2 3 0 = 8 * explicitZ 0 1 3 2 3 0 := by decide
 254theorem e_013231 : m2Num 0 1 3 2 3 1 = 8 * explicitZ 0 1 3 2 3 1 := by decide
 255theorem e_013232 : m2Num 0 1 3 2 3 2 = 8 * explicitZ 0 1 3 2 3 2 := by decide
 256theorem e_013233 : m2Num 0 1 3 2 3 3 = 8 * explicitZ 0 1 3 2 3 3 := by decide
 257theorem e_013300 : m2Num 0 1 3 3 0 0 = 8 * explicitZ 0 1 3 3 0 0 := by decide
 258theorem e_013301 : m2Num 0 1 3 3 0 1 = 8 * explicitZ 0 1 3 3 0 1 := by decide
 259theorem e_013302 : m2Num 0 1 3 3 0 2 = 8 * explicitZ 0 1 3 3 0 2 := by decide
 260theorem e_013303 : m2Num 0 1 3 3 0 3 = 8 * explicitZ 0 1 3 3 0 3 := by decide
 261theorem e_013310 : m2Num 0 1 3 3 1 0 = 8 * explicitZ 0 1 3 3 1 0 := by decide
 262theorem e_013311 : m2Num 0 1 3 3 1 1 = 8 * explicitZ 0 1 3 3 1 1 := by decide
 263theorem e_013312 : m2Num 0 1 3 3 1 2 = 8 * explicitZ 0 1 3 3 1 2 := by decide
 264theorem e_013313 : m2Num 0 1 3 3 1 3 = 8 * explicitZ 0 1 3 3 1 3 := by decide
 265theorem e_013320 : m2Num 0 1 3 3 2 0 = 8 * explicitZ 0 1 3 3 2 0 := by decide
 266theorem e_013321 : m2Num 0 1 3 3 2 1 = 8 * explicitZ 0 1 3 3 2 1 := by decide
 267theorem e_013322 : m2Num 0 1 3 3 2 2 = 8 * explicitZ 0 1 3 3 2 2 := by decide
 268theorem e_013323 : m2Num 0 1 3 3 2 3 = 8 * explicitZ 0 1 3 3 2 3 := by decide
 269theorem e_013330 : m2Num 0 1 3 3 3 0 = 8 * explicitZ 0 1 3 3 3 0 := by decide
 270theorem e_013331 : m2Num 0 1 3 3 3 1 = 8 * explicitZ 0 1 3 3 3 1 := by decide
 271theorem e_013332 : m2Num 0 1 3 3 3 2 = 8 * explicitZ 0 1 3 3 3 2 := by decide
 272theorem e_013333 : m2Num 0 1 3 3 3 3 = 8 * explicitZ 0 1 3 3 3 3 := by decide
 273
 274end M2NumChunk01
 275end ReggeExactMidpointM2TTIdentity4D
 276end Analysis
 277end Gravity
 278end IndisputableMonolith
 279
source mirrored from github.com/jonwashburn/shape-of-logic