show/hide visualization coordinates
a : (-0.04154957120105718, 0.737177643757063, -0.2982906305504589)
b : (-0.4934643333690837, 0.6450041276693366, -1.1855769939454124)
c : (-0.9806708525419335, 0.3972326622569074, -0.34817678579947897)
d : (-0.5056966162589388, 0.42684524024851045, 0.5313245331830891)
e : (0.46246644757690375, 0.6751313884631687, 0.563172145789424)
f : (0.9391283427403452, 0.5416897397105117, -0.3057275976087248)
g : (0.3419620110072581, 0.12985443094713423, -0.9940473276036031)
h : (-0.45366241788520434, -0.33448305838763986, -1.3831134712704887)
i : (-1.337170057171016, 0.11071071052780229, -1.2374537326929516)
j : (-1.8565946493831644, -0.08186820826170899, -0.40492057837229267)
k : (-1.2727733211849293, -0.20074863921571867, 0.39821085537752504)
l : (-0.6720905066788788, -0.3063271995884452, 1.1906963908585912)
m : (-0.015521664639603472, 0.41747369810776935, 1.4028982196852038)
n : (0.9632503403335064, 0.23542886942313465, 1.3087438643419667)
o : (1.4615739401856547, 0.6389467119952363, 0.5413802344008855)
p : (1.7983116633563707, 0.04370186513464003, -0.18820271364526187)
q : (0.972449296799289, -0.4439414906135957, -0.4713198432918726)
r : (0.023387391360884913, -0.7319028529812837, -0.5992250950564922)
s : (-0.9290149364067638, -0.4404923301057076, -0.5097280938768575)
t : (-0.40164124196240014, -0.6827963437639142, 0.3046218010535874)
u : (0.2963812997682662, -0.43077024687328597, 0.9748809880267582)
v : (1.1694133225292367, -0.3165604001943478, 0.500780578666608)
w : (0.531526113025258, -1.0293063182555628, 0.20907325233025548)
show/hide computer existence proof
(see shape-existence, preprint)
Attempting to prove existence
Starting realization:
Abstract data:
mode: maximal_simplices
data: [['o', 'n', 'v'], ['k', 't', 'l'], ['o', 'v', 'p'], ['t', 'u', 'w'], ['m', 'e', 'd'], ['t', 'u', 'l'], ['a', 'd', 'e'], ['t', 'r', 's'], ['r', 'q', 'w'], ['s', 'i', 'h'], ['m', 'd', 'l'], ['g', 'r', 'h'], ['t', 'r', 'w'], ['g', 'f', 'q'], ['i', 'j', 'c'], ['j', 's', 'i'], ['e', 'o', 'f'], ['t', 'k', 's'], ['a', 'f', 'e'], ['m', 'u', 'l'], ['s', 'r', 'h'], ['m', 'e', 'n'], ['g', 'a', 'f'], ['o', 'f', 'p'], ['u', 'w', 'v'], ['g', 'b', 'h'], ['f', 'q', 'p'], ['c', 'b', 'i'], ['m', 'u', 'n'], ['q', 'v', 'w'], ['b', 'i', 'h'], ['k', 's', 'j'], ['a', 'b', 'c'], ['k', 'd', 'l'], ['k', 'd', 'c'], ['g', 'r', 'q'], ['q', 'v', 'p'], ['e', 'o', 'n'], ['u', 'n', 'v'], ['g', 'a', 'b'], ['j', 'c', 'k'], ['a', 'd', 'c']]
Coordinate Data:
k : [86628639551959015349 / 50000000000000000000, 65285361707949895303 / 100000000000000000000, 41574061290966029 / 1250000000000000000]
a : [50134904105530819751 / 100000000000000000000, -28507266589328264993 / 100000000000000000000, 2919042939843027111 / 4000000000000000000]
c : [144047032239618462687 / 100000000000000000000, 2743615780343644607 / 50000000000000000000, 38982344510488839607 / 50000000000000000000]
i : [179696952702526680399 / 100000000000000000000, 34139426733597797629 / 100000000000000000000, 83446191855162471913 / 50000000000000000000]
b : [19065276064466694949 / 20000000000000000000, -19289914980555626707 / 100000000000000000000, 161704709835571037167 / 100000000000000000000]
m : [47532113449385446589 / 100000000000000000000, 3463127975601094543 / 100000000000000000000, -97142811527490605913 / 100000000000000000000]
h : [22836547193486384041 / 25000000000000000000, 19664700906285502639 / 25000000000000000000, 36291671513615727833 / 20000000000000000000]
f : [-23966443644304710141 / 50000000000000000000, -4479238092336571747 / 50000000000000000000, 73719770201902271439 / 100000000000000000000]
v : [-35480692633749277551 / 50000000000000000000, 4804158612863300631 / 6250000000000000000, -3465523712815505663 / 50000000000000000000]
g : [11783745884699289343 / 100000000000000000000, 32225054691664605347 / 100000000000000000000, 71275871600695048501 / 50000000000000000000]
q : [-51264982694503807359 / 100000000000000000000, 89604646847737603591 / 100000000000000000000, 90278994770217045513 / 100000000000000000000]
l : [905511981226503921 / 800000000000000000, 37921608872611273093 / 50000000000000000000, -18980657161207336769 / 25000000000000000000]
d : [96549608611318976957 / 100000000000000000000, 2525973761526986603 / 100000000000000000000, -9985442877279130607 / 100000000000000000000]
o : [-50088723516570178087 / 50000000000000000000, -18684173413145601279 / 100000000000000000000, -10991012999058754641 / 100000000000000000000]
t : [86144071181665116701 / 100000000000000000000, 113490132162769432421 / 100000000000000000000, 6342415167835525091 / 50000000000000000000]
p : [-1045712651173531183 / 781250000000000000, 20420155636457013807 / 50000000000000000000, 30983640902777987723 / 50000000000000000000]
e : [-266697772265270553 / 100000000000000000000, -2787830132492354549 / 12500000000000000000, -1317020413791260923 / 10000000000000000000]
r : [8728241569867322439 / 20000000000000000000, 118400783084506385029 / 100000000000000000000, 103069519946679003851 / 100000000000000000000]
j : [231639411923741524677 / 100000000000000000000, 53397318612548929407 / 100000000000000000000, 20909767069564762599 / 25000000000000000000]
u : [2042727126074810239 / 12500000000000000000, 17657504494741324719 / 20000000000000000000, -27170544180823013661 / 50000000000000000000]
w : [-7172664317100699807 / 100000000000000000000, 148141129611934303429 / 100000000000000000000, 22239685208004240239 / 100000000000000000000]
n : [-25172543523962770429 / 50000000000000000000, 1083380542203228161 / 5000000000000000000, -21931843998291720467 / 25000000000000000000]
s : [27776288125220297573 / 20000000000000000000, 89259730796948782997 / 100000000000000000000, 47059909914357768007 / 50000000000000000000]
Desired square lengths:
default : 1
Checking inequality 1:
d = 3
|V| = 23
|E| = 63
Success: d|V| >= |E|
Checking self-intersection:
Square collision distance = 103621699529694213032597846575998276723216420423548700943587373594357795508075736239255175040957419750790696138955821369 / 245462304427055523793795061163524340677730440164701692846434148851192056461726882500000000000000000000000000000000000000
Collision distance in [649730047916697656965265354571 / 1000000000000000000000000000000, 162432511979174414241316338643 / 250000000000000000000000000000] ~ [0.64973, 0.64973]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [3457 / 10000, 3459 / 10000] ~ [0.3457, 0.3459]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 33719313244666760444839749107057400880913 / 800000000000000000000000000000000000000000000000000000000000000000000000000000
rho in [1026512805032570581961800913329 / 5000000000000000000000000000000000000000000000000, 1026512805037570581961800913329 / 5000000000000000000000000000000000000000000000000] ~ [0.0, 0.0]
sigma_min ^ 2 / (16 * E ^ .5) in [3734640312500000000000000000 / 3968626966596885885752423630459, 2492641875000000000000000000 / 2645751311064590590501615753639] ~ [0.00094, 0.00094]
Success: rho < sigma_min ^ 2 / (16 * E ^ .5)
Checking inequality 4:
LHS NUM := sigma_min - [sigma_min ^ 2 - 16 * rho * |E| ^ .5 ] ^ .5 in [-199999999999962311915354873 / 1000000000000000000000000000000, 8000000000001508395542819 / 40000000000000000000000000000] ~ [-0.0002, 0.0002]
LHS DEN := 8 * |E| ^ .5 in [7937253933193771771504847260917 / 125000000000000000000000000000, 3968626966596885885752423630459 / 62500000000000000000000000000] ~ [63.49803, 63.49803]
LHS := (LHS NUM) / (LHS DEN) in [-199999999999962311915354873 / 63498031465550174172038778087336, 200000000000037709888570475 / 63498031465550174172038778087336] ~ [-0.0, 0.0]
CD / |V| ^ .5 in [649730047916697656965265354571 / 4795831523312719541597438064163, 324865023958348828482632677286 / 2397915761656359770798719032081] ~ [0.13548, 0.13548]
Success: LHS < CD / |V| ^ .5
Success: existence proven