show/hide visualization coordinates
a : (-0.036485189338461566, 0.17620987433846164, -0.3317931835923076)
b : (-0.9546369677384616, -0.20961774946153833, -0.24160459979230764)
c : (-0.7330735796384615, 0.6614915938384617, 0.19666303960769238)
d : (0.19794358116153843, 0.5801284503384616, 0.5524539214076923)
e : (0.9146575207615384, 0.4027038081384616, -0.12196561349230761)
f : (0.6930938541615385, -0.46840548256153836, -0.5602332552923076)
g : (-0.1527181813384616, -0.7985496787615383, -0.1411786357923076)
h : (-0.42854951853846157, -0.1972637635615383, 0.6087361727076923)
i : (-1.3986915906384614, 0.045118752938461626, 0.6174207047076924)
j : (-1.6290513609384616, 0.5285923558384616, -0.2270838825923076)
k : (0.5417939222615384, -0.3496630389615384, 0.42109675330769236)
l : (1.4734066859615385, -0.4059644721615383, 0.062030901707692376)
m : (1.5123108238615384, 0.03521935003846166, -0.8345423228923077)
show/hide computer existence proof
(see shape-existence, preprint)
Attempting to prove existence
Starting realization:
Abstract data:
mode: maximal_simplices
data: [['b', 'a', 'c'], ['m', 'l', 'f'], ['i', 'h', 'c'], ['k', 'l', 'f'], ['b', 'j', 'c'], ['b', 'g', 'a'], ['g', 'a', 'f'], ['d', 'a', 'e'], ['b', 'h', 'g'], ['h', 'd', 'k'], ['b', 'i', 'j'], ['m', 'e', 'l'], ['e', 'a', 'f'], ['h', 'd', 'c'], ['b', 'i', 'h'], ['d', 'a', 'c'], ['m', 'e', 'f'], ['k', 'g', 'h'], ['k', 'e', 'l'], ['k', 'g', 'f'], ['k', 'd', 'e'], ['i', 'j', 'c']]
Coordinate Data:
k : [501983613 / 5000000000, 8755783269 / 10000000000, 12948777 / 1250000000]
m : [-870120179 / 1000000000, 4906959379 / 10000000000, 6329990489 / 5000000000]
b : [7984138063 / 5000000000, 3677665187 / 5000000000, 6730603747 / 10000000000]
f : [-509032093 / 10000000000, 1988641541 / 2000000000, 4958445151 / 5000000000]
e : [-2724668759 / 10000000000, 616057399 / 5000000000, 1383553471 / 2500000000]
c : [2750528449 / 2000000000, -1355763059 / 10000000000, 2347927353 / 10000000000]
a : [3393379171 / 5000000000, 437131767 / 1250000000, 1526497917 / 2000000000]
h : [5353700817 / 5000000000, 1446358103 / 2000000000, -886401989 / 5000000000]
g : [3974544131 / 5000000000, 13244649667 / 10000000000, 5726344107 / 10000000000]
l : [-8312160411 / 10000000000, 9318797601 / 10000000000, 923562183 / 2500000000]
j : [11356210029 / 5000000000, -26770679 / 10000000000, 263415863 / 400000000]
d : [4442470637 / 10000000000, -67766453 / 1250000000, -241996293 / 2000000000]
i : [4081764471 / 2000000000, 96159307 / 200000000, -929824649 / 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 = 499999954910174235893023025691480749729910012154352987329561 / 1000000693120793524836455161689989694709000000000000000000000
Collision distance in [1414213 / 2000000, 70710651 / 100000000] ~ [0.70711, 0.70711]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [6347 / 10000, 6349 / 10000] ~ [0.6347, 0.6349]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 23185639554204513248886439919 / 10000000000000000000000000000000000000000
rho in [76134157 / 50000000000000, 76634157 / 50000000000000] ~ [0.0, 0.0]
sigma_min ^ 2 / (16 * E ^ .5) in [40284409 / 9191300240, 40309801 / 9191300224] ~ [0.00438, 0.00439]
Success: rho < sigma_min ^ 2 / (16 * E ^ .5)
Checking inequality 4:
LHS NUM := sigma_min - [sigma_min ^ 2 - 16 * rho * |E| ^ .5 ] ^ .5 in [-4489 / 50000000, 31099 / 100000000] ~ [-9e-05, 0.00031]
LHS DEN := 8 * |E| ^ .5 in [71807033 / 1562500, 114891253 / 2500000] ~ [45.9565, 45.9565]
LHS := (LHS NUM) / (LHS DEN) in [-4489 / 2297825056, 31099 / 4595650112] ~ [-0.0, 1e-05]
CD / |V| ^ .5 in [35355325 / 180277564, 70710651 / 360555127] ~ [0.19612, 0.19612]
Success: LHS < CD / |V| ^ .5
Success: existence proven