show/hide visualization coordinates
a : (0.5710534389800507, 0.652593570038178, 0.03964233103349096)
b : (0.38621481425426885, 0.6562255055256793, -0.9431198435815562)
c : (-0.3720831402118491, 0.6277539808214373, -0.2918337432128187)
d : (-0.186855088131075, 0.6119259100277088, 0.6907343413987825)
e : (0.4939989960754654, -0.12018872759304089, 0.6696186268545942)
f : (1.143121777841628, -0.15727621768951328, -0.09016037540231397)
g : (1.3295019669584245, 0.675349704406306, -0.6116932113377647)
h : (1.1278935694814831, 0.3248277440667131, -1.5262906142350552)
i : (0.19002712193394222, 0.017236612447631083, -1.686896412118718)
j : (-0.551502266821045, 0.5445534895183092, -1.27208190324869)
k : (-1.1403004387654947, 0.07474539986720341, -0.6143607833101157)
l : (-1.0869762571353787, 0.34399141953691936, 0.34723326437606533)
m : (-0.962540271357468, 0.546889090472904, 1.3184944138988044)
n : (-0.22171114476330944, -0.1229768375583441, 1.3680105087829013)
o : (-0.10549826519525718, -0.9144942217672359, 0.7680148445338879)
p : (0.30837851753760537, -0.7071909476998061, -0.11840004775731167)
q : (0.7405915673043811, -0.4103100596711017, -0.9699008510068392)
r : (1.7158464354702412, -0.19780707262804642, -0.9089055838415081)
s : (-0.24674997217636607, -0.3084248952437437, -0.8483438780048824)
t : (-0.6580432505733815, -0.5060279386719134, 0.04148244008947477)
u : (-0.931519371616206, -0.3996713245747592, 0.9974631312423659)
v : (-1.011984736915457, -0.2056711047539902, 1.9751590142738693)
w : (-0.5308640021752014, -1.0260530788774966, 1.6661343305733354)
show/hide computer existence proof
(see shape-existence, preprint)
Attempting to prove existence
Starting realization:
Abstract data:
mode: maximal_simplices
data: [['c', 'd', 'a'], ['b', 'g', 'h'], ['d', 'm', 'n'], ['r', 'g', 'f'], ['j', 'c', 'k'], ['w', 'o', 'n'], ['r', 'h', 'q'], ['w', 'v', 'n'], ['e', 'a', 'f'], ['d', 'e', 'n'], ['i', 'h', 'q'], ['w', 'u', 'v'], ['t', 'l', 'k'], ['j', 'i', 's'], ['w', 'o', 'u'], ['u', 't', 'o'], ['p', 'q', 'f'], ['d', 'l', 'm'], ['f', 'e', 'p'], ['b', 'a', 'c'], ['j', 'b', 'i'], ['j', 'b', 'c'], ['r', 'q', 'f'], ['d', 'e', 'a'], ['c', 'l', 'k'], ['i', 's', 'q'], ['g', 'a', 'f'], ['u', 'l', 'm'], ['t', 'p', 's'], ['e', 'o', 'n'], ['r', 'g', 'h'], ['u', 'v', 'm'], ['v', 'm', 'n'], ['e', 'o', 'p'], ['p', 'q', 's'], ['u', 't', 'l'], ['t', 'o', 'p'], ['t', 'k', 's'], ['c', 'l', 'd'], ['j', 'k', 's'], ['b', 'g', 'a'], ['b', 'h', 'i']]
Coordinate Data:
n : [762244702213457877 / 1000000000000000000, 32839343305866561621 / 50000000000000000000, -19180143650924346963 / 20000000000000000000]
t : [119857680802352998673 / 100000000000000000000, 10398379672309006969 / 10000000000000000000, 1837604430736045853 / 5000000000000000000]
a : [-3051988152990227897 / 100000000000000000000, -5939177073959540467 / 50000000000000000000, 36936099520319299443 / 100000000000000000000]
j : [109203582427119335547 / 100000000000000000000, -134293261991525423 / 12500000000000000000, 42027130737134352129 / 25000000000000000000]
q : [-312590640397238569 / 1562500000000000000, 47206004411504442747 / 50000000000000000000, 6894520886217615823 / 5000000000000000000]
l : [162750981458552715063 / 100000000000000000000, 9490930451103391423 / 50000000000000000000, 1544251546515465407 / 25000000000000000000]
f : [-60258822039147959273 / 100000000000000000000, 4319289039053128179 / 6250000000000000000, 12479092540974948287 / 25000000000000000000]
o : [64603182264540558999 / 100000000000000000000, 144830425032622308877 / 100000000000000000000, -35901151829720392209 / 100000000000000000000]
b : [771593715979397799 / 5000000000000000000, -12241547696669208979 / 100000000000000000000, 67606158490912001997 / 50000000000000000000]
v : [1242014635492484407 / 800000000000000000, 73948113331297732767 / 100000000000000000000, -156615568803718544327 / 100000000000000000000]
s : [39364176481325722599 / 50000000000000000000, 84223492380273093651 / 100000000000000000000, 25146944084831324787 / 20000000000000000000]
c : [91261669766199747649 / 100000000000000000000, -939439522624500939 / 10000000000000000000, 70083706944950263231 / 100000000000000000000]
i : [35050643551620620561 / 100000000000000000000, 51657341611135614849 / 100000000000000000000, 209589973835540193207 / 100000000000000000000]
k : [42020849905391078049 / 25000000000000000000, 45906462869178379877 / 100000000000000000000, 102336410954679960807 / 100000000000000000000]
e : [465345613746830411 / 10000000000000000000, 16349968903800702993 / 25000000000000000000, -3257691257723877913 / 12500000000000000000]
h : [-58736001203133484473 / 100000000000000000000, 20898228449227410461 / 100000000000000000000, 96764697023586951633 / 50000000000000000000]
r : [-2938282195050231729 / 2500000000000000000, 14632342023740672363 / 20000000000000000000, 131790891007819209273 / 100000000000000000000]
d : [36369432279061169181 / 50000000000000000000, -3905794073436078073 / 50000000000000000000, -28173101516209859983 / 100000000000000000000]
g : [-78896840950827599773 / 100000000000000000000, -14153967584731885733 / 100000000000000000000, 25517413439361216027 / 25000000000000000000]
w : [26784938990633741709 / 25000000000000000000, 19498288842956045193 / 12500000000000000000, -6285655021683257601 / 5000000000000000000]
p : [23215503991254304287 / 100000000000000000000, 24820019525175863647 / 20000000000000000000, 26370168699699782353 / 50000000000000000000]
m : [3006147657615233011 / 2000000000000000000, -1307906191391682537 / 100000000000000000000, -90949108766212045739 / 100000000000000000000]
u : [36801323226658862987 / 25000000000000000000, 93348135313374638999 / 100000000000000000000, -58845980500568194127 / 100000000000000000000]
Desired square lengths:
default : 1
Checking inequality 1:
d = 3
|V| = 23
|E| = 63
Success: d|V| >= |E|
Checking self-intersection:
Square collision distance = 25593681687107260892497664323869682060167614431145038141198638297716008392176389307667690123015399770536881248434811601 / 61254729858115098360516873417210784632795717276596819650300297821707347148984635625000000000000000000000000000000000000
Collision distance in [646392885392177745215877506577 / 1000000000000000000000000000000, 323196442696088872607938753289 / 500000000000000000000000000000] ~ [0.64639, 0.64639]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [3559 / 10000, 3561 / 10000] ~ [0.3559, 0.3561]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 86657962444121295458844849101970261952437 / 2000000000000000000000000000000000000000000000000000000000000000000000000000000
rho in [260195182813728821110661349707 / 1250000000000000000000000000000000000000000000000, 260195182814978821110661349707 / 1250000000000000000000000000000000000000000000000] ~ [0.0, 0.0]
sigma_min ^ 2 / (16 * E ^ .5) in [3958275312500000000000000000 / 3968626966596885885752423630459, 2641816875000000000000000000 / 2645751311064590590501615753639] ~ [0.001, 0.001]
Success: rho < sigma_min ^ 2 / (16 * E ^ .5)
Checking inequality 4:
LHS NUM := sigma_min - [sigma_min ^ 2 - 16 * rho * |E| ^ .5 ] ^ .5 in [-199999999999962882601728749 / 1000000000000000000000000000000, 200000000000037138256601451 / 1000000000000000000000000000000] ~ [-0.0002, 0.0002]
LHS DEN := 8 * |E| ^ .5 in [7937253933193771771504847260917 / 125000000000000000000000000000, 3968626966596885885752423630459 / 62500000000000000000000000000] ~ [63.49803, 63.49803]
LHS := (LHS NUM) / (LHS DEN) in [-199999999999962882601728749 / 63498031465550174172038778087336, 66666666666679046085533817 / 21166010488516724724012926029112] ~ [-0.0, 0.0]
CD / |V| ^ .5 in [646392885392177745215877506577 / 4795831523312719541597438064163, 323196442696088872607938753289 / 2397915761656359770798719032081] ~ [0.13478, 0.13478]
Success: LHS < CD / |V| ^ .5
Success: existence proven