show/hide visualization coordinates
a : (-0.014894167646153866, 0.37687290850769234, 0.5594706116076923)
b : (0.4749870950538462, 0.3635523775076923, -0.31221678199230773)
c : (-0.5188285692461538, 0.4737834274076923, -0.29881749279230774)
d : (-0.8600556810461537, 0.9107488958076924, 0.5334236005076923)
e : (-0.7089790693461537, 0.24920278810769234, 1.2679524320076923)
f : (-0.28596487034615387, -0.5458983890923076, 0.8333570967076923)
g : (0.5616500497538461, -0.4048710293923077, 0.3218297462076923)
h : (1.3201510993538461, -0.1703196011923077, -0.2861684321923077)
i : (0.9015517906538462, 0.06070354570769232, -1.1644638973923078)
j : (-0.0835628813461538, -0.048780805092307644, -1.0319412226923077)
k : (-0.3071994048461539, -0.49437449189230764, -0.16508888699230773)
l : (-1.0301989737461539, -0.06159027239230763, 0.37339922140769227)
m : (0.5513435827538462, -0.7090293539923077, -0.6307359943923077)
show/hide computer existence proof
(see shape-existence, preprint)
Attempting to prove existence
Starting realization:
Abstract data:
mode: maximal_simplices
data: [['b', 'a', 'c'], ['k', 'l', 'f'], ['b', 'j', 'c'], ['b', 'g', 'a'], ['g', 'a', 'f'], ['d', 'a', 'e'], ['b', 'h', 'g'], ['m', 'i', 'h'], ['b', 'i', 'j'], ['m', 'i', 'j'], ['e', 'a', 'f'], ['m', 'h', 'g'], ['e', 'l', 'f'], ['k', 'l', 'c'], ['b', 'i', 'h'], ['m', 'k', 'g'], ['d', 'a', 'c'], ['d', 'l', 'c'], ['d', 'l', 'e'], ['j', 'k', 'c'], ['k', 'g', 'f'], ['m', 'j', 'k']]
Coordinate Data:
k : [3758306933 / 5000000000, 1971597887 / 2000000000, 4015952519 / 5000000000]
e : [11534410511 / 10000000000, 484443327 / 2000000000, -787313519 / 1250000000]
b : [-305251133 / 10000000000, 1278720741 / 10000000000, 2375795997 / 2500000000]
f : [7304268521 / 10000000000, 10373228407 / 10000000000, -1952554799 / 10000000000]
m : [-106881601 / 1000000000, 1500567257 / 1250000000, 793023507 / 625000000]
c : [963290551 / 1000000000, 88205121 / 5000000000, 1171148887 / 1250000000]
a : [2296780747 / 5000000000, 1145515431 / 10000000000, 196577513 / 2500000000]
h : [-1094611397 / 1250000000, 413590033 / 625000000, 924270049 / 1000000000]
g : [-29297017 / 250000000, 896295481 / 1000000000, 1581359353 / 5000000000]
l : [2949321911 / 2000000000, 138253681 / 250000000, 1323511977 / 5000000000]
j : [5280248631 / 10000000000, 5402052567 / 10000000000, 3340085679 / 2000000000]
d : [3261294157 / 2500000000, -2096622221 / 5000000000, 1046780163 / 10000000000]
i : [-4570898089 / 10000000000, 4307209059 / 10000000000, 9012827571 / 5000000000]
Desired square lengths:
default : 1
Checking inequality 1:
d = 3
|V| = 13
|E| = 33
Success: d|V| >= |E|
Checking self-intersection:
Square collision distance = 19565166460574266611982711403964001078640849897445694482327 / 35121270294106725555184435149147683335450000000000000000000
Collision distance in [18659357 / 25000000, 74637429 / 100000000] ~ [0.74637, 0.74637]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [383 / 500, 3831 / 5000] ~ [0.766, 0.7662]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 26303470703256439770961 / 10000000000000000000000000000000000000000
rho in [162183447 / 100000000000000000, 1162183447 / 100000000000000000] ~ [0.0, 0.0]
sigma_min ^ 2 / (16 * E ^ .5) in [733445 / 114891253, 14676561 / 2297825056] ~ [0.00638, 0.00639]
Success: rho < sigma_min ^ 2 / (16 * E ^ .5)
Checking inequality 4:
LHS NUM := sigma_min - [sigma_min ^ 2 - 16 * rho * |E| ^ .5 ] ^ .5 in [-19991 / 100000000, 2007 / 10000000] ~ [-0.0002, 0.0002]
LHS DEN := 8 * |E| ^ .5 in [71807033 / 1562500, 114891253 / 2500000] ~ [45.9565, 45.9565]
LHS := (LHS NUM) / (LHS DEN) in [-19991 / 4595650112, 10035 / 2297825056] ~ [-0.0, 0.0]
CD / |V| ^ .5 in [18659357 / 90138782, 74637429 / 360555127] ~ [0.20701, 0.20701]
Success: LHS < CD / |V| ^ .5
Success: existence proven