show/hide visualization coordinates
a : (-1.1028772536437499, -0.6535581368, -0.8013931574687498)
b : (-0.6253465818437501, -0.7156653886000001, 0.07501145883125004)
c : (-1.6178162729437502, -0.8320205797999999, 0.03706698213125004)
d : (-1.93179001924375, -1.2120454111, -0.8329850398687499)
e : (-1.9976178684437502, -0.22860638069999994, -0.66409537026875)
f : (-1.21372522374375, 0.06923569640000005, -0.11928719276874994)
g : (-0.34346371054375, -0.034617141100000026, -0.6008106129687498)
h : (0.3330709170562499, -0.4364599511999999, 0.01629185063125005)
i : (-0.35214982474375, 0.19950114600000002, 0.37134805363125006)
j : (0.38370225605624997, 0.534605176, -0.21705776056874998)
k : (1.22100505995625, 0.021292817600000014, -0.028800925368749952)
l : (0.5864938331562499, 0.23299512920000004, 0.7145655755312501)
m : (1.1277397367562498, 0.9623851134000001, 0.29620859993125004)
n : (2.02808610425625, 0.6071282614, 0.04488083483125005)
o : (1.57310166655625, 0.27646674070000005, 0.87170572313125)
p : (1.93158718135625, 1.2093629086000002, 0.83735098063125)
show/hide computer existence proof
(see shape-existence, preprint)
Attempting to prove existence
Starting realization:
Abstract data:
mode: maximal_simplices
data: [['j', 'g', 'h'], ['p', 'o', 'm'], ['d', 'a', 'e'], ['a', 'g', 'b'], ['k', 'h', 'l'], ['a', 'c', 'b'], ['f', 'g', 'i'], ['a', 'f', 'g'], ['j', 'l', 'i'], ['e', 'c', 'f'], ['k', 'j', 'm'], ['k', 'm', 'n'], ['b', 'f', 'i'], ['b', 'f', 'c'], ['k', 'o', 'l'], ['d', 'a', 'c'], ['h', 'l', 'i'], ['b', 'g', 'h'], ['a', 'e', 'f'], ['p', 'o', 'n'], ['p', 'm', 'n'], ['k', 'o', 'n'], ['d', 'c', 'e'], ['j', 'm', 'l'], ['j', 'g', 'i'], ['o', 'm', 'l'], ['b', 'h', 'i'], ['k', 'j', 'h']]
Coordinate Data:
n : [-4002534179 / 2500000000, 573829889 / 10000000000, 4393641191 / 10000000000]
j : [216850883 / 5000000000, 1299060743 / 10000000000, 1402605429 / 2000000000]
o : [-11460292339 / 10000000000, 485055637 / 1250000000, -968651923 / 2500000000]
p : [-15045147487 / 10000000000, -5448516583 / 10000000000, -3531060267 / 10000000000]
k : [-7939326273 / 10000000000, 6432184327 / 10000000000, 5130458793 / 10000000000]
g : [963170179 / 1250000000, 3495641957 / 5000000000, 10850555669 / 10000000000]
e : [24246903011 / 10000000000, 893117631 / 1000000000, 5741701621 / 5000000000]
b : [2104838029 / 2000000000, 13801766389 / 10000000000, 4092334951 / 10000000000]
m : [-7006673041 / 10000000000, -2978738631 / 10000000000, 94018177 / 500000000]
l : [-318842801 / 2000000000, 4315161211 / 10000000000, -287900777 / 1250000000]
d : [23588624519 / 10000000000, 9382783307 / 5000000000, 6586149969 / 5000000000]
c : [1278055441 / 625000000, 14965318301 / 10000000000, 2235889859 / 5000000000]
a : [15299496863 / 10000000000, 13180693871 / 10000000000, 6428190557 / 5000000000]
i : [3896111287 / 5000000000, 4650101043 / 10000000000, 1128969003 / 10000000000]
h : [235003789 / 2500000000, 2201942403 / 2000000000, 4679531033 / 10000000000]
f : [4101994141 / 2500000000, 5952755539 / 10000000000, 6035321467 / 10000000000]
Desired square lengths:
default : 1
Checking inequality 1:
d = 3
|V| = 16
|E| = 42
Success: d|V| >= |E|
Checking self-intersection:
Square collision distance = 3472289001960984874380645913521974262976539696772472544369 / 6945066196160555145000682704006343352950000000000000000000
Collision distance in [2209631 / 3125000, 70708193 / 100000000] ~ [0.70708, 0.70708]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [3851 / 10000, 3853 / 10000] ~ [0.3851, 0.3853]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 19374201846459492509586431732101 / 1250000000000000000000000000000000000000
rho in [12449 / 100000000, 249 / 2000000] ~ [0.00012, 0.00012]
sigma_min ^ 2 / (16 * E ^ .5) in [14830201 / 10369185120, 14845609 / 10369185104] ~ [0.00143, 0.00143]
Success: rho < sigma_min ^ 2 / (16 * E ^ .5)
Checking inequality 4:
LHS NUM := sigma_min - [sigma_min ^ 2 - 16 * rho * |E| ^ .5 ] ^ .5 in [67729 / 4000000, 867149 / 50000000] ~ [0.01693, 0.01734]
LHS DEN := 8 * |E| ^ .5 in [648074069 / 12500000, 64807407 / 1250000] ~ [51.84593, 51.84593]
LHS := (LHS NUM) / (LHS DEN) in [338645 / 1036918512, 867149 / 2592296276] ~ [0.00033, 0.00033]
CD / |V| ^ .5 in [70708192 / 400000001, 70708193 / 400000000] ~ [0.17677, 0.17677]
Success: LHS < CD / |V| ^ .5
Success: existence proven