13 vertices

bcdefg aghijc abjd acje adjif aeikg afklhb bglmki bhkfej biedc fihmlg gkmh hlk

show/hide visualization coordinates

a : (0.5764029820692309, -0.16197219506580812, 0.48669409990769225)
b : (-0.1822136023307691, 0.48954707413419185, 0.4818444246076922)
c : (0.23250438896923087, 0.21144902933419188, 1.3482568352076922)
d : (0.41915805486923086, -0.7675905161658081, 1.2667585087076922)
e : (0.10861761736923087, -1.0359266628658081, 0.35485920030769225)
f : (0.5180071461692308, -0.565058243765808, -0.4266029839923077)
g : (0.4254351668692309, 0.42375321478969785, -0.3096315012923077)
h : (-0.5442770870307692, 0.6305657373341919, -0.43958043369230776)
i : (-0.38841985253076916, -0.2970644298658081, -0.1001532763923077)
j : (-0.42774004113076913, -0.3873989740658081, 0.8949816856076922)
k : (-0.09487977093076916, -0.04627338916580814, -1.0226163238923078)
l : (0.12536684206923088, 0.9241166030341919, -1.1217863390923077)
m : (-0.7679618444307692, 0.5818527523341919, -1.4130238959923078)
			
show/hide computer existence proof (see shape-existence, preprint)

Attempting to prove existence

Starting realization:
	Abstract data:	
		mode: maximal_simplices
		data: [['b', 'a', 'c'], ['b', 'j', 'c'], ['b', 'g', 'a'], ['g', 'a', 'f'], ['d', 'a', 'e'], ['b', 'h', 'g'], ['l', 'k', 'g'], ['i', 'h', 'k'], ['b', 'i', 'j'], ['m', 'k', 'l'], ['e', 'a', 'f'], ['j', 'd', 'c'], ['m', 'h', 'k'], ['b', 'i', 'h'], ['d', 'a', 'c'], ['j', 'd', 'e'], ['m', 'h', 'l'], ['l', 'h', 'g'], ['i', 'j', 'e'], ['k', 'g', 'f'], ['i', 'e', 'f'], ['i', 'k', 'f']]
	Coordinate Data:
		k : [5728104533 / 10000000000, 940060553 / 2000000000, 7508292783 / 5000000000]
		e : [73862613 / 200000000, 7298417751 / 5000000000, 310457581 / 2500000000]
		b : [6601442847 / 10000000000, -164475467 / 2500000000, -28021919 / 10000000000]
		f : [-200382319 / 5000000000, 9888151311 / 10000000000, 9056452167 / 10000000000]
		m : [3114731317 / 2500000000, -31619173 / 200000000, 18920661287 / 10000000000]
		c : [1227131467 / 5000000000, 106153929 / 500000000, -347685841 / 400000000]
		a : [-984722997 / 10000000000, 732161353 / 1250000000, -4782417 / 625000000]
		h : [5111038847 / 5000000000, -4136177 / 20000000, 1148278333 / 1250000000]
		g : [104991031 / 2000000000, 1836272247 / 500000000000000, 394336867 / 500000000]
		l : [3525638403 / 10000000000, -5003597157 / 10000000000, 8004142859 / 5000000000]
		j : [1811341447 / 2000000000, 4055779307 / 5000000000, -4159394529 / 10000000000]
		d : [23509051 / 400000000, 2382694807 / 2000000000, -196929069 / 250000000]
		i : [8663505349 / 10000000000, 1802053293 / 2500000000, 5791955091 / 10000000000]

Desired square lengths:
	default : 1

Checking inequality 1:
	 d  = 3
	|V| = 13
	|E| = 33
	Success: d|V| >= |E|

Checking self-intersection:
	Square collision distance = 31249999987053570071499114416028512419506949508146288381329 / 62500000019335042991191800941112906297912500000000000000000
	Collision distance in [35355339 / 50000000, 70710679 / 100000000] ~ [0.70711, 0.70711]
	Success: starting realization non-self-intersecting

Checking inequality 2:
	sigma_min in [7553 / 10000, 1511 / 2000] ~ [0.7553, 0.7555]
	Success: sigma_min > 0

Checking inequality 3:
	rho_squared = 55055994942149041618259851027041191666243 / 31250000000000000000000000000000000000000000000000000000000
	rho in [66366253 / 50000000000000000, 566366253 / 50000000000000000] ~ [0.0, 0.0]
	sigma_min ^ 2 / (16 * E ^ .5) in [57047809 / 9191300240, 57078025 / 9191300224] ~ [0.00621, 0.00621]
	Success: rho < sigma_min ^ 2 / (16 * E ^ .5)

Checking inequality 4:
	LHS NUM := sigma_min - [sigma_min ^ 2 - 16 * rho * |E| ^ .5 ] ^ .5 in [-2499 / 12500000, 20069 / 100000000] ~ [-0.0002, 0.0002]
	LHS DEN := 8 * |E| ^ .5 in [71807033 / 1562500, 114891253 / 2500000] ~ [45.9565, 45.9565]
	LHS     := (LHS NUM) / (LHS DEN) in [-2499 / 574456264, 20069 / 4595650112] ~ [-0.0, 0.0]
	CD / |V| ^ .5 in [35355339 / 180277564, 70710679 / 360555127] ~ [0.19612, 0.19612]
	Success: LHS < CD / |V| ^ .5

Success: existence proven