show/hide visualization coordinates
a : (-0.4444199015879027, 0.9376966434577436, 0.5940183200457946)
b : (0.48667261114154725, 1.299642912733361, 0.5486131342558282)
c : (0.11270617459869897, 0.7835673749399792, -0.2219808857253261)
d : (-0.5576478898092289, 0.09823477051275725, 0.06252684640294603)
e : (-0.24172779601586036, 0.051270861392658296, 1.0101496012889546)
f : (-0.6177391116380786, 0.7912025018406126, 1.567927924629014)
g : (-0.13765644523625908, 1.6139941658486203, 1.2637330675727958)
h : (0.36367166875303775, 0.7564729050311089, 1.3791774670466566)
i : (0.5894606356376405, 0.30548498835963966, 0.5156792091158651)
j : (0.5995902266013924, -0.06910043536948768, -0.4114578636606349)
k : (-0.25440631345853204, 0.13591203629161935, -0.8896417153631804)
l : (-0.4505548454991223, -0.7464539500758882, -0.4619081306635255)
m : (0.14104856403539573, -0.5675983558313988, 0.32423185829173934)
n : (0.02580615329974323, 1.24992275729561, 2.1806474519915837)
o : (-0.850064604469434, 1.6802733782921195, 1.962361495748939)
p : (0.4982224778563748, -1.0623404512879406, -0.46801624316958573)
q : (0.4025696553499558, -0.5023147152741971, -1.2909510598767295)
r : (-0.5770109826822287, -0.6291783139488516, -1.4469234962998827)
s : (-0.16853515052539558, -1.4700626300063224, -1.091872709013976)
t : (0.7953500099795257, -1.4198235978770677, -1.353409392882832)
u : (0.08667255501446114, -1.134330026162023, -1.9985990435543424)
v : (0.1979923086542681, -2.1024728201626535, -1.7743058361800985)
show/hide computer existence proof
(see shape-existence, preprint)
Attempting to prove existence
Starting realization:
Abstract data:
mode: maximal_simplices
data: [['e', 'i', 'm'], ['n', 'g', 'h'], ['j', 'i', 'c'], ['j', 'i', 'm'], ['e', 'f', 'h'], ['n', 'f', 'h'], ['q', 'k', 'r'], ['l', 'p', 's'], ['e', 'i', 'h'], ['q', 't', 'p'], ['v', 't', 's'], ['u', 's', 'v'], ['q', 'j', 'k'], ['j', 'p', 'm'], ['o', 'f', 'g'], ['t', 'q', 'u'], ['b', 'i', 'h'], ['f', 'a', 'g'], ['q', 'j', 'p'], ['b', 'g', 'h'], ['d', 'k', 'c'], ['n', 'o', 'f'], ['n', 'o', 'g'], ['b', 'i', 'c'], ['d', 'e', 'm'], ['a', 'g', 'b'], ['l', 's', 'r'], ['j', 'k', 'c'], ['l', 'd', 'm'], ['l', 'd', 'k'], ['d', 'e', 'a'], ['u', 's', 'r'], ['l', 'p', 'm'], ['d', 'a', 'c'], ['t', 'p', 's'], ['v', 't', 'u'], ['a', 'b', 'c'], ['u', 'q', 'r'], ['e', 'a', 'f'], ['l', 'k', 'r']]
Coordinate Data:
e : [16354263604080849857 / 25000000000000000000, 44440367392789947681 / 100000000000000000000, -25814961926328649861 / 50000000000000000000]
n : [38663659484763033713 / 100000000000000000000, -3771241109875260621 / 5000000000000000000, -168679708922920208831 / 100000000000000000000]
t : [-3829072618321520411 / 10000000000000000000, 47887453329940636121 / 25000000000000000000, 23090746945565168089 / 12500000000000000000]
i : [-17701788749026689237 / 100000000000000000000, 19018954696091811743 / 100000000000000000000, -1091442317674173029 / 50000000000000000000]
h : [2438553969716792291 / 50000000000000000000, -6519959242763777627 / 25000000000000000000, -88532710428427494627 / 100000000000000000000]
q : [197461855948355817 / 20000000000000000000, 49899462529737742063 / 50000000000000000000, 22310017782988889203 / 12500000000000000000]
u : [1303080772531649733 / 4000000000000000000, 163000456148258093127 / 100000000000000000000, 249244940631672394689 / 100000000000000000000]
s : [14524447466819230371 / 25000000000000000000, 9828685826634401349 / 5000000000000000000, 158572307177635750877 / 100000000000000000000]
d : [3031533243614382643 / 3125000000000000000, 39743976480780051489 / 100000000000000000000, 43132351635943561861 / 100000000000000000000]
v : [21445043949310550733 / 100000000000000000000, 259814735548321134533 / 100000000000000000000, 226815619894248000943 / 100000000000000000000]
o : [63125367630840378683 / 50000000000000000000, -59229942148578090537 / 50000000000000000000, -73425556649327877091 / 50000000000000000000]
r : [98945373082960227899 / 100000000000000000000, 112485284926940940569 / 100000000000000000000, 48519346476556606063 / 25000000000000000000]
p : [-2144493242725030307 / 25000000000000000000, 15580149866084983539 / 10000000000000000000, 19237332118639346697 / 20000000000000000000]
a : [85686264973527627441 / 100000000000000000000, -8840442162743716687 / 20000000000000000000, -10016795728341297139 / 100000000000000000000]
k : [3334245308029527873 / 5000000000000000000, 17988124951446921219 / 50000000000000000000, 138349207812556191487 / 100000000000000000000]
c : [7493414338716864969 / 25000000000000000000, -1439464198097107193 / 5000000000000000000, 4473945303048173321 / 6250000000000000000]
m : [27139418411197787667 / 100000000000000000000, 53163644557597831477 / 50000000000000000000, 16961850447064230469 / 100000000000000000000]
b : [-1855746574854341627 / 25000000000000000000, -40198418870640161289 / 50000000000000000000, -2738138574672327677 / 50000000000000000000]
j : [-18714747845401874657 / 100000000000000000000, 28238748534502274509 / 50000000000000000000, 22632705660575415091 / 25000000000000000000]
l : [86299759364649585457 / 100000000000000000000, 62106424269822306491 / 50000000000000000000, 95575849342590715273 / 100000000000000000000]
f : [2575454649463630437 / 2500000000000000000, -3694099581500685001 / 12500000000000000000, -10740775618666324721 / 10000000000000000000]
g : [13752479834590815433 / 25000000000000000000, -6989497690800390309 / 6250000000000000000, -76988270481041417167 / 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 = 10416666666666666666503841065016165751010960224235784443283974448317232388424335279894556277598968987820934260447891107 / 20833333333333333333868117875581095433059196889783127182679787799786895993104587500000000000000000000000000000000000000
Collision distance in [707106781186547524386242283293 / 1000000000000000000000000000000, 353553390593273762193121141647 / 500000000000000000000000000000] ~ [0.70711, 0.70711]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [4267 / 10000, 4269 / 10000] ~ [0.4267, 0.4269]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 13842674697223392774257256406890493727871 / 400000000000000000000000000000000000000000000000000000000000000000000000000000
rho in [1860287255857505516756603912349 / 10000000000000000000000000000000000000000000000000, 1860287255867505516756603912349 / 10000000000000000000000000000000000000000000000000] ~ [0.0, 0.0]
sigma_min ^ 2 / (16 * E ^ .5) in [2275911125000000000000000000 / 1549193338482966754071706159913, 316395156250000000000000000 / 215165741455967604732181411099] ~ [0.00147, 0.00147]
Success: rho < sigma_min ^ 2 / (16 * E ^ .5)
Checking inequality 4:
LHS NUM := sigma_min - [sigma_min ^ 2 - 16 * rho * |E| ^ .5 ] ^ .5 in [-99999999999986498268332447 / 500000000000000000000000000000, 200000000000027016120219871 / 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 [-99999999999986498268332447 / 30983866769659335081434123198256, 200000000000027016120219871 / 61967733539318670162868246396512] ~ [-0.0, 0.0]
CD / |V| ^ .5 in [707106781186547524386242283293 / 4690415759823429554565630113545, 117851130197757920731040380549 / 781735959970571592427605018924] ~ [0.15076, 0.15076]
Success: LHS < CD / |V| ^ .5
Success: existence proven