show/hide visualization coordinates
a : (0.6403312738678641, 0.9209678308012592, -0.29307868237985346)
b : (0.7968401526097395, 0.26685801280125876, 0.4469519364941006)
c : (1.4235147466294806, 0.30037204418705854, -0.33160812086208336)
d : (0.8018733908789423, 0.3699850389644451, -1.1118106944151036)
e : (-0.1321600048621936, 0.6084341116110626, -0.845871499495944)
f : (-0.2454245243485883, 1.3791424006791504, -0.21883092522083647)
g : (0.23152782180777232, 1.0762085071590288, 0.6062433233487591)
h : (-0.06925895939753945, 0.1827096353613671, 0.9396905880675652)
i : (0.4525286484650324, -0.6366376455298732, 0.7021874816095952)
j : (1.2958118247768544, -0.5546539736810367, 0.17100751013135262)
k : (1.1338484849510513, -0.5255085613988237, -0.8153587613395301)
l : (0.1509503043582942, -0.3502963917899384, -0.872032054947675)
m : (-0.769175417593951, -0.1088983780415303, -0.563656221328724)
n : (-1.0428066717461464, 0.8515357368709255, -0.5117693476184684)
o : (-0.700033785353407, 0.7619635047507445, 0.4233689114571608)
p : (-1.0559929843521094, 0.039426659824684185, 1.016018518200046)
q : (-0.4267041997836859, -0.7221678959887441, 1.1708389243865158)
r : (-0.19909915974076886, -1.340008924128708, 0.41819796769201445)
s : (0.5023597128654361, -1.0215642051549387, -0.21941352138244452)
t : (-0.4550592599649067, -1.0565300004640954, -0.5059903934829151)
u : (-0.8832125348890495, -0.6225830061082289, 0.28671054587646333)
v : (-1.4506588591781227, 0.18124549927493155, 0.10820451521000485)
show/hide computer existence proof
(see shape-existence, preprint)
Attempting to prove existence
Starting realization:
Abstract data:
mode: maximal_simplices
data: [['q', 'i', 'h'], ['n', 'e', 'f'], ['n', 'e', 'm'], ['j', 'k', 's'], ['n', 'o', 'v'], ['u', 'v', 'm'], ['u', 'q', 'p'], ['s', 't', 'r'], ['v', 'n', 'm'], ['s', 'r', 'i'], ['v', 'o', 'p'], ['o', 'f', 'g'], ['b', 'i', 'h'], ['f', 'a', 'g'], ['v', 'u', 'p'], ['q', 'p', 'h'], ['b', 'g', 'h'], ['d', 'k', 'c'], ['l', 't', 's'], ['o', 'g', 'h'], ['q', 'r', 'i'], ['n', 'o', 'f'], ['a', 'g', 'b'], ['j', 'k', 'c'], ['j', 's', 'i'], ['l', 'd', 'k'], ['l', 'k', 's'], ['d', 'e', 'a'], ['l', 't', 'm'], ['j', 'b', 'c'], ['u', 't', 'r'], ['d', 'a', 'c'], ['u', 't', 'm'], ['a', 'b', 'c'], ['o', 'p', 'h'], ['e', 'a', 'f'], ['u', 'q', 'r'], ['l', 'e', 'm'], ['l', 'd', 'e'], ['j', 'b', 'i']]
Coordinate Data:
e : [1193111541990998967 / 1562500000000000000, -12765357038361859089 / 50000000000000000000, 144205702092319209193 / 100000000000000000000]
n : [1674238053758192339 / 1000000000000000000, -24920438301355006929 / 50000000000000000000, 6924717931535726891 / 6250000000000000000]
t : [108649064197695243379 / 100000000000000000000, 140965697130792080601 / 100000000000000000000, 55108795745508156419 / 50000000000000000000]
i : [17890273354701339741 / 100000000000000000000, 98976461637369867267 / 100000000000000000000, -1060019601823472547 / 10000000000000000000]
h : [70069034140958524519 / 100000000000000000000, 1704173354824583269 / 10000000000000000000, -34350506664031727877 / 100000000000000000000]
q : [105813558179573162533 / 100000000000000000000, 53764743341628472977 / 50000000000000000000, -14366335073981695677 / 25000000000000000000]
u : [151464391690109533083 / 100000000000000000000, 97570997695205445469 / 100000000000000000000, 30947497555078466859 / 100000000000000000000]
s : [1613395864332620427 / 12500000000000000000, 17183639699984551207 / 12500000000000000000, 81559904280969255257 / 100000000000000000000]
d : [-2130525110836206833 / 12500000000000000000, -84290340603098537 / 5000000000000000000, 42699905396058793181 / 25000000000000000000]
v : [104104512059508405519 / 50000000000000000000, 17188147156889387049 / 100000000000000000000, 9759620124344863653 / 20000000000000000000]
o : [133146516736545281253 / 100000000000000000000, -40883653390691909397 / 100000000000000000000, 17281660997008716069 / 100000000000000000000]
r : [41526527087640731369 / 50000000000000000000, 169313589497253347863 / 100000000000000000000, 17798755373523357771 / 100000000000000000000]
p : [2636600572443992153 / 1562500000000000000, 6274006220382825347 / 20000000000000000000, -20991649838639905091 / 50000000000000000000]
a : [-177997837116367699 / 20000000000000000000, -56784085995743367609 / 100000000000000000000, 88926420380710141759 / 100000000000000000000]
k : [-25120855146950279299 / 50000000000000000000, 87863553224264923151 / 100000000000000000000, 141154428276677818583 / 100000000000000000000]
c : [-19802084115435871451 / 25000000000000000000, 5275492665676692747 / 100000000000000000000, 46389682114466566283 / 50000000000000000000]
m : [35015169990149919251 / 25000000000000000000, 46202534888535575171 / 100000000000000000000, 57992087137798602573 / 50000000000000000000]
b : [-8270438529884689297 / 50000000000000000000, 8626895804256670279 / 100000000000000000000, 373083962332868611 / 2500000000000000000]
j : [-16609511069120217297 / 25000000000000000000, 45389047226243107691 / 50000000000000000000, 21258900564794769559 / 50000000000000000000]
l : [48048107765375152413 / 100000000000000000000, 14068467252675275291 / 20000000000000000000, 14682175763749229499 / 10000000000000000000]
f : [87685590636063407807 / 100000000000000000000, -51300771491766254061 / 50000000000000000000, 407508223324042231 / 500000000000000000]
g : [9997589005106835397 / 25000000000000000000, -72308153631520332977 / 100000000000000000000, -1005780192151103157 / 100000000000000000000]
Desired square lengths:
default : 1
Checking inequality 1:
d = 3
|V| = 22
|E| = 60
Success: d|V| >= |E|
Checking self-intersection:
Square collision distance = 2437379368181162445317336868689269389434050944089786349632271414322677149077961047315156680119599952546209669004979889 / 3840268704891844468061717917239123066330540179485910294591299870920764595038286800000000000000000000000000000000000000
Collision distance in [796674210639348512201368688837 / 1000000000000000000000000000000, 398337105319674256100684344419 / 500000000000000000000000000000] ~ [0.79667, 0.79667]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [2457 / 5000, 1229 / 2500] ~ [0.4914, 0.4916]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 1418315784346749821667978055026316544431223 / 25000000000000000000000000000000000000000000000000000000000000000000000000000000
rho in [2381861275848574537774420442253 / 10000000000000000000000000000000000000000000000000, 2381861275858574537774420442253 / 10000000000000000000000000000000000000000000000000] ~ [0.0, 0.0]
sigma_min ^ 2 / (16 * E ^ .5) in [431203500000000000000000000 / 221313334068995250581672308559, 3776102500000000000000000000 / 1936491673103708442589632699891] ~ [0.00195, 0.00195]
Success: rho < sigma_min ^ 2 / (16 * E ^ .5)
Checking inequality 4:
LHS NUM := sigma_min - [sigma_min ^ 2 - 16 * rho * |E| ^ .5 ] ^ .5 in [-199999999999969975885909397 / 1000000000000000000000000000000, 40000000000006007266783477 / 200000000000000000000000000000] ~ [-0.0002, 0.0002]
LHS DEN := 8 * |E| ^ .5 in [1936491673103708442589632699891 / 31250000000000000000000000000, 1549193338482966754071706159913 / 25000000000000000000000000000] ~ [61.96773, 61.96773]
LHS := (LHS NUM) / (LHS DEN) in [-199999999999969975885909397 / 61967733539318670162868246396512, 200000000000030036333917385 / 61967733539318670162868246396512] ~ [-0.0, 0.0]
CD / |V| ^ .5 in [796674210639348512201368688837 / 4690415759823429554565630113545, 44259678368852695122298260491 / 260578653323523864142535006308] ~ [0.16985, 0.16985]
Success: LHS < CD / |V| ^ .5
Success: existence proven