show/hide visualization coordinates
a : (0.025025740413333386, 0.5674303993733333, -0.20652921305999983)
b : (0.6309496171133334, -0.028652457626666683, -0.7333512731599999)
c : (-0.22093771408666657, 0.3026756928733333, -1.13894914226)
d : (-0.7973749145866666, 0.022876152873333333, -0.37120415115999983)
e : (-0.7470814744866667, 0.6238906436733334, 0.4264500042400002)
f : (0.18918278781333336, 0.6354718017733333, 0.7775555552400002)
g : (0.9071289131133333, 0.2892882653733333, 0.17364304494000016)
h : (0.31315269961333336, -0.5101242157266667, 0.08346575984000015)
i : (-0.16521708728666668, -0.6314106830266666, -0.7862766962599997)
j : (0.32862662401333337, -0.38107640502666673, -1.6190138325599999)
k : (-0.6249253597866666, -0.8563846954266667, 0.07282457714000012)
l : (-1.2854238979866668, -0.2178221002266667, 0.46776696924000016)
m : (-0.3367130046866666, -0.21505354502666674, 0.7838998148400002)
n : (0.6426219258133334, -0.23121899992666672, 0.9854978597400001)
o : (1.1409851450133335, 0.6301101460733334, 1.08422072324)
show/hide computer existence proof
(see shape-existence, preprint)
Attempting to prove existence
Starting realization:
Abstract data:
mode: maximal_simplices
data: [['d', 'i', 'k'], ['a', 'd', 'e'], ['d', 'e', 'l'], ['l', 'd', 'k'], ['b', 'h', 'i'], ['j', 'c', 'i'], ['o', 'f', 'g'], ['h', 'n', 'm'], ['h', 'i', 'k'], ['d', 'c', 'i'], ['b', 'h', 'g'], ['a', 'b', 'g'], ['o', 'f', 'n'], ['o', 'n', 'g'], ['f', 'e', 'm'], ['f', 'n', 'm'], ['j', 'b', 'i'], ['a', 'b', 'c'], ['a', 'f', 'e'], ['a', 'c', 'd'], ['h', 'k', 'm'], ['h', 'n', 'g'], ['j', 'b', 'c'], ['l', 'k', 'm'], ['a', 'f', 'g'], ['e', 'l', 'm']]
Coordinate Data:
e : [11905699159 / 10000000000, -1527381101 / 10000000000, 1529487013 / 10000000000]
o : [-1743741759 / 2500000000, -12716609 / 80000000, -5048220177 / 10000000000]
m : [7802014461 / 10000000000, 3431030393 / 5000000000, -2045011093 / 10000000000]
h : [651678709 / 5000000000, 9812767493 / 10000000000, 4959329457 / 10000000000]
g : [-4636404717 / 10000000000, 909321341 / 5000000000, 2028778303 / 5000000000]
a : [418462701 / 1000000000, -481389329 / 5000000000, 3929639593 / 5000000000]
l : [8644561697 / 5000000000, 3444873169 / 5000000000, 1116317363 / 10000000000]
d : [310215839 / 250000000, 4482763807 / 10000000000, 9506028567 / 10000000000]
c : [1328852311 / 2000000000, 1684768407 / 10000000000, 8591739239 / 5000000000]
n : [-497833711 / 2500000000, 1404743067 / 2000000000, -2030495771 / 5000000000]
b : [-1874611757 / 10000000000, 624756239 / 1250000000, 13127499787 / 10000000000]
j : [574309087 / 5000000000, 4261144693 / 5000000000, 21984125381 / 10000000000]
k : [2671034503 / 2500000000, 1327537229 / 1000000000, 1266435321 / 2500000000]
i : [6087055287 / 10000000000, 5512816083 / 5000000000, 6828377009 / 5000000000]
f : [317882067 / 1250000000, -821596341 / 5000000000, -1981568497 / 10000000000]
Desired square lengths:
default : 1
Checking inequality 1:
d = 3
|V| = 15
|E| = 39
Success: d|V| >= |E|
Checking self-intersection:
Square collision distance = 499999999661977204790685295343708371391263732730779359692569 / 999999999662339202768544858201495627016100000000000000000000
Collision distance in [35355339 / 50000000, 70710679 / 100000000] ~ [0.70711, 0.70711]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [7143 / 10000, 1429 / 2000] ~ [0.7143, 0.7145]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 10787966892881587685047 / 10000000000000000000000000000000000000000
rho in [51932569 / 50000000000000000, 551932569 / 50000000000000000] ~ [0.0, 0.0]
sigma_min ^ 2 / (16 * E ^ .5) in [17007483 / 3330665600, 51051025 / 9991996784] ~ [0.00511, 0.00511]
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, 10039 / 50000000] ~ [-0.0002, 0.0002]
LHS DEN := 8 * |E| ^ .5 in [624499799 / 12500000, 3122499 / 62500] ~ [49.95998, 49.95998]
LHS := (LHS NUM) / (LHS DEN) in [-19993 / 4995998392, 10039 / 2497999196] ~ [-0.0, 0.0]
CD / |V| ^ .5 in [23570226 / 129099445, 70710679 / 387298334] ~ [0.18257, 0.18257]
Success: LHS < CD / |V| ^ .5
Success: existence proven