show/hide visualization coordinates
a : (-0.6878555428669302, -0.09568219957901103, -0.7218323981117234)
b : (-0.037593312887730934, 0.6479607769789322, -0.5664163253311982)
c : (0.27466575272430127, -0.21396693003721168, -0.9658846016949079)
d : (-0.37774974489428104, -0.9534407809394005, -1.1318136295923344)
e : (-1.267719780303528, -0.9092123581707121, -0.6779445045209571)
f : (-0.8850084160336966, -0.5221391906100892, 0.16092758025318177)
g : (-0.760462243360993, 0.4682505118915108, 0.1007903367898052)
h : (-0.31338982628785056, 1.3624213822168656, 0.07660958920054384)
i : (0.6341724048130218, 1.312452797725422, -0.2390309638896101)
j : (0.936437942454074, 0.5002743623289536, -0.7380316991911832)
k : (0.8349698234815192, -0.2960026662142217, -0.14167013550131657)
l : (0.41669442666675005, -1.1098791580209846, -0.5449699600782235)
m : (-0.49760823101204615, -1.3590756130166777, -0.22567107661780572)
n : (-0.9257204290234144, -1.7829393692070734, -1.0238311245418068)
o : (0.07501071968007145, -0.7501805533318373, 0.3232864295697434)
p : (-0.36913089773968466, -0.03919797131666758, 0.8684854682215053)
q : (-0.5430647380963729, 0.941813292232186, 0.9542987537258827)
r : (0.4134276591527929, 1.108276368395599, 0.7146900346049836)
s : (1.1202834194047595, 0.5825156642589848, 0.241476957667769)
t : (0.6285888727477728, -0.0756106301633458, 0.8116578529788205)
u : (0.18748837624137016, 0.5150336976872405, 1.4873572165716349)
v : (1.143563765140096, 0.6683285668915395, 1.237516199487196)
show/hide computer existence proof
(see shape-existence, preprint)
Attempting to prove existence
Starting realization:
Abstract data:
mode: maximal_simplices
data: [['t', 'o', 'k'], ['q', 'p', 'u'], ['j', 'c', 'k'], ['v', 't', 'u'], ['e', 'm', 'n'], ['j', 's', 'k'], ['j', 'c', 'b'], ['v', 'r', 'u'], ['v', 's', 'r'], ['e', 'd', 'n'], ['f', 'o', 'p'], ['s', 't', 'k'], ['n', 'd', 'm'], ['i', 'b', 'h'], ['c', 'b', 'a'], ['g', 'p', 'q'], ['s', 'v', 't'], ['j', 's', 'i'], ['m', 'd', 'l'], ['c', 'd', 'a'], ['g', 'b', 'a'], ['g', 'f', 'p'], ['f', 'o', 'm'], ['g', 'f', 'a'], ['e', 'f', 'm'], ['t', 'p', 'o'], ['p', 't', 'u'], ['i', 'r', 'h'], ['e', 'f', 'a'], ['s', 'i', 'r'], ['r', 'q', 'u'], ['o', 'l', 'k'], ['c', 'l', 'k'], ['m', 'o', 'l'], ['j', 'i', 'b'], ['g', 'b', 'h'], ['c', 'd', 'l'], ['r', 'q', 'h'], ['g', 'q', 'h'], ['e', 'd', 'a']]
Coordinate Data:
b : [3297114404074078047 / 6250000000000000000, 59700198199937989901 / 50000000000000000000, -385110490754958623 / 20000000000000000000]
d : [18738187264530239917 / 100000000000000000000, -1273117480998665323 / 3125000000000000000, -58465282879888421059 / 100000000000000000000]
s : [84270751847217140857 / 50000000000000000000, 28213971281970310717 / 25000000000000000000, 78863775846121929147 / 100000000000000000000]
o : [4000889607622842677 / 6250000000000000000, -10206868315600482581 / 50000000000000000000, 43522361518159686263 / 50000000000000000000]
m : [6752338652753725989 / 100000000000000000000, -16260648519936998587 / 20000000000000000000, 32148972417564461029 / 100000000000000000000]
i : [59965201117630261959 / 50000000000000000000, 185849598474524946843 / 100000000000000000000, 1925811480649001269 / 6250000000000000000]
n : [-7211776229676621679 / 20000000000000000000, -123689618218724570411 / 100000000000000000000, -9533406474967129011 / 20000000000000000000]
e : [-35129408138197236587 / 50000000000000000000, -2269807319693027427 / 6250000000000000000, -13078370372750687433 / 100000000000000000000]
f : [-31987679849411318107 / 100000000000000000000, 2390399640973853297 / 100000000000000000000, 1416176762093264233 / 2000000000000000000]
a : [-2454478506546934459 / 20000000000000000000, 22518049372040833443 / 50000000000000000000, -17467159731827305171 / 100000000000000000000]
h : [1573386195323330139 / 6250000000000000000, 190846456923669337191 / 100000000000000000000, 62377038999399413973 / 100000000000000000000]
p : [245000899749873431 / 1250000000000000000, 25342260785158007413 / 50000000000000000000, 28312925380299112547 / 20000000000000000000]
t : [59686024514367810411 / 50000000000000000000, 11760813921412046563 / 25000000000000000000, 135881865377227080153 / 100000000000000000000]
l : [98182604420633348761 / 100000000000000000000, -56383597100115683323 / 100000000000000000000, 219084071522681181 / 100000000000000000000]
j : [75078477999682865883 / 50000000000000000000, 104631754934878120309 / 100000000000000000000, -9543544919886641399 / 50000000000000000000]
q : [275835993040131327 / 12500000000000000000, 29757129585040275257 / 20000000000000000000, 75072977725966644607 / 50000000000000000000]
c : [41989868513194234169 / 50000000000000000000, 16603812849130798771 / 50000000000000000000, -41872380090145757783 / 100000000000000000000]
v : [85434769133983973503 / 50000000000000000000, 24287435078227344001 / 20000000000000000000, 22308462503508077959 / 12500000000000000000]
u : [75261999378095359361 / 100000000000000000000, 21221537694141361487 / 20000000000000000000, 203451801736508514939 / 100000000000000000000]
r : [97855927669237627457 / 100000000000000000000, 646218576334150991 / 390625000000000000, 31546270884960845601 / 25000000000000000000]
g : [-19533062582140961899 / 100000000000000000000, 101429369891133849721 / 100000000000000000000, 64795113758325556339 / 100000000000000000000]
k : [70005072051055125951 / 50000000000000000000, 250040520805605961 / 1000000000000000000, 10137266632303342803 / 25000000000000000000]
Desired square lengths:
default : 1
Checking inequality 1:
d = 3
|V| = 22
|E| = 60
Success: d|V| >= |E|
Checking self-intersection:
Square collision distance = 31249999999999999997900902889756546318085006498117140216654011373227722661526830826633959600514751600870252220182319849 / 62499999999999999998255688943375870191818637051529749674941840507552473964290178125000000000000000000000000000000000000
Collision distance in [707106781186547524386963102701 / 1000000000000000000000000000000, 353553390593273762193481551351 / 500000000000000000000000000000] ~ [0.70711, 0.70711]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [4421 / 10000, 4423 / 10000] ~ [0.4421, 0.4423]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 777871186447474348831980951265974380980699 / 20000000000000000000000000000000000000000000000000000000000000000000000000000000
rho in [394429001582661096498457319167 / 2000000000000000000000000000000000000000000000000, 394429001584661096498457319167 / 2000000000000000000000000000000000000000000000000] ~ [0.0, 0.0]
sigma_min ^ 2 / (16 * E ^ .5) in [2443155125000000000000000000 / 1549193338482966754071706159913, 3056707656250000000000000000 / 1936491673103708442589632699891] ~ [0.00158, 0.00158]
Success: rho < sigma_min ^ 2 / (16 * E ^ .5)
Checking inequality 4:
LHS NUM := sigma_min - [sigma_min ^ 2 - 16 * rho * |E| ^ .5 ] ^ .5 in [-24999999999996546197254373 / 125000000000000000000000000000, 100000000000013821460795283 / 500000000000000000000000000000] ~ [-0.0002, 0.0002]
LHS DEN := 8 * |E| ^ .5 in [1936491673103708442589632699891 / 31250000000000000000000000000, 1549193338482966754071706159913 / 25000000000000000000000000000] ~ [61.96773, 61.96773]
LHS := (LHS NUM) / (LHS DEN) in [-2272727272726958745204943 / 704178790219530342759866436324, 1075268817204449693126831 / 333159857738272420230474442992] ~ [-0.0, 0.0]
CD / |V| ^ .5 in [707106781186547524386963102701 / 4690415759823429554565630113545, 39283710065919306910386839039 / 260578653323523864142535006308] ~ [0.15076, 0.15076]
Success: LHS < CD / |V| ^ .5
Success: existence proven