show/hide visualization coordinates
a : (-0.7725533038086678, -0.30552101725332953, -0.22230165365213306)
b : (-0.05184812475790734, -0.16222245941930463, -0.9005711931510701)
c : (-0.004338989576435637, -0.9432917468346349, -0.27793674957216163)
d : (-0.5932196756582857, -0.9391388045548099, 0.5302725615782297)
e : (-0.6780705217294507, 0.0407133648426915, 0.7110764886595229)
f : (-0.6218442810827367, 0.6702740242582264, -0.06383769109138016)
g : (-0.9089412906536414, 0.3487459599544126, -0.9661652430150075)
h : (-0.11184163249626033, 0.6393054293847494, -1.4955113771179658)
i : (0.6608809991059973, 0.5384980869325618, -0.868823564632827)
j : (0.6396821907469892, -0.18476417753659674, -0.17857556042049827)
k : (0.597828140305733, -0.8998096668354909, 0.5192483333341981)
l : (0.026838427577039026, -1.7065926354195586, 0.36735366732948727)
m : (0.01997445168279377, -1.2494304067166941, 1.2567105037468798)
n : (-0.7220580504611473, -0.612806865660817, 1.4667062959320518)
o : (0.16296596859360563, -0.26468042110701256, 1.1576100903608753)
p : (0.1965415236046501, 0.4624560590859752, 0.47193872499824535)
q : (0.22601882739387003, 1.1736273326610402, -0.23046180760614976)
r : (-0.5467038042083876, 1.2744346751132278, -0.857149620091289)
s : (0.3840401429593696, 1.4479683297396568, -1.1790219170082157)
t : (1.0640888028161255, 0.6957192012050011, 0.032677954087018346)
u : (1.032560199646747, -0.023484261839292975, 0.7267617573321902)
show/hide computer existence proof
(see shape-existence, preprint)
Attempting to prove existence
Starting realization:
Abstract data:
mode: maximal_simplices
data: [['n', 'o', 'm'], ['t', 'j', 'i'], ['g', 'b', 'h'], ['q', 's', 'i'], ['g', 'f', 'r'], ['a', 'b', 'c'], ['b', 'j', 'i'], ['b', 'j', 'c'], ['a', 'd', 'c'], ['t', 'p', 'u'], ['k', 'o', 'm'], ['o', 'p', 'e'], ['k', 'j', 'u'], ['k', 'l', 'm'], ['g', 'a', 'b'], ['d', 'n', 'm'], ['h', 's', 'i'], ['k', 'o', 'u'], ['l', 'd', 'c'], ['a', 'e', 'd'], ['a', 'f', 'e'], ['b', 'h', 'i'], ['f', 'p', 'e'], ['p', 'o', 'u'], ['g', 'h', 'r'], ['h', 'r', 's'], ['d', 'n', 'e'], ['q', 'p', 'f'], ['t', 'j', 'u'], ['k', 'j', 'c'], ['g', 'a', 'f'], ['q', 't', 'i'], ['q', 'r', 's'], ['d', 'l', 'm'], ['t', 'p', 'q'], ['o', 'n', 'e'], ['l', 'k', 'c'], ['q', 'f', 'r']]
Coordinate Data:
g : [146827739403954065873 / 100000000000000000000, 2170534008017056177 / 20000000000000000000, 7635600591023741153 / 5000000000000000000]
s : [17529596042652960663 / 100000000000000000000, -99069566938439143693 / 100000000000000000000, 173997679219795646251 / 100000000000000000000]
l : [53249767580886021779 / 100000000000000000000, 21638652957748242553 / 10000000000000000000, 3872024157205070277 / 20000000000000000000]
o : [39637013479229358837 / 100000000000000000000, 36097654073113901609 / 50000000000000000000, -11933104303422687729 / 20000000000000000000]
e : [12374066251153498873 / 10000000000000000000, 20827964775628696969 / 50000000000000000000, -15012161346978207547 / 100000000000000000000]
j : [-50216304600681241 / 625000000000000000, 32101841894593110077 / 50000000000000000000, 7395304356102390031 / 10000000000000000000]
c : [56367509296233487989 / 100000000000000000000, 14005644071899003377 / 10000000000000000000, 83889162476190237029 / 100000000000000000000]
u : [-11830602406521194841 / 25000000000000000000, 9615138443891168187 / 20000000000000000000, -414517205356123663 / 2500000000000000000]
d : [115255577904418487237 / 100000000000000000000, 69820573245503770227 / 50000000000000000000, 613646272230220563 / 20000000000000000000]
k : [-3849203691983374317 / 100000000000000000000, 135708232719075647487 / 100000000000000000000, 4170654185554271483 / 100000000000000000000]
r : [110603990759428690629 / 100000000000000000000, -81716201475796245259 / 100000000000000000000, 141810449528102968539 / 100000000000000000000]
f : [944944307574908723 / 800000000000000000, -4260027278059218633 / 20000000000000000000, 15619814157028021621 / 25000000000000000000]
q : [16665863799601461261 / 50000000000000000000, -1790886680764437277 / 2500000000000000000, 79141668279589052159 / 100000000000000000000]
i : [-5077244786004905317 / 50000000000000000000, -812254265772964681 / 10000000000000000000, 142977843982256762287 / 100000000000000000000]
p : [7255891595624982957 / 20000000000000000000, -51833987307097913 / 10000000000000000000, 8901615019149540639 / 100000000000000000000]
a : [133188940719456699543 / 100000000000000000000, 3051174710434379837 / 4000000000000000000, 39162826442093688967 / 50000000000000000000]
n : [128139415384704661183 / 100000000000000000000, 107007952601608245811 / 100000000000000000000, -45287571037115551409 / 50000000000000000000]
t : [-5047526994302262393 / 10000000000000000000, -23844654084973572389 / 100000000000000000000, 6603461513784030469 / 12500000000000000000]
m : [26968082585155272463 / 50000000000000000000, 85335153353597978147 / 50000000000000000000, -69575562855713910751 / 100000000000000000000]
h : [2097430424631748671 / 3125000000000000000, -18203276902948400989 / 100000000000000000000, 41129325046154135733 / 20000000000000000000]
b : [15279605703595165621 / 25000000000000000000, 30974755988728504903 / 50000000000000000000, 73076303417040539259 / 50000000000000000000]
Desired square lengths:
default : 1
Checking inequality 1:
d = 3
|V| = 21
|E| = 57
Success: d|V| >= |E|
Checking self-intersection:
Square collision distance = 127309947184280824014548113086828600397582504072797656595595912449553045407795021688359795134721234105546323248181451529 / 249907664615343693098302277763710882706070186278102659640806147235899742653207735000000000000000000000000000000000000000
Collision distance in [713742209510482960919244183257 / 1000000000000000000000000000000, 356871104755241480459622091629 / 500000000000000000000000000000] ~ [0.71374, 0.71374]
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 = 830424831303258966207483738524172991229831 / 25000000000000000000000000000000000000000000000000000000000000000000000000000000
rho in [1822552969110372897430382660557 / 10000000000000000000000000000000000000000000000000, 1822552969120372897430382660557 / 10000000000000000000000000000000000000000000000000] ~ [0.0, 0.0]
sigma_min ^ 2 / (16 * E ^ .5) in [7469280625000000000000000000 / 7549834435270749697236684806947, 1246320937500000000000000000 / 1258305739211791616206114134491] ~ [0.00099, 0.00099]
Success: rho < sigma_min ^ 2 / (16 * E ^ .5)
Checking inequality 4:
LHS NUM := sigma_min - [sigma_min ^ 2 - 16 * rho * |E| ^ .5 ] ^ .5 in [-49999999999992043958851521 / 250000000000000000000000000000, 100000000000015921288014313 / 500000000000000000000000000000] ~ [-0.0002, 0.0002]
LHS DEN := 8 * |E| ^ .5 in [3774917217635374848618342403473 / 62500000000000000000000000000, 7549834435270749697236684806947 / 125000000000000000000000000000] ~ [60.39868, 60.39868]
LHS := (LHS NUM) / (LHS DEN) in [-16666666666664014652950507 / 5033222956847166464824456537964, 100000000000015921288014313 / 30199337741082998788946739227784] ~ [-0.0, 0.0]
CD / |V| ^ .5 in [713742209510482960919244183257 / 4582575694955840006588047193729, 356871104755241480459622091629 / 2291287847477920003294023596864] ~ [0.15575, 0.15575]
Success: LHS < CD / |V| ^ .5
Success: existence proven