show/hide visualization coordinates
a : (-0.31077779030727315, 0.5226909701722492, 0.9731978344642078)
b : (-0.2672015203952738, -0.46903722439590584, 0.8524654991138787)
c : (0.3445028022316522, -0.017025907934386186, 1.5016985785778394)
d : (0.6671048191207856, 0.5894505943843097, 0.7749839228605184)
e : (0.06188741321821489, 1.3588902181547393, 0.570840451339672)
f : (-0.8296452135770838, 1.015910651813039, 0.27497799608126333)
g : (-1.0219404724374066, 0.05070237219667412, 0.452165778898981)
h : (-0.8460314149982722, -0.88689280584846, 0.15221364002114496)
i : (0.1408581324528319, -1.048196738636097, 0.14673072118200647)
j : (0.7107781668678858, -0.4023294681404263, 0.6547136178181193)
k : (0.9654083166697545, 0.20434911565367742, -0.09834984748706899)
l : (0.869785462131998, 1.194393122386326, 0.004941654693964348)
m : (-0.035277109839331855, 0.9272391864924874, -0.3259518558998098)
n : (-0.8455080130133241, 0.36216498254583984, -0.4815700668390164)
o : (-1.5406898130565647, -0.3359719165708755, -0.3103183953717368)
p : (-0.6956290312265472, -0.5781873785758704, -0.7869775450568618)
q : (-0.44476644693886236, -1.5087527283004634, -0.520301536206328)
r : (0.2597841258823975, -0.8702931315591054, -0.8301044310702997)
s : (1.0384710160638626, -0.786903641562702, -0.20825805131267916)
t : (0.976632727246405, -0.19772252495284487, -1.0138892559382762)
u : (0.7711980000787657, 0.7739430166479755, -0.8970019249774651)
v : (0.031055843825387452, 0.10157923602982216, -0.8862067848920531)
show/hide computer existence proof
(see shape-existence, preprint)
Attempting to prove existence
Starting realization:
Abstract data:
mode: maximal_simplices
data: [['e', 'd', 'a'], ['h', 'i', 'b'], ['k', 't', 's'], ['v', 't', 'u'], ['v', 't', 'r'], ['m', 'u', 'l'], ['h', 'q', 'p'], ['s', 'i', 'r'], ['d', 'c', 'a'], ['v', 'n', 'p'], ['q', 'r', 'p'], ['h', 'q', 'i'], ['v', 'n', 'm'], ['h', 'o', 'g'], ['h', 'o', 'p'], ['q', 'i', 'r'], ['s', 'j', 'k'], ['h', 'g', 'b'], ['n', 'm', 'f'], ['k', 'j', 'd'], ['g', 'a', 'b'], ['g', 'a', 'f'], ['s', 't', 'r'], ['e', 'a', 'f'], ['o', 'n', 'g'], ['s', 'i', 'j'], ['e', 'm', 'l'], ['c', 'a', 'b'], ['k', 't', 'u'], ['j', 'c', 'b'], ['j', 'd', 'c'], ['g', 'n', 'f'], ['k', 'd', 'l'], ['o', 'n', 'p'], ['e', 'm', 'f'], ['i', 'j', 'b'], ['k', 'u', 'l'], ['v', 'm', 'u'], ['v', 'r', 'p'], ['e', 'd', 'l']]
Coordinate Data:
j : [-12018655358105184703 / 50000000000000000000, 10855434792653421789 / 12500000000000000000, -3717092894230932461 / 25000000000000000000]
p : [11660340909323293259 / 10000000000000000000, 652682933654823653 / 625000000000000000, 32325186177643594679 / 25000000000000000000]
a : [1220598203145398753 / 1562500000000000000, -88415085781877647 / 1562500000000000000, -46716793241532586087 / 100000000000000000000]
i : [8238673181323754029 / 25000000000000000000, 37857551347698617067 / 25000000000000000000, 2245619880417971853 / 6250000000000000000]
c : [6295112873706491533 / 50000000000000000000, 6039140290077920157 / 12500000000000000000, -49783433826447869409 / 50000000000000000000]
g : [14923455321431887321 / 10000000000000000000, 8308058861503467153 / 20000000000000000000, 1077282462998019893 / 20000000000000000000]
r : [10531046691169227277 / 50000000000000000000, 133639844683095289353 / 100000000000000000000, 133613433311918169571 / 100000000000000000000]
l : [-19969020121310797517 / 50000000000000000000, -72828780711447848713 / 100000000000000000000, 1565900772984117563 / 3125000000000000000]
u : [-15039647018649181849 / 50000000000000000000, -30783770137612797621 / 100000000000000000000, 140303182702634715311 / 100000000000000000000]
d : [-4917493985375088419 / 25000000000000000000, -12334527911246218883 / 100000000000000000000, -13447701040581823393 / 50000000000000000000]
m : [25284108477255696267 / 50000000000000000000, -46113387122063990199 / 100000000000000000000, 83198175794869175031 / 100000000000000000000]
o : [100554743638117342457 / 50000000000000000000, 2506491349508509067 / 3125000000000000000, 20408707435515470307 / 25000000000000000000]
q : [11439643833058055177 / 12500000000000000000, 197485804357231092401 / 100000000000000000000, 12829142978190125383 / 12500000000000000000]
f : [1625062841603582297 / 1250000000000000000, -27490266827059574059 / 50000000000000000000, 5776297649190466061 / 25000000000000000000]
t : [-2531138337703115151 / 5000000000000000000, 33191392011234614639 / 50000000000000000000, 6079676631948632859 / 4000000000000000000]
e : [40851764648756716483 / 100000000000000000000, -44639245144144591911 / 50000000000000000000, -6481054929079000479 / 100000000000000000000]
k : [-12375081424099311657 / 25000000000000000000, 13087809980908502693 / 50000000000000000000, 12087594990719020489 / 20000000000000000000]
n : [65795653635955308077 / 50000000000000000000, 5197016636300381643 / 50000000000000000000, 98759996888789836463 / 100000000000000000000]
s : [-710082445447600541 / 1250000000000000000, 125300895683454942987 / 100000000000000000000, 35714397668078057509 / 50000000000000000000]
h : [65821823735202707077 / 50000000000000000000, 67649906056015370049 / 50000000000000000000, 17690813101386851881 / 50000000000000000000]
v : [21967460794019731573 / 50000000000000000000, 18226303962101263809 / 50000000000000000000, 27844733738818699311 / 20000000000000000000]
b : [73760658010105588339 / 100000000000000000000, 93514253966775327751 / 100000000000000000000, -17321779853249835321 / 50000000000000000000]
Desired square lengths:
default : 1
Checking inequality 1:
d = 3
|V| = 22
|E| = 60
Success: d|V| >= |E|
Checking self-intersection:
Square collision distance = 35155961799393988114064510007298460562604189137626800185512463811754561746079925377847380083902011113192892148589936609 / 58526356401183890750055514266938247095554959870578799064703542055933009832325502500000000000000000000000000000000000000
Collision distance in [775039341473991312721458422297 / 1000000000000000000000000000000, 387519670736995656360729211149 / 500000000000000000000000000000] ~ [0.77504, 0.77504]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [3947 / 10000, 3949 / 10000] ~ [0.3947, 0.3949]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 953800320177651612634147862713297502925459 / 20000000000000000000000000000000000000000000000000000000000000000000000000000000
rho in [1091902193523790168135658597471 / 5000000000000000000000000000000000000000000000000, 1091902193528790168135658597471 / 5000000000000000000000000000000000000000000000000] ~ [0.0, 0.0]
sigma_min ^ 2 / (16 * E ^ .5) in [1947351125000000000000000000 / 1549193338482966754071706159913, 221514218750000000000000000 / 176044697554882585689966609081] ~ [0.00126, 0.00126]
Success: rho < sigma_min ^ 2 / (16 * E ^ .5)
Checking inequality 4:
LHS NUM := sigma_min - [sigma_min ^ 2 - 16 * rho * |E| ^ .5 ] ^ .5 in [-199999999999965731727435159 / 1000000000000000000000000000000, 50000000000008571409194273 / 250000000000000000000000000000] ~ [-0.0002, 0.0002]
LHS DEN := 8 * |E| ^ .5 in [1936491673103708442589632699891 / 31250000000000000000000000000, 1549193338482966754071706159913 / 25000000000000000000000000000] ~ [61.96773, 61.96773]
LHS := (LHS NUM) / (LHS DEN) in [-66666666666655243909145053 / 20655911179772890054289415465504, 50000000000008571409194273 / 15491933384829667540717061599128] ~ [-0.0, 0.0]
CD / |V| ^ .5 in [775039341473991312721458422297 / 4690415759823429554565630113545, 129173223578998552120243070383 / 781735959970571592427605018924] ~ [0.16524, 0.16524]
Success: LHS < CD / |V| ^ .5
Success: existence proven