show/hide visualization coordinates
a : (-0.37482157748104206, -0.6545891587996262, -1.0038471944834286)
b : (0.5727835015845938, -0.3364037309551292, -0.9755161578552982)
c : (0.36973772747835815, -1.311273869966251, -0.8838612306443969)
d : (-0.1408164747210061, -0.983503768964842, -0.08893911653126135)
e : (-1.0750092939139981, -0.6892872023477796, -0.2907320512349259)
f : (-1.0553546099306947, 0.07492408010635676, -0.9353984837155698)
g : (-0.14864986396065305, 0.27042840385993056, -1.3091157070664075)
h : (0.490835035670246, 0.590901497626941, -0.6102909369591509)
i : (1.2911503049605833, 0.03446896892322826, -0.38695641042747725)
j : (0.8452628780413822, -0.8282996858380491, -0.14859816979630075)
k : (0.3391455107867428, -0.5240669060220196, 0.6584257618492507)
l : (-0.65598774832607, -0.4563383510745447, 0.5868531452124528)
m : (-1.1125100064450817, 0.2511001613555628, 0.04729946023514203)
n : (-0.486081500741789, 0.7848560343859524, -0.520760391583226)
o : (0.17364083365665722, 1.261731753520412, 0.06006315304617077)
p : (0.8293759144369621, 0.5566605959451029, 0.3300375344038481)
q : (1.3066544271930272, -0.29197195647910146, 0.5581340320256628)
r : (0.750611627855997, 0.17016911189461018, 1.2489611002763528)
s : (-0.1903313188992244, -0.12830303015165612, 1.4087758410667883)
t : (-0.9522750324185117, 0.3927652335741696, 1.0241596142039695)
u : (-0.7663613690522552, 1.1302347248352314, 0.37487165094507086)
v : (-0.01099896577422177, 0.6857970945715, 0.8564345570327311)
show/hide computer existence proof
(see shape-existence, preprint)
Attempting to prove existence
Starting realization:
Abstract data:
mode: maximal_simplices
data: [['n', 'g', 'h'], ['d', 'j', 'k'], ['q', 'k', 'r'], ['n', 'f', 'm'], ['n', 'o', 'u'], ['v', 's', 'r'], ['v', 'p', 'r'], ['p', 'i', 'h'], ['n', 'f', 'g'], ['v', 'o', 'p'], ['q', 'j', 'k'], ['q', 'p', 'r'], ['v', 't', 's'], ['u', 'n', 'm'], ['b', 'i', 'h'], ['f', 'a', 'g'], ['n', 'o', 'h'], ['d', 'j', 'c'], ['b', 'g', 'h'], ['l', 't', 's'], ['u', 'o', 'v'], ['s', 'k', 'r'], ['q', 'j', 'i'], ['a', 'g', 'b'], ['q', 'p', 'i'], ['l', 'd', 'k'], ['l', 'k', 's'], ['d', 'e', 'a'], ['l', 't', 'm'], ['j', 'b', 'c'], ['d', 'a', 'c'], ['v', 't', 'u'], ['u', 't', 'm'], ['a', 'b', 'c'], ['o', 'p', 'h'], ['e', 'a', 'f'], ['e', 'f', 'm'], ['l', 'e', 'm'], ['l', 'd', 'e'], ['j', 'b', 'i']]
Coordinate Data:
e : [16735066024589079437 / 10000000000000000000, 55334463215652185429 / 50000000000000000000, 76021187842167055987 / 100000000000000000000]
n : [4338315237146794877 / 4000000000000000000, -3674539724206883123 / 10000000000000000000, 49512010938498533907 / 50000000000000000000]
t : [155077234096342164509 / 100000000000000000000, 2463682839109448307 / 100000000000000000000, -27733989350861240993 / 50000000000000000000]
i : [-17316324910391837727 / 25000000000000000000, 38293309304203583099 / 100000000000000000000, 17128724752284439437 / 20000000000000000000]
h : [672889205466648773 / 6250000000000000000, -17349943566167687583 / 100000000000000000000, 107977076414589553873 / 100000000000000000000]
q : [-35407855932405876493 / 50000000000000000000, 70937401844436559479 / 100000000000000000000, -4432710241945903507 / 50000000000000000000]
u : [136485867759716485417 / 100000000000000000000, -71283266286996725301 / 100000000000000000000, 4730408812083691973 / 50000000000000000000]
s : [4930178921525838281 / 6250000000000000000, 54570509211692016671 / 100000000000000000000, -9392960138800435997 / 10000000000000000000]
d : [4620711145411974503 / 6250000000000000000, 14009058309301060529 / 10000000000000000000, 11168378874360119921 / 20000000000000000000]
v : [60949627431913156227 / 100000000000000000000, -6709875815155897961 / 25000000000000000000, -38695472984598636467 / 100000000000000000000]
o : [42485647488825258407 / 100000000000000000000, -84432969155514789651 / 100000000000000000000, 40941667414057393309 / 100000000000000000000]
r : [-1901428991388590347 / 12500000000000000000, 24723295007065389659 / 100000000000000000000, -38974063654480399293 / 50000000000000000000]
p : [-184702884713641917 / 800000000000000000, -348146334949597049 / 2500000000000000000, 13944229278289662713 / 100000000000000000000]
a : [48665944301297590929 / 50000000000000000000, 107199122076489024541 / 100000000000000000000, 147332702167017336007 / 100000000000000000000]
k : [25935179775816696153 / 100000000000000000000, 94146896798728357903 / 100000000000000000000, -2361824183281325407 / 12500000000000000000]
c : [1143797905332758247 / 5000000000000000000, 86433796596575753589 / 50000000000000000000, 135334105783114148103 / 100000000000000000000]
m : [171100731498999156809 / 100000000000000000000, 2078773757621266233 / 12500000000000000000, 42218036695160268417 / 100000000000000000000]
b : [321422587003949747 / 12500000000000000000, 2355643102876229047 / 3125000000000000000, 1128903113314095939 / 781250000000000000]
j : [-3084569618705905677 / 12500000000000000000, 24914034956066264539 / 20000000000000000000, 30903899849152270063 / 50000000000000000000]
l : [15681063210887248419 / 12500000000000000000, 87374041303980878001 / 100000000000000000000, -11737331802570809861 / 100000000000000000000]
f : [165385191847560469767 / 100000000000000000000, 4280974773236341619 / 12500000000000000000, 70243915545115725683 / 50000000000000000000]
g : [4669669828159768091 / 6250000000000000000, 14697365810533353599 / 100000000000000000000, 177859553425315201741 / 100000000000000000000]
Desired square lengths:
default : 1
Checking inequality 1:
d = 3
|V| = 22
|E| = 60
Success: d|V| >= |E|
Checking self-intersection:
Square collision distance = 1406087256134133322383758436277386591398884953624382027264726785408705985618163948633054089673555751924737711516375401 / 2333501874824203908958137893527109448537564164432508372236795117651616061456494950000000000000000000000000000000000000
Collision distance in [776250796791918275030016886113 / 1000000000000000000000000000000, 388125398395959137515008443057 / 500000000000000000000000000000] ~ [0.77625, 0.77625]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [771 / 2000, 3857 / 10000] ~ [0.3855, 0.3857]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 1251260932290568360915575532360184898529957 / 25000000000000000000000000000000000000000000000000000000000000000000000000000000
rho in [1118597752675450515503692042761 / 5000000000000000000000000000000000000000000000000, 1118597752680450515503692042761 / 5000000000000000000000000000000000000000000000000] ~ [0.0, 0.0]
sigma_min ^ 2 / (16 * E ^ .5) in [1857628125000000000000000000 / 1549193338482966754071706159913, 2324445156250000000000000000 / 1936491673103708442589632699891] ~ [0.0012, 0.0012]
Success: rho < sigma_min ^ 2 / (16 * E ^ .5)
Checking inequality 4:
LHS NUM := sigma_min - [sigma_min ^ 2 - 16 * rho * |E| ^ .5 ] ^ .5 in [-199999999999964056537477069 / 1000000000000000000000000000000, 20000000000003596211023387 / 100000000000000000000000000000] ~ [-0.0002, 0.0002]
LHS DEN := 8 * |E| ^ .5 in [1936491673103708442589632699891 / 31250000000000000000000000000, 1549193338482966754071706159913 / 25000000000000000000000000000] ~ [61.96773, 61.96773]
LHS := (LHS NUM) / (LHS DEN) in [-199999999999964056537477069 / 61967733539318670162868246396512, 100000000000017981055116935 / 30983866769659335081434123198256] ~ [-0.0, 0.0]
CD / |V| ^ .5 in [776250796791918275030016886113 / 4690415759823429554565630113545, 388125398395959137515008443057 / 2345207879911714777282815056772] ~ [0.1655, 0.1655]
Success: LHS < CD / |V| ^ .5
Success: existence proven