show/hide visualization coordinates
a : (0.23729366062307689, 0.13289686326923078, 0.5418640136846153)
b : (-0.728626272776923, 0.3528971895692308, 0.6782404671846154)
c : (-0.37020087417692304, -0.5314875392307693, 0.9772302421846153)
d : (0.22017222832307692, -0.8141453146307693, 0.22121160208461532)
e : (0.953300354723077, -0.20030658393076928, -0.07157699591538469)
f : (0.503849367423077, 0.6737795505692308, -0.25587903541538465)
g : (-0.0781939863769231, 1.0773744167692307, 0.4500506514846154)
h : (-0.48453622347692304, 0.5232099778692307, -0.27643937451538464)
i : (-0.6742811884769231, -0.40874401943076927, 0.03252436688461535)
j : (-0.614016066976923, -1.3273669111307693, 0.4230369768846154)
k : (0.09429135482307693, -0.23261752163076926, -0.5825168563153846)
l : (0.913540454623077, 0.1543046814692307, -1.0057450732153845)
m : (0.02740719172307693, 0.6002052104692308, -1.1320009850153845)
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'], ['m', 'h', 'f'], ['b', 'g', 'a'], ['g', 'a', 'f'], ['d', 'a', 'e'], ['b', 'h', 'g'], ['h', 'g', 'f'], ['i', 'h', 'k'], ['m', 'k', 'l'], ['e', 'a', 'f'], ['j', 'd', 'c'], ['e', 'l', 'f'], ['m', 'h', 'k'], ['b', 'i', 'h'], ['b', 'i', 'c'], ['d', 'a', 'c'], ['k', 'e', 'l'], ['i', 'k', 'd'], ['k', 'd', 'e'], ['i', 'j', 'd'], ['i', 'j', 'c']]
Coordinate Data:
k : [283339693 / 500000000, 497309863 / 2000000000, -34041977 / 5000000000]
m : [4997952229 / 10000000000, 2703694159 / 2500000000, -5562925241 / 10000000000]
b : [-160148901 / 625000000, 8341696427 / 10000000000, 12539489281 / 10000000000]
f : [4881186993 / 5000000000, 11550520037 / 10000000000, 639658851 / 2000000000]
e : [14256883859 / 10000000000, 702414673 / 2500000000, 100826293 / 200000000]
c : [102187157 / 1000000000, -502150861 / 10000000000, 15529387031 / 10000000000]
a : [3548408459 / 5000000000, 1535423291 / 2500000000, 5587862373 / 5000000000]
h : [-121481923 / 10000000000, 1004482431 / 1000000000, 187043179 / 625000000]
g : [123185639 / 312500000, 15586468699 / 10000000000, 2564397781 / 2500000000]
l : [6929642429 / 5000000000, 3177885673 / 5000000000, -4300366123 / 10000000000]
j : [-708140179 / 5000000000, -423047229 / 500000000, 4993727189 / 5000000000]
d : [1385120519 / 2000000000, -665745723 / 2000000000, 796920063 / 1000000000]
i : [-2018931573 / 10000000000, 725284337 / 10000000000, 3041164139 / 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 = 1953124999854466511238285806828138826971845844251395811081 / 3906250011413661973324013510674413030132421875000000000000
Collision distance in [35355339 / 50000000, 70710679 / 100000000] ~ [0.70711, 0.70711]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [7077 / 10000, 7079 / 10000] ~ [0.7077, 0.7079]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 1995869513633196437271199 / 10000000000000000000000000000000000000000
rho in [70637623 / 5000000000000000, 120637623 / 5000000000000000] ~ [0.0, 0.0]
sigma_min ^ 2 / (16 * E ^ .5) in [50083929 / 9191300240, 50112241 / 9191300224] ~ [0.00545, 0.00545]
Success: rho < sigma_min ^ 2 / (16 * E ^ .5)
Checking inequality 4:
LHS NUM := sigma_min - [sigma_min ^ 2 - 16 * rho * |E| ^ .5 ] ^ .5 in [-19909 / 100000000, 20157 / 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 [-463 / 106875584, 20157 / 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