show/hide visualization coordinates
a : (-0.62872768408125, 0.05818999201249997, -0.4458154966500001)
b : (0.11546314671874996, 0.1554745768125, -1.10666019605)
c : (-0.68604479168125, -0.3975827342875001, -1.3340643193500001)
d : (-0.9729057707812501, -0.8788008575875, -0.5057287012500001)
e : (-0.40027229898125, -0.6049279288875, 0.26698374574999995)
f : (-0.39027783338125, 0.37363680461250004, 0.47268054424999995)
g : (0.05534175691874993, 0.7777246094124999, -0.3261537481500001)
h : (0.58140124251875, -0.06938641348750008, -0.2508919880500001)
i : (2.0596818749996082e-05, -0.7495872487875, -0.6973484452500001)
j : (-0.30040916498125003, -1.5169343085875, -0.1308500358500001)
k : (0.5109405961187501, -0.9924440150875, 0.12726136864999993)
l : (0.39142802471875, -0.19780427548750007, 0.7224625358499999)
m : (0.20175354991875, 0.6408706288124999, 1.23299950645)
n : (-0.02670183528125003, 1.3039885498125, 0.5202002641499999)
o : (0.74305365371875, 0.6784494419125, 0.39301020274999987)
p : (0.80593681171875, 1.4191331788125, 1.0619147627499999)
show/hide computer existence proof
(see shape-existence, preprint)
Attempting to prove existence
Starting realization:
Abstract data:
mode: maximal_simplices
data: [['p', 'o', 'm'], ['k', 'h', 'i'], ['o', 'g', 'h'], ['d', 'a', 'e'], ['a', 'g', 'b'], ['k', 'h', 'l'], ['d', 'j', 'e'], ['a', 'c', 'b'], ['b', 'c', 'i'], ['a', 'f', 'g'], ['f', 'm', 'n'], ['o', 'h', 'l'], ['k', 'j', 'e'], ['f', 'm', 'l'], ['f', 'e', 'l'], ['d', 'a', 'c'], ['d', 'c', 'i'], ['b', 'g', 'h'], ['f', 'g', 'n'], ['k', 'e', 'l'], ['a', 'e', 'f'], ['o', 'g', 'n'], ['p', 'o', 'n'], ['p', 'm', 'n'], ['o', 'm', 'l'], ['b', 'h', 'i'], ['k', 'j', 'i'], ['d', 'j', 'i']]
Coordinate Data:
n : [886406473 / 2000000000, 9703264423 / 5000000000, 5245876557 / 5000000000]
j : [423739767 / 2500000000, -4401349869 / 5000000000, 1990625057 / 5000000000]
o : [2425917451 / 2000000000, 13151137767 / 10000000000, 3687941 / 4000000]
p : [2551683767 / 2000000000, 642436723 / 312500000, 159088981 / 100000000]
k : [9808456679 / 10000000000, -3557796803 / 10000000000, 6562364159 / 10000000000]
g : [5252468287 / 10000000000, 7071944721 / 5000000000, 2028212991 / 10000000000]
e : [43520483 / 625000000, 317364059 / 10000000000, 795958793 / 1000000000]
b : [1170736437 / 2000000000, 1980347279 / 2500000000, -180526609 / 312500000]
m : [6716586217 / 10000000000, 3193837409 / 2500000000, 17619745537 / 10000000000]
l : [1722666193 / 2000000000, 4388600593 / 10000000000, 12514375831 / 10000000000]
d : [-503000699 / 1000000000, -605341307 / 2500000000, 11623173 / 500000000]
c : [-2161397199 / 10000000000, 478163201 / 2000000000, -8050892721 / 10000000000]
a : [-1588226123 / 10000000000, 1737135817 / 2500000000, 415797753 / 5000000000]
i : [2349628343 / 5000000000, -56461457 / 500000000, -84186699 / 500000000]
h : [10513063143 / 10000000000, 5672779213 / 10000000000, 21725239 / 78125000]
f : [3110439 / 39062500, 5051505697 / 5000000000, 2003311183 / 2000000000]
Desired square lengths:
default : 1
Checking inequality 1:
d = 3
|V| = 16
|E| = 42
Success: d|V| >= |E|
Checking self-intersection:
Square collision distance = 13888888890219187284080393459365868763114431016081795357169 / 27777777782654923952917159683366517565825000000000000000000
Collision distance in [35355339 / 50000000, 70710679 / 100000000] ~ [0.70711, 0.70711]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [263 / 400, 6577 / 10000] ~ [0.6575, 0.6577]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 33320816142086970349 / 40000000000000000000000000000000000000
rho in [456349757 / 500000000000000000, 5456349757 / 500000000000000000] ~ [0.0, 0.0]
sigma_min ^ 2 / (16 * E ^ .5) in [8646125 / 2073837024, 43256929 / 10369185104] ~ [0.00417, 0.00417]
Success: rho < sigma_min ^ 2 / (16 * E ^ .5)
Checking inequality 4:
LHS NUM := sigma_min - [sigma_min ^ 2 - 16 * rho * |E| ^ .5 ] ^ .5 in [-19993 / 100000000, 20087 / 100000000] ~ [-0.0002, 0.0002]
LHS DEN := 8 * |E| ^ .5 in [648074069 / 12500000, 64807407 / 1250000] ~ [51.84593, 51.84593]
LHS := (LHS NUM) / (LHS DEN) in [-19993 / 5184592552, 20087 / 5184592552] ~ [-0.0, 0.0]
CD / |V| ^ .5 in [70710678 / 400000001, 70710679 / 400000000] ~ [0.17678, 0.17678]
Success: LHS < CD / |V| ^ .5
Success: existence proven