show/hide visualization coordinates
a : (0.76267556779375, -0.48698272265000003, 0.38364407413750007)
b : (0.52464797839375, 0.46443583624999996, 0.1883351075375001)
c : (-0.0032145196062500214, -0.05525313805000004, 0.8601122679375)
d : (-0.07367439200625003, -1.00630312925, 0.5592147433375001)
e : (0.37033516589374993, -1.06093205095, -0.33514043966249996)
f : (1.35759322499375, -0.9051215474500001, -0.30281998486249995)
g : (0.74210159049375, -0.16059255295000002, -0.5613671260624999)
h : (0.11844909529375003, 0.60597915555, -0.7144206490624999)
i : (-0.18677121880625003, 1.15593740535, 0.0630023267375)
j : (0.13232342509374995, 0.9278837741499999, 0.9828773995375)
k : (-0.74781999840625, 0.58113050255, 0.6586711032374999)
l : (-0.7509944084062501, -0.33509522575000006, 0.25802120863750005)
m : (-0.61971094570625, -1.18013605345, -0.26031328926249997)
n : (-0.24429876090625002, -0.31933829865, -0.6039597886624999)
o : (-0.79622046060625, 0.46962122824999997, -0.3339129370624999)
p : (-0.5854213435062501, 1.30476681705, -0.8419440164625)
show/hide computer existence proof
(see shape-existence, preprint)
Attempting to prove existence
Starting realization:
Abstract data:
mode: maximal_simplices
data: [['d', 'a', 'e'], ['a', 'g', 'b'], ['m', 'n', 'l'], ['d', 'c', 'l'], ['k', 'c', 'l'], ['o', 'n', 'l'], ['a', 'c', 'b'], ['a', 'f', 'g'], ['b', 'c', 'j'], ['h', 'g', 'n'], ['p', 'h', 'i'], ['p', 'o', 'i'], ['f', 'e', 'g'], ['b', 'j', 'i'], ['k', 'o', 'l'], ['k', 'o', 'i'], ['p', 'o', 'h'], ['d', 'a', 'c'], ['b', 'g', 'h'], ['a', 'e', 'f'], ['d', 'm', 'l'], ['e', 'g', 'n'], ['e', 'n', 'm'], ['o', 'h', 'n'], ['k', 'c', 'j'], ['b', 'h', 'i'], ['e', 'd', 'm'], ['k', 'j', 'i']]
Coordinate Data:
n : [1071401991 / 5000000000, 209133803 / 1000000000, -1252510737 / 10000000000]
j : [2954512921 / 5000000000, 7281779379 / 5000000000, 2923172229 / 2000000000]
o : [-675282603 / 2000000000, 9980933299 / 10000000000, 1447957779 / 10000000000]
k : [-2892408393 / 10000000000, 5548013021 / 5000000000, 5686899091 / 5000000000]
p : [-317105461 / 2500000000, 18332389187 / 10000000000, -726470603 / 2000000000]
g : [1500850937 / 1250000000, 3678795487 / 10000000000, -826584111 / 10000000000]
e : [33156573 / 40000000, -5324599493 / 10000000000, 1435682753 / 10000000000]
m : [-805658933 / 5000000000, -3258319759 / 5000000000, 2183954257 / 10000000000]
l : [-2924152493 / 10000000000, 1933768759 / 10000000000, 1841824809 / 2500000000]
b : [78658171 / 80000000, 9929079379 / 10000000000, 266817529 / 400000000]
d : [3849047671 / 10000000000, -1194577569 / 2500000000, 10379234583 / 10000000000]
c : [910729279 / 2000000000, 1183047409 / 2500000000, 13388209829 / 10000000000]
a : [12212547269 / 10000000000, 41489379 / 1000000000, 8623527891 / 10000000000]
i : [2718079403 / 10000000000, 1684409507 / 1000000000, 5417110417 / 10000000000]
h : [360642659 / 625000000, 2836128143 / 2500000000, -2357119341 / 10000000000]
f : [18161723841 / 10000000000, -1883247229 / 5000000000, 1758887301 / 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 = 31249999984292315103696093034614213075715903296106968777969 / 62499999991417284168710701050396803881925000000000000000000
Collision distance in [35355339 / 50000000, 70710679 / 100000000] ~ [0.70711, 0.70711]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [7077 / 10000, 7079 / 10000] ~ [0.7077, 0.7079]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 13040482275786038727421 / 10000000000000000000000000000000000000000
rho in [114194931 / 100000000000000000, 1114194931 / 100000000000000000] ~ [0.0, 0.0]
sigma_min ^ 2 / (16 * E ^ .5) in [794983 / 164590240, 50112241 / 10369185104] ~ [0.00483, 0.00483]
Success: rho < sigma_min ^ 2 / (16 * E ^ .5)
Checking inequality 4:
LHS NUM := sigma_min - [sigma_min ^ 2 - 16 * rho * |E| ^ .5 ] ^ .5 in [-2499 / 12500000, 10041 / 50000000] ~ [-0.0002, 0.0002]
LHS DEN := 8 * |E| ^ .5 in [648074069 / 12500000, 64807407 / 1250000] ~ [51.84593, 51.84593]
LHS := (LHS NUM) / (LHS DEN) in [-2499 / 648074069, 10041 / 2592296276] ~ [-0.0, 0.0]
CD / |V| ^ .5 in [70710678 / 400000001, 70710679 / 400000000] ~ [0.17678, 0.17678]
Success: LHS < CD / |V| ^ .5
Success: existence proven