show/hide visualization coordinates
a : (-0.009766258123305172, 0.8598227994719365, 0.7498048301767075)
b : (0.7938424798934971, 0.28753131764115003, 0.9131922715758705)
c : (0.8965039839426099, 1.277418123904816, 0.815290655800166)
d : (0.37339356018246955, 1.3485301799959313, -0.0340023207585598)
e : (-0.4116367876072001, 0.7416583057363287, -0.15823549379163993)
f : (-0.8290323533616423, 0.2980492530296174, 0.6348546335237765)
g : (-0.101713409190616, 0.0008199408181340795, 1.253451343353559)
h : (0.3950039053216441, -0.576194874094258, 0.6051259521838576)
i : (1.2872968169283687, -0.2859913763684485, 0.2593004328766497)
j : (1.1075981905717267, 0.674337767789943, 0.04604861326999998)
k : (0.4267338861469138, 0.588136410342499, -0.6812705222780301)
l : (-0.4271544864044279, 0.1525759275002591, -0.9661594708314197)
m : (-1.1573532535569688, 0.08776102135942032, -0.28600596728176986)
n : (-1.5359633691850583, -0.3967576880830955, 0.5025978626253917)
o : (-0.5956144909780484, -0.6719636529444648, 0.7026120225229866)
p : (-0.09904805986139464, -1.2482208471785028, 0.053497683148494235)
q : (0.6159743287578694, -0.6873254383062359, -0.3638023576844952)
r : (1.2464438118125214, 0.015483829733405119, -0.6932979778289577)
s : (0.4504347134078484, -0.2392828589885222, -1.2423548506341748)
t : (-0.2533526325750083, -0.8239325596937233, -0.8387856507443351)
u : (-1.1682120607315158, -0.5074377420891489, -1.0895111124401815)
v : (-1.0043785153902833, -0.8950178395770405, -0.182350576783896)
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'], ['i', 'j', 'r'], ['k', 'e', 'l'], ['m', 'u', 'l'], ['h', 'q', 'p'], ['d', 'c', 'a'], ['o', 'p', 'v'], ['h', 'q', 'i'], ['v', 'n', 'm'], ['h', 'o', 'g'], ['q', 't', 's'], ['s', 't', 'l'], ['h', 'o', 'p'], ['q', 'i', 'r'], ['o', 'n', 'f'], ['h', 'g', 'b'], ['k', 'e', 'd'], ['v', 't', 'p'], ['n', 'm', 'f'], ['k', 'j', 'd'], ['g', 'a', 'b'], ['g', 'a', 'f'], ['k', 's', 'l'], ['k', 's', 'r'], ['e', 'a', 'f'], ['e', 'm', 'l'], ['c', 'a', 'b'], ['k', 'j', 'r'], ['g', 'o', 'f'], ['q', 't', 'p'], ['j', 'c', 'b'], ['j', 'd', 'c'], ['q', 's', 'r'], ['v', 'o', 'n'], ['t', 'u', 'l'], ['e', 'm', 'f'], ['i', 'j', 'b'], ['v', 'm', 'u'], ['v', 't', 'u']]
Coordinate Data:
j : [-62843610549141156439 / 100000000000000000000, -8535495141625499751 / 50000000000000000000, 53426153977096684459 / 100000000000000000000]
p : [3613813405885686929 / 6250000000000000000, 21898108901699198561 / 12500000000000000000, 52681246989247260083 / 100000000000000000000]
a : [6111604290045254979 / 12500000000000000000, -35619493451450353417 / 100000000000000000000, -16949467713574078313 / 100000000000000000000]
i : [-20203368296201337667 / 25000000000000000000, 19740481033147040331 / 25000000000000000000, 32100972016431706661 / 100000000000000000000]
c : [-41734189886229466701 / 100000000000000000000, -483618911842114257 / 625000000000000000, -23498050275919926513 / 100000000000000000000]
g : [58087549427093120283 / 100000000000000000000, 6285099051741237369 / 12500000000000000000, -33657059515629615977 / 50000000000000000000]
r : [-7672817267322060539 / 10000000000000000000, 48814403522402795357 / 100000000000000000000, 127360813086992463697 / 100000000000000000000]
l : [90631657148474310421 / 100000000000000000000, 7021038749143478957 / 20000000000000000000, 154646962387238650047 / 100000000000000000000]
u : [5148044205661971683 / 3125000000000000000, 2022131214093163967 / 2000000000000000000, 33396425309622965429 / 20000000000000000000]
d : [10576852489784566203 / 100000000000000000000, -675921852030798707 / 800000000000000000, 61431247379952657823 / 100000000000000000000]
m : [16365153386372840663 / 10000000000000000000, 41586684359801272173 / 100000000000000000000, 86631612032273666869 / 100000000000000000000]
o : [107477657605836363667 / 100000000000000000000, 117559151790189776009 / 100000000000000000000, -12230186948201976181 / 100000000000000000000]
q : [-13681224367755422801 / 100000000000000000000, 14886916290795863133 / 12500000000000000000, 94411251072546200443 / 100000000000000000000]
f : [65409721922097870799 / 50000000000000000000, 20557861192781567687 / 100000000000000000000, -2727224024140486841 / 50000000000000000000]
t : [73251471765532346027 / 100000000000000000000, 33189010616278908043 / 25000000000000000000, 70954790189265092269 / 50000000000000000000]
e : [4453994363437576853 / 5000000000000000000, -5950761019472392697 / 25000000000000000000, 73854564683260667131 / 100000000000000000000]
k : [655352486667517341 / 12500000000000000000, -264089204328331061 / 3125000000000000000, 126158067531899683037 / 100000000000000000000]
n : [201512545426537368523 / 100000000000000000000, 90038555304052860637 / 100000000000000000000, 3885614520778753021 / 50000000000000000000]
s : [1436368583623339733 / 50000000000000000000, 74291072394595525721 / 100000000000000000000, 182266500367514183497 / 100000000000000000000]
h : [336632719034684613 / 4000000000000000000, 107982273905169101309 / 100000000000000000000, -99263196571563143 / 4000000000000000000]
v : [148354060047059855569 / 100000000000000000000, 139864570453447348357 / 100000000000000000000, 76266072982486275057 / 100000000000000000000]
b : [-7867009870329547379 / 25000000000000000000, 21609654731628304889 / 100000000000000000000, -16644105926745183517 / 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 = 8518046725235688874487942752017121301616080788842321647858052497438476084205575960118819111293041614605265800850772729 / 13348511928327772202116564716691587478982100052353604880779454630823180223941885781250000000000000000000000000000000000
Collision distance in [99853569663693095336701891127 / 125000000000000000000000000000, 798828557309544762693615129017 / 1000000000000000000000000000000] ~ [0.79883, 0.79883]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [121 / 250, 2421 / 5000] ~ [0.484, 0.4842]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 705122808612688886800377379570262008666491 / 12500000000000000000000000000000000000000000000000000000000000000000000000000000
rho in [2375075255418554331076939140713 / 10000000000000000000000000000000000000000000000000, 2375075255428554331076939140713 / 10000000000000000000000000000000000000000000000000] ~ [0.0, 0.0]
sigma_min ^ 2 / (16 * E ^ .5) in [2928200000000000000000000000 / 1549193338482966754071706159913, 407030625000000000000000000 / 215165741455967604732181411099] ~ [0.00189, 0.00189]
Success: rho < sigma_min ^ 2 / (16 * E ^ .5)
Checking inequality 4:
LHS NUM := sigma_min - [sigma_min ^ 2 - 16 * rho * |E| ^ .5 ] ^ .5 in [-49999999999992400969095229 / 250000000000000000000000000000, 100000000000015204342000437 / 500000000000000000000000000000] ~ [-0.0002, 0.0002]
LHS DEN := 8 * |E| ^ .5 in [1936491673103708442589632699891 / 31250000000000000000000000000, 1549193338482966754071706159913 / 25000000000000000000000000000] ~ [61.96773, 61.96773]
LHS := (LHS NUM) / (LHS DEN) in [-49999999999992400969095229 / 15491933384829667540717061599128, 358422939068154854272403 / 111053285912757473410158147664] ~ [-0.0, 0.0]
CD / |V| ^ .5 in [798828557309544762693615129016 / 4690415759823429554565630113545, 798828557309544762693615129017 / 4690415759823429554565630113544] ~ [0.17031, 0.17031]
Success: LHS < CD / |V| ^ .5
Success: existence proven