show/hide visualization coordinates
a : (-0.24522777165840412, -0.41963545013008197, 0.8580444820786447)
b : (-1.0660503681061098, -0.4401206331239136, 0.2872287303350929)
c : (-0.4539828016558567, -1.2305568307823669, 0.31139299177448887)
d : (0.4788425673972268, -0.8711116902765909, 0.33661246476187545)
e : (0.7132384603071571, -0.1998130294218664, 1.0397601543133739)
f : (-0.004215092829465084, 0.45308287881916387, 1.2826332324709915)
g : (-0.9333396303171699, 0.3006493187439402, 0.9457480834942943)
h : (-1.1082023142245145, 0.5118908010661782, -0.015917179434040807)
i : (-1.4853277735429191, -0.21340845794555258, -0.591866285528422)
j : (-0.670552543755043, -0.7923636542324046, -0.5610084564316368)
k : (0.15137454442923998, -1.3553812517230077, -0.47471218406246113)
l : (1.0423756432203923, -0.9016024150435624, -0.48891814530444255)
m : (1.083908697438413, -0.10619057205582522, 0.1157263828624584)
n : (0.6535102579346785, 0.6775061695725333, 0.5635841732757146)
o : (-0.31309716145051725, 0.9051015012671391, 0.4458112486269876)
p : (-0.4961166276878473, 1.1279639763477958, -0.5117043868480299)
q : (-0.5877759050743753, 0.174986773228741, -0.8005521446796657)
r : (0.2248752922513954, -0.407553555343659, -0.7849061524851257)
s : (1.1258254326593287, 0.016741860143972498, -0.8758030440442077)
t : (1.1889692914148033, 0.8102170978711045, -0.2704850282745297)
u : (0.3811650266751791, 1.37442643776692, -0.09983893062561455)
v : (0.31980277657440886, 0.5851707252513461, -0.7108300062757458)
show/hide computer existence proof
(see shape-existence, preprint)
Attempting to prove existence
Starting realization:
Abstract data:
mode: maximal_simplices
data: [['q', 'i', 'h'], ['n', 'e', 'f'], ['n', 't', 'm'], ['n', 'e', 'm'], ['n', 'o', 'u'], ['v', 's', 'r'], ['t', 's', 'm'], ['q', 'j', 'r'], ['n', 't', 'u'], ['v', 't', 's'], ['o', 'f', 'g'], ['b', 'i', 'h'], ['f', 'a', 'g'], ['u', 'p', 'v'], ['q', 'p', 'h'], ['b', 'g', 'h'], ['d', 'k', 'c'], ['o', 'g', 'h'], ['n', 'o', 'f'], ['d', 'e', 'm'], ['q', 'j', 'i'], ['a', 'g', 'b'], ['l', 's', 'r'], ['j', 'k', 'c'], ['l', 'd', 'm'], ['l', 'd', 'k'], ['l', 's', 'm'], ['d', 'e', 'a'], ['j', 'b', 'c'], ['j', 'k', 'r'], ['d', 'a', 'c'], ['v', 'q', 'r'], ['v', 't', 'u'], ['a', 'b', 'c'], ['o', 'p', 'h'], ['u', 'o', 'p'], ['v', 'q', 'p'], ['e', 'a', 'f'], ['l', 'k', 'r'], ['j', 'b', 'i']]
Coordinate Data:
e : [11018629795225209487 / 10000000000000000000, 6875080193117047081 / 20000000000000000000, 78199174443542238811 / 50000000000000000000]
n : [52106738857502122481 / 50000000000000000000, 122107320865025212103 / 100000000000000000000, 2719518769582964301 / 2500000000000000000]
t : [157759381063016721263 / 100000000000000000000, 135378413694882315837 / 100000000000000000000, 25373830628294135053 / 100000000000000000000]
i : [-109670325432755516491 / 100000000000000000000, 6603171622643323903 / 20000000000000000000, -422768443568443409 / 6250000000000000000]
h : [-4497361218807191781 / 6250000000000000000, 26386446003597422557 / 25000000000000000000, 635382693904287871 / 1250000000000000000]
q : [-9957569292950564069 / 50000000000000000000, 71855381230645979351 / 100000000000000000000, -6908220253054866747 / 25000000000000000000]
u : [19244738647263575017 / 25000000000000000000, 38359869536892776287 / 20000000000000000000, 4243844039318564841 / 10000000000000000000]
d : [86746708661259070569 / 100000000000000000000, -4094308139985901437 / 12500000000000000000, 86083579931934654769 / 100000000000000000000]
s : [75722497593734628719 / 50000000000000000000, 2801544496108456249 / 5000000000000000000, -35157970948673667301 / 100000000000000000000]
v : [2833709183159091311 / 4000000000000000000, 56436888216453244991 / 50000000000000000000, -9330333585913732751 / 50000000000000000000]
o : [1510547155296934499 / 20000000000000000000, 144866854034485785683 / 100000000000000000000, 48501729159222932957 / 50000000000000000000]
r : [1533749528666898321 / 2500000000000000000, 3400337093351493069 / 25000000000000000000, -3258535224095684119 / 12500000000000000000]
a : [2867934951139196427 / 20000000000000000000, 6196579447381839427 / 50000000000000000000, 138226781663611580501 / 100000000000000000000]
p : [-10749210847248334549 / 100000000000000000000, 167153101542551455427 / 100000000000000000000, 39121711592003819 / 3125000000000000000]
k : [53999906364460395009 / 100000000000000000000, -81181421264528899217 / 100000000000000000000, 247555752475049557 / 5000000000000000000]
c : [-6535828244049275889 / 100000000000000000000, -3434948958523241007 / 5000000000000000000, 83561632633195996667 / 100000000000000000000]
m : [147253321665377673381 / 100000000000000000000, 21868823351094677581 / 50000000000000000000, 6399497174199294589 / 10000000000000000000]
b : [-67742584889074582257 / 100000000000000000000, 10344640595380517191 / 100000000000000000000, 81145206489256397161 / 100000000000000000000]
j : [-5638560490793583023 / 20000000000000000000, -6219915378867147469 / 25000000000000000000, -735702437483315107 / 20000000000000000000]
l : [35775004060893904103 / 25000000000000000000, -35803537596584364409 / 100000000000000000000, 3530518925302851057 / 100000000000000000000]
f : [38440942638589885891 / 100000000000000000000, 24916247947422065751 / 25000000000000000000, 1411606692990986441 / 781250000000000000]
g : [-2723575555509030349 / 5000000000000000000, 84421635782165891657 / 100000000000000000000, 73498570902588265159 / 50000000000000000000]
Desired square lengths:
default : 1
Checking inequality 1:
d = 3
|V| = 22
|E| = 60
Success: d|V| >= |E|
Checking self-intersection:
Square collision distance = 140538558678001956618199787742854017535578240457974949644745123746661950680717879697341361303244348236727450579163483441 / 231964213044306805925075923298559370899914589138756269615222591114278030308882410000000000000000000000000000000000000000
Collision distance in [778372087342598699295324597607 / 1000000000000000000000000000000, 97296510917824837411915574701 / 125000000000000000000000000000] ~ [0.77837, 0.77837]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [3669 / 10000, 3671 / 10000] ~ [0.3669, 0.3671]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 2885818431490148581928790007168074602902747 / 50000000000000000000000000000000000000000000000000000000000000000000000000000000
rho in [75075722600613019001959577479 / 312500000000000000000000000000000000000000000000, 75075722600925519001959577479 / 312500000000000000000000000000000000000000000000] ~ [0.0, 0.0]
sigma_min ^ 2 / (16 * E ^ .5) in [1682695125000000000000000000 / 1549193338482966754071706159913, 2105662656250000000000000000 / 1936491673103708442589632699891] ~ [0.00109, 0.00109]
Success: rho < sigma_min ^ 2 / (16 * E ^ .5)
Checking inequality 4:
LHS NUM := sigma_min - [sigma_min ^ 2 - 16 * rho * |E| ^ .5 ] ^ .5 in [-1999999999999594462773227 / 10000000000000000000000000000, 200000000000040575828822293 / 1000000000000000000000000000000] ~ [-0.0002, 0.0002]
LHS DEN := 8 * |E| ^ .5 in [1936491673103708442589632699891 / 31250000000000000000000000000, 1549193338482966754071706159913 / 25000000000000000000000000000] ~ [61.96773, 61.96773]
LHS := (LHS NUM) / (LHS DEN) in [-49999999999989861569330675 / 15491933384829667540717061599128, 200000000000040575828822293 / 61967733539318670162868246396512] ~ [-0.0, 0.0]
CD / |V| ^ .5 in [778372087342598699295324597607 / 4690415759823429554565630113545, 97296510917824837411915574701 / 586301969977928694320703764193] ~ [0.16595, 0.16595]
Success: LHS < CD / |V| ^ .5
Success: existence proven