show/hide visualization coordinates
a : (-0.32465609437487875, 1.0001225933993318, -0.33258762657995966)
b : (0.4734870325422027, 1.316535820316761, 0.18010157633611795)
c : (0.5570984161347781, 1.1023035577100435, -0.7930960778904742)
d : (-0.05405573370770955, 0.35164641797350904, -1.0441029775822381)
e : (-0.9914944437914922, 0.3495169084484475, -0.6959591423278473)
f : (-1.1531601018467654, 0.7907165283843551, 0.1867679448140202)
g : (-0.270716363227587, 0.8457648873543939, 0.653953910299407)
h : (0.6797726067462987, 0.6169427070943936, 0.8642183337738543)
i : (0.8120017653080699, 0.42055675516319735, -0.10735153376533824)
j : (0.9369666818677004, 0.2227473627882407, -1.0795938975396673)
k : (0.3257247823060988, -0.5329066859195696, -1.3149028410412251)
l : (-0.45400059701888823, -0.49372976315222566, -0.6900080486489483)
m : (-0.8915967548645873, -0.17378115633090957, 0.1503148009938428)
n : (-1.003252202678007, 0.2809476803257378, 1.0339180751426413)
o : (-0.052461089447003395, -0.02140260531426369, 1.1015979375417193)
p : (0.7198171804958252, -0.33040561185772743, 0.546527297243377)
q : (0.7942246739711288, -0.5252919807369432, -0.4314721036459062)
r : (0.17151398204685053, -1.2733939848004843, -0.6607640260489871)
s : (-0.307103263315103, -0.9849749153132518, 0.16853686795647266)
t : (-0.7848911838602161, -0.6942408864084384, 0.9975075715509676)
u : (0.16725903290635424, -0.9955359571603075, 1.0488032346424954)
v : (0.6495216738069317, -1.2721376719642914, 0.21759072477567648)
show/hide computer existence proof
(see shape-existence, preprint)
Attempting to prove existence
Starting realization:
Abstract data:
mode: maximal_simplices
data: [['n', 't', 'm'], ['j', 'i', 'c'], ['d', 'j', 'k'], ['v', 'q', 'p'], ['u', 't', 's'], ['q', 'k', 'r'], ['n', 'f', 'm'], ['n', 'o', 't'], ['v', 's', 'r'], ['t', 's', 'm'], ['p', 'i', 'h'], ['n', 'f', 'g'], ['v', 'u', 's'], ['q', 'j', 'k'], ['b', 'i', 'h'], ['f', 'a', 'g'], ['u', 'p', 'v'], ['d', 'j', 'c'], ['b', 'g', 'h'], ['o', 'g', 'h'], ['n', 'o', 'g'], ['b', 'i', 'c'], ['q', 'j', 'i'], ['a', 'g', 'b'], ['l', 's', 'r'], ['q', 'p', 'i'], ['l', 's', 'm'], ['l', 'd', 'k'], ['d', 'e', 'a'], ['d', 'a', 'c'], ['u', 'o', 't'], ['v', 'q', 'r'], ['a', 'b', 'c'], ['o', 'p', 'h'], ['u', 'o', 'p'], ['e', 'a', 'f'], ['e', 'f', 'm'], ['l', 'e', 'm'], ['l', 'd', 'e'], ['l', 'k', 'r']]
Coordinate Data:
e : [-55457826376886383931 / 100000000000000000000, 41555514351578280129 / 50000000000000000000, -27419887617272669841 / 100000000000000000000]
n : [-11326720453107575299 / 20000000000000000000, 38127052945442798441 / 50000000000000000000, 145567834129776190861 / 100000000000000000000]
t : [-17398750191879385041 / 50000000000000000000, -5316187695633008037 / 25000000000000000000, 141926783770608808037 / 100000000000000000000]
i : [31222948633267452943 / 25000000000000000000, 22553753343657887361 / 25000000000000000000, 3930109154872279531 / 12500000000000000000]
h : [111668878676892703787 / 100000000000000000000, 54926804283875589311 / 50000000000000000000, 64298929996448738007 / 50000000000000000000]
q : [123114085399375711607 / 100000000000000000000, -4369860215382508933 / 100000000000000000000, -971183749078564097 / 100000000000000000000]
u : [60417521292898253341 / 100000000000000000000, -51394257857718940331 / 100000000000000000000, 147056350079761580217 / 100000000000000000000]
s : [12981291670752532773 / 100000000000000000000, -5033815367301336833 / 10000000000000000000, 3689357088197457421 / 6250000000000000000]
d : [19143022315745938603 / 50000000000000000000, 41661989827831358123 / 50000000000000000000, -15558567785677939017 / 25000000000000000000]
v : [108643785382956004769 / 100000000000000000000, -2470450916816166369 / 3125000000000000000, 998985923329370439 / 1562500000000000000]
o : [7689101811512499271 / 20000000000000000000, 23009538663442721729 / 50000000000000000000, 152335820369683988357 / 100000000000000000000]
r : [60843016206947884523 / 100000000000000000000, -79180060621736598007 / 100000000000000000000, -23900375989386648121 / 100000000000000000000]
p : [28918334012961338223 / 25000000000000000000, 7559388336269535157 / 50000000000000000000, 96828756339849756489 / 100000000000000000000]
a : [11226008564774955189 / 100000000000000000000, 74085798599122494373 / 50000000000000000000, 8917263957516090539 / 100000000000000000000]
k : [953301202910908867 / 1250000000000000000, -641416341705643057 / 12500000000000000000, -22328564372152612283 / 25000000000000000000]
c : [99401459615740639009 / 100000000000000000000, 158389693629316157429 / 100000000000000000000, -18566790586767681309 / 50000000000000000000]
m : [-45468057484195901783 / 100000000000000000000, 3078122222522085301 / 10000000000000000000, 14301876678724085321 / 25000000000000000000]
b : [91040321256483103533 / 100000000000000000000, 44953229972496976487 / 25000000000000000000, 60186184249123854653 / 100000000000000000000]
j : [137388286189032869781 / 100000000000000000000, 17608518534283970133 / 25000000000000000000, -65783363138454679709 / 100000000000000000000]
l : [-427110424906496843 / 25000000000000000000, -1213638456910754027 / 100000000000000000000, -26824778249382766383 / 100000000000000000000]
f : [-71624392182413711793 / 100000000000000000000, 63615495348373661953 / 50000000000000000000, 30426410548457039169 / 50000000000000000000]
g : [4154995419876032857 / 25000000000000000000, 1659197832421889997 / 1250000000000000000, 26892854411363184827 / 25000000000000000000]
Desired square lengths:
default : 1
Checking inequality 1:
d = 3
|V| = 22
|E| = 60
Success: d|V| >= |E|
Checking self-intersection:
Square collision distance = 46544757293561297789673837100879620916397569817440748753617704358565863453915764543274115903443192288988154883136198067 / 75171771135736665019287736249493587657567736300298043674838909580539880214753470000000000000000000000000000000000000000
Collision distance in [39343953482987845072042171847 / 50000000000000000000000000000, 786879069659756901440843436941 / 1000000000000000000000000000000] ~ [0.78688, 0.78688]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [3911 / 10000, 3913 / 10000] ~ [0.3911, 0.3913]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 2348181813308170766149050944732141282651703 / 50000000000000000000000000000000000000000000000000000000000000000000000000000000
rho in [216710950960405817981513356113 / 1000000000000000000000000000000000000000000000000, 216710950961405817981513356113 / 1000000000000000000000000000000000000000000000000] ~ [0.0, 0.0]
sigma_min ^ 2 / (16 * E ^ .5) in [1911990125000000000000000000 / 1549193338482966754071706159913, 2392432656250000000000000000 / 1936491673103708442589632699891] ~ [0.00123, 0.00124]
Success: rho < sigma_min ^ 2 / (16 * E ^ .5)
Checking inequality 4:
LHS NUM := sigma_min - [sigma_min ^ 2 - 16 * rho * |E| ^ .5 ] ^ .5 in [-199999999999965680842156487 / 1000000000000000000000000000000, 100000000000017168353955803 / 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 [-199999999999965680842156487 / 61967733539318670162868246396512, 100000000000017168353955803 / 30983866769659335081434123198256] ~ [-0.0, 0.0]
CD / |V| ^ .5 in [157375813931951380288168687388 / 938083151964685910913126022709, 786879069659756901440843436941 / 4690415759823429554565630113544] ~ [0.16776, 0.16776]
Success: LHS < CD / |V| ^ .5
Success: existence proven