show/hide visualization coordinates
a : (0.5208692239713756, -0.3778748268722478, -0.7248519095890102)
b : (-0.4135304116264959, -0.16785709613649769, -1.012584204910844)
c : (0.3000910409987964, 0.5290625015644286, -1.0836299415411779)
d : (0.9548996387453983, 0.43375884104209605, -0.3338680375955501)
e : (1.3638069528678785, -0.46810619725198266, -0.19446121868069405)
f : (0.7118485825050154, -1.2255334962925442, -0.22987548108893302)
g : (-0.21332949034559606, -1.036191578931501, -0.5588058260656052)
h : (-1.1480029967717977, -0.8255210506502271, -0.8451681226387371)
i : (-1.1420693643943174, 0.05075838752240441, -0.3634014381921406)
j : (-0.6234856992272333, 0.7863127056306422, -0.7993266924894789)
k : (0.16162150593435165, 1.033974510161856, -0.2316381273591706)
l : (0.9167424511054365, 1.0876645737453754, 0.4217451715063)
m : (1.3261575150860412, 0.18600621292232367, 0.5609985583363697)
n : (0.6341372706848449, -0.5320015131464271, 0.486346789137707)
o : (-0.059366372754558916, -1.2479943074049045, 0.40630295673189387)
p : (-0.9015520657727163, -0.7890467137003487, 0.1233005455967165)
q : (-1.2140062573553339, 0.012391974331768862, 0.6332695716049742)
r : (-0.6951406696152349, 0.7477551145962132, 0.19735724808161137)
s : (-0.019921471170085137, 1.2636522343213499, 0.7245471530593126)
t : (0.38897688469938596, 0.36155268404074314, 0.8624548611497984)
u : (-0.30050419307635207, -0.35983058793227884, 0.797477801300158)
v : (-0.548242074488803, 0.5370676284397558, 1.1638103436464986)
show/hide computer existence proof
(see shape-existence, preprint)
Attempting to prove existence
Starting realization:
Abstract data:
mode: maximal_simplices
data: [['n', 'e', 'f'], ['n', 't', 'm'], ['n', 'e', 'm'], ['o', 'p', 'g'], ['j', 'r', 'i'], ['n', 'o', 'u'], ['u', 'q', 'p'], ['v', 's', 'r'], ['n', 't', 'u'], ['p', 'i', 'h'], ['v', 't', 's'], ['o', 'f', 'g'], ['b', 'i', 'h'], ['f', 'a', 'g'], ['b', 'g', 'h'], ['d', 'k', 'c'], ['l', 't', 's'], ['q', 'r', 'i'], ['n', 'o', 'f'], ['s', 'k', 'r'], ['d', 'e', 'm'], ['a', 'g', 'b'], ['j', 'k', 'c'], ['q', 'p', 'i'], ['l', 'd', 'm'], ['l', 'd', 'k'], ['p', 'g', 'h'], ['l', 'k', 's'], ['u', 'q', 'v'], ['d', 'e', 'a'], ['l', 't', 'm'], ['j', 'b', 'c'], ['j', 'k', 'r'], ['d', 'a', 'c'], ['v', 'q', 'r'], ['v', 't', 'u'], ['a', 'b', 'c'], ['u', 'o', 'p'], ['e', 'a', 'f'], ['j', 'b', 'i']]
Coordinate Data:
e : [-25543233225891951621 / 25000000000000000000, 99565592755465879189 / 100000000000000000000, 67388189725082767701 / 100000000000000000000]
n : [-29205964685264456853 / 100000000000000000000, 52977562172455164411 / 50000000000000000000, -138522211351467653 / 20000000000000000000]
t : [-4689926086718562741 / 100000000000000000000, 13279763700954643 / 80000000000000000, -1915170912898323393 / 5000000000000000000]
i : [37103674705662943879 / 25000000000000000000, 47679134278027173243 / 100000000000000000000, 10535276459528428763 / 12500000000000000000]
h : [29801612412079959543 / 20000000000000000000, 13530707809529031889 / 10000000000000000000, 26491776024177411809 / 20000000000000000000]
q : [2431381064355522139 / 1562500000000000000, 1609867987409085181 / 3125000000000000000, -769244465174202971 / 5000000000000000000]
u : [2008068177839226329 / 3125000000000000000, 88738031823495496037 / 100000000000000000000, -496964254265663093 / 1562500000000000000]
d : [-612822014913198021 / 1000000000000000000, 4689544463029006601 / 50000000000000000000, 81328871616568372089 / 100000000000000000000]
s : [36199909500228552039 / 100000000000000000000, -73610250401867357523 / 100000000000000000000, -24512647448917891731 / 100000000000000000000]
v : [8903196983210034541 / 10000000000000000000, -951789813707957281 / 100000000000000000000, -8554870813454563059 / 12500000000000000000]
o : [20072199829337963737 / 50000000000000000000, 88777201885379033103 / 50000000000000000000, 7311772183823979917 / 100000000000000000000]
r : [103721829344743529269 / 100000000000000000000, -22020538429353704703 / 100000000000000000000, 28206343048852226153 / 100000000000000000000]
p : [24872593792098332801 / 20000000000000000000, 32914911100075620851 / 25000000000000000000, 3561201329734171477 / 10000000000000000000]
a : [-17879160013917521383 / 100000000000000000000, 11317806964686549203 / 12500000000000000000, 24085451763182876727 / 20000000000000000000]
k : [9022805894892436149 / 50000000000000000000, -25321238992958988147 / 50000000000000000000, 71105880592930431273 / 100000000000000000000]
c : [1049664570835098481 / 25000000000000000000, -151277126175238513 / 100000000000000000000, 6252202480445246129 / 4000000000000000000]
m : [-98407989125384078309 / 100000000000000000000, 34154351738035250837 / 100000000000000000000, -815778797662360561 / 10000000000000000000]
b : [75560803545869627963 / 100000000000000000000, 34770341321958692249 / 50000000000000000000, 74600244174048877881 / 50000000000000000000]
j : [96556332305943354499 / 100000000000000000000, -5175259506559320347 / 20000000000000000000, 25574947421192247763 / 20000000000000000000]
l : [-14366620681830905839 / 25000000000000000000, -14002871086067479209 / 25000000000000000000, 5767550706383365489 / 100000000000000000000]
f : [-18488547933640752221 / 50000000000000000000, 43827080664880509763 / 25000000000000000000, 70929615965906664907 / 100000000000000000000]
g : [13885177854444910087 / 25000000000000000000, 78187065461708859 / 50000000000000000, 103822650463573884559 / 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 = 8789012240703946948301845862924038590282927258062993580300741226957683809666475697211913193973958419105071221872061169 / 14634375624979583334652418978744258541759084223888774521287049037385619694227192031250000000000000000000000000000000000
Collision distance in [774966511219385275661121907949 / 1000000000000000000000000000000, 15499330224387705513222438159 / 20000000000000000000000000000] ~ [0.77497, 0.77497]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [2247 / 5000, 281 / 625] ~ [0.4494, 0.4496]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 2160674847709536467604876629092003761372703 / 50000000000000000000000000000000000000000000000000000000000000000000000000000000
rho in [259848203747732330966992979139 / 1250000000000000000000000000000000000000000000000, 259848203748982330966992979139 / 1250000000000000000000000000000000000000000000000] ~ [0.0, 0.0]
sigma_min ^ 2 / (16 * E ^ .5) in [360643500000000000000000000 / 221313334068995250581672308559, 3158440000000000000000000000 / 1936491673103708442589632699891] ~ [0.00163, 0.00163]
Success: rho < sigma_min ^ 2 / (16 * E ^ .5)
Checking inequality 4:
LHS NUM := sigma_min - [sigma_min ^ 2 - 16 * rho * |E| ^ .5 ] ^ .5 in [-12499999999998209274438333 / 62500000000000000000000000000, 200000000000028664360036649 / 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 [-1388888888888689919382037 / 430331482911935209464362822198, 6451612903226731108388279 / 1998959146429634521382846657952] ~ [-0.0, 0.0]
CD / |V| ^ .5 in [774966511219385275661121907949 / 4690415759823429554565630113545, 43053695067743626425617883775 / 260578653323523864142535006308] ~ [0.16522, 0.16522]
Success: LHS < CD / |V| ^ .5
Success: existence proven