show/hide visualization coordinates
a : (0.14612115021598865, 0.24872925523226197, 1.0403190735366543)
b : (0.2915236119374095, 0.7461040856146246, 0.1850551363643526)
c : (-0.6369506329623892, 0.5976722225067239, 0.5255012533521454)
d : (-0.7839818274602449, 0.03386726759852199, 1.3382163329867578)
e : (-0.2411011569399898, -0.6550318536088877, 0.8579054145441962)
f : (0.7377117995326458, -0.5575057366563942, 1.0379438903027605)
g : (1.0619322740915147, 0.30172974555525933, 0.6422224352547319)
h : (0.9839116868147096, 0.2666267731943008, -0.3541111280123139)
i : (0.4337587594773341, 0.9880019322991096, -0.7747649481169555)
j : (-0.4794593466645448, 0.7395964828061685, -0.45176738887408807)
k : (-1.3847782256497871, 0.46762742445695976, -0.12553042184927476)
l : (-1.0763236764350599, -0.29663296419101526, 0.44082798888758856)
m : (-0.4131718764916459, -0.7955759057691356, -0.11710178382684788)
n : (0.42205734465994404, -1.1539625993539648, 0.299972701122594)
o : (1.2143010197414812, -0.5603073894541286, 0.15882224574932607)
p : (1.7178656648020643, -0.36294537454630593, 0.9999351295625116)
q : (0.47765171502499176, -0.5802001787110964, -0.5171600608211125)
r : (0.5447218756500646, 0.10904496202036695, -1.2385772282989818)
s : (-0.2585129129720588, 0.6748168709539103, -1.4248995871528432)
t : (-1.158570308609185, 0.38849847142644967, -1.0963901372873228)
u : (-1.2467842843243466, -0.4342548992813331, -0.5348786187255868)
v : (-0.35192265343889617, -0.1658985920923981, -0.8915402986982882)
show/hide computer existence proof
(see shape-existence, preprint)
Attempting to prove existence
Starting realization:
Abstract data:
mode: maximal_simplices
data: [['l', 'u', 'm'], ['e', 'm', 'n'], ['j', 'i', 'b'], ['c', 'b', 'a'], ['v', 'q', 'r'], ['i', 's', 'j'], ['g', 'b', 'h'], ['e', 'f', 'a'], ['e', 'f', 'n'], ['i', 'b', 'h'], ['m', 'v', 'q'], ['e', 'l', 'm'], ['f', 'g', 'a'], ['o', 'g', 'h'], ['s', 'v', 'r'], ['f', 'o', 'p'], ['r', 'q', 'h'], ['g', 'b', 'a'], ['m', 'u', 'v'], ['k', 'j', 'c'], ['f', 'o', 'n'], ['t', 'j', 'k'], ['t', 'u', 'v'], ['i', 'r', 'h'], ['l', 'k', 'c'], ['o', 'q', 'h'], ['e', 'l', 'd'], ['j', 'b', 'c'], ['o', 'q', 'n'], ['t', 's', 'j'], ['o', 'p', 'g'], ['i', 's', 'r'], ['t', 'u', 'k'], ['e', 'd', 'a'], ['c', 'd', 'a'], ['f', 'g', 'p'], ['m', 'n', 'q'], ['l', 'd', 'c'], ['l', 'u', 'k'], ['t', 'v', 's']]
Coordinate Data:
b : [23269918887001760099 / 100000000000000000000, -20702537369514866017 / 100000000000000000000, 4231807863286234947 / 12500000000000000000]
m : [5858716733119206341 / 6250000000000000000, 667327308844305831 / 500000000000000000, 64070154925409933041 / 100000000000000000000]
i : [2261601033252324947 / 25000000000000000000, -359138576303706937 / 800000000000000000, 64918235677210340773 / 50000000000000000000]
c : [58058671688490818579 / 50000000000000000000, -2929675529362396323 / 50000000000000000000, -190148792489402249 / 100000000000000000000]
u : [177100708513177386733 / 100000000000000000000, 97333361120080911213 / 100000000000000000000, 21169567683056765381 / 20000000000000000000]
p : [-119364286399463733759 / 100000000000000000000, 22550602161644547689 / 25000000000000000000, -47633536413526021373 / 100000000000000000000]
f : [-2668612484065232683 / 12500000000000000000, 54829222428793511143 / 50000000000000000000, -12858603121887726087 / 25000000000000000000]
r : [-512476871065936799 / 25000000000000000000, 10750843747477725843 / 25000000000000000000, 1376700776348619679 / 781250000000000000]
o : [-6900782189340541931 / 10000000000000000000, 54969305068680224393 / 50000000000000000000, 1823887598389626559 / 5000000000000000000]
e : [38266197887370845397 / 50000000000000000000, 14926382069104545973 / 12500000000000000000, -6686112982338898121 / 20000000000000000000]
s : [15654714275589717601 / 20000000000000000000, -2714763180688686493 / 20000000000000000000, 194849935258009468403 / 100000000000000000000]
h : [-1436527768772757821 / 3125000000000000000, 6811298468129379893 / 25000000000000000000, 87771089343956527747 / 100000000000000000000]
l : [8002732386212434127 / 5000000000000000000, 83571167611049120797 / 100000000000000000000, 2069294413491571337 / 25000000000000000000]
v : [10951818178079041449 / 12500000000000000000, 35248865200593702481 / 50000000000000000000, 141514006412553952971 / 100000000000000000000]
g : [-13442736832102190177 / 25000000000000000000, 23734896636421663351 / 100000000000000000000, -1186226698274804527 / 10000000000000000000]
q : [186284343129741457 / 4000000000000000000, 111927889063057242511 / 100000000000000000000, 52037991312418193377 / 50000000000000000000]
a : [37810165059143844227 / 100000000000000000000, 7258736417180350687 / 25000000000000000000, -51671930810940282453 / 100000000000000000000]
n : [10216545614748308253 / 100000000000000000000, 169304131127344078531 / 100000000000000000000, 11181353215232869181 / 50000000000000000000]
k : [23862512830715177661 / 12500000000000000000, 357256437312581119 / 5000000000000000000, 1298260374553052299 / 2000000000000000000]
d : [130820462826767205687 / 100000000000000000000, 50521144432095399563 / 100000000000000000000, -81461656755950627139 / 100000000000000000000]
j : [100368214747197203679 / 100000000000000000000, -1002588854433462599 / 5000000000000000000, 48768357715066972593 / 50000000000000000000]
t : [168279310941661214557 / 100000000000000000000, 15058024049302631269 / 100000000000000000000, 161998990271457408923 / 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 = 555555555555555555544029491021704913348955496410127604807699906520345462339927270405625728486816293578519888026472801 / 1111111111111111111105740269921628766075161589392995037601401551822935659276765000000000000000000000000000000000000000
Collision distance in [707106781186547524395218210753 / 1000000000000000000000000000000, 353553390593273762197609105377 / 500000000000000000000000000000] ~ [0.70711, 0.70711]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [1529 / 5000, 153 / 500] ~ [0.3058, 0.306]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 1312634815270569725897459302662139909581847 / 25000000000000000000000000000000000000000000000000000000000000000000000000000000
rho in [1145702760435956061460217489193 / 5000000000000000000000000000000000000000000000000, 1145702760440956061460217489193 / 5000000000000000000000000000000000000000000000000] ~ [0.0, 0.0]
sigma_min ^ 2 / (16 * E ^ .5) in [1168920500000000000000000000 / 1549193338482966754071706159913, 162562500000000000000000000 / 215165741455967604732181411099] ~ [0.00075, 0.00076]
Success: rho < sigma_min ^ 2 / (16 * E ^ .5)
Checking inequality 4:
LHS NUM := sigma_min - [sigma_min ^ 2 - 16 * rho * |E| ^ .5 ] ^ .5 in [-49999999999988399247814713 / 250000000000000000000000000000, 200000000000046433357340921 / 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 [-16666666666662799749271571 / 5163977794943222513572353866376, 200000000000046433357340921 / 61967733539318670162868246396512] ~ [-0.0, 0.0]
CD / |V| ^ .5 in [707106781186547524395218210753 / 4690415759823429554565630113545, 39283710065919306910845456153 / 260578653323523864142535006308] ~ [0.15076, 0.15076]
Success: LHS < CD / |V| ^ .5
Success: existence proven