show/hide visualization coordinates
a : (-0.5699164660499998, 0.19021735007500007, -0.89678371664375)
b : (-0.8049410738499998, -0.016931452424999938, 0.05287559445625001)
c : (-0.8724431677499999, 0.9216159308750002, -0.2856096738437499)
d : (0.037675215050000155, 0.9592523195750001, -0.6982451438437499)
e : (0.4185966164500001, 0.04695729047500008, -0.84863352724375)
f : (-0.20448191634999985, -0.6312621752249999, -0.45902924334374995)
g : (-0.45737327504999986, -0.8498839820249999, 0.48344116265625003)
h : (-0.28228744764999986, 0.040572650275000066, 0.9034791831562501)
i : (-0.9707069818499998, 0.7342977679750001, 0.6917623782562501)
j : (-0.05996486724999983, 0.792552933775, 0.28291627465625)
k : (0.8240236558500003, 0.651238666475, -0.16272323124374993)
l : (0.7749779665500001, -0.33341247482499997, 0.004777964856250039)
m : (0.69013525355, -0.914464861725, -0.8046538344437499)
n : (0.3699123175500002, -1.244312459625, 0.08341025835625004)
o : (0.43582824725000013, -0.6551955168249999, 0.88876503585625)
p : (0.6709659235500001, 0.30875801317500007, 0.76425051835625)
show/hide computer existence proof
(see shape-existence, preprint)
Attempting to prove existence
Starting realization:
Abstract data:
mode: maximal_simplices
data: [['c', 'j', 'i'], ['k', 'p', 'l'], ['o', 'g', 'h'], ['d', 'a', 'e'], ['m', 'n', 'l'], ['o', 'n', 'l'], ['a', 'c', 'b'], ['b', 'c', 'i'], ['a', 'f', 'b'], ['p', 'j', 'h'], ['f', 'm', 'n'], ['f', 'e', 'm'], ['p', 'j', 'k'], ['d', 'j', 'k'], ['p', 'o', 'h'], ['b', 'f', 'g'], ['d', 'a', 'c'], ['b', 'g', 'h'], ['d', 'e', 'k'], ['f', 'g', 'n'], ['k', 'e', 'l'], ['a', 'e', 'f'], ['e', 'm', 'l'], ['d', 'c', 'j'], ['p', 'o', 'l'], ['j', 'h', 'i'], ['o', 'g', 'n'], ['b', 'h', 'i']]
Coordinate Data:
n : [348063671 / 400000000, -8803257629 / 10000000000, 1456568241 / 2500000000]
j : [4402819927 / 10000000000, 2313079261 / 2000000000, 7821333127 / 10000000000]
p : [2342425567 / 2000000000, 6727447099 / 10000000000, 3158668891 / 2500000000]
k : [6621352579 / 5000000000, 158628963 / 156250000, 841234517 / 2500000000]
o : [292523471 / 312500000, -2912088201 / 10000000000, 13879820739 / 10000000000]
g : [428735849 / 10000000000, -4858972853 / 10000000000, 9826582007 / 10000000000]
e : [2297108691 / 2500000000, 32104999 / 78125000, -873541223 / 2500000000]
b : [-3046942139 / 10000000000, 3470552443 / 10000000000, 220837053 / 400000000]
l : [2550449653 / 2000000000, 305742219 / 10000000000, 5039950029 / 10000000000]
m : [2380764227 / 2000000000, -110095633 / 200000000, -763591991 / 2500000000]
d : [21516883 / 40000000, 13232390163 / 10000000000, -995140529 / 5000000000]
c : [-1860981539 / 5000000000, 3214006569 / 2500000000, 1068036821 / 5000000000]
a : [-696696061 / 10000000000, 1385510117 / 2500000000, -1987833393 / 5000000000]
i : [-4704601219 / 10000000000, 10982844647 / 10000000000, 11909794163 / 10000000000]
h : [2179594123 / 10000000000, 404559347 / 1000000000, 3506740553 / 2500000000]
f : [739412359 / 2500000000, -534550957 / 2000000000, 401877947 / 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 = 8569972975485222572257153716192698217319513917305885642409 / 15354452541007630166515541574368977654887500000000000000000
Collision distance in [74708937 / 100000000, 37354469 / 50000000] ~ [0.74709, 0.74709]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [1147 / 2000, 5737 / 10000] ~ [0.5735, 0.5737]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 30897174243583938072269 / 10000000000000000000000000000000000000000
rho in [2197199 / 1250000000000000, 14697199 / 1250000000000000] ~ [0.0, 0.0]
sigma_min ^ 2 / (16 * E ^ .5) in [6578045 / 2073837024, 32913169 / 10369185104] ~ [0.00317, 0.00317]
Success: rho < sigma_min ^ 2 / (16 * E ^ .5)
Checking inequality 4:
LHS NUM := sigma_min - [sigma_min ^ 2 - 16 * rho * |E| ^ .5 ] ^ .5 in [-3997 / 20000000, 20107 / 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 [-19985 / 5184592552, 20107 / 5184592552] ~ [-0.0, 0.0]
CD / |V| ^ .5 in [74708937 / 400000001, 37354469 / 200000000] ~ [0.18677, 0.18677]
Success: LHS < CD / |V| ^ .5
Success: existence proven