show/hide visualization coordinates
a : (-0.19204836412129378, -1.5172243799897722, 0.5671568479918635)
b : (-0.2200819913872505, -0.570271269475305, 0.8873035678396364)
c : (-0.25839544985518825, -0.7682811314217178, -0.09214738727357807)
d : (0.548446781264504, -1.359016302592933, -0.08601781770366257)
e : (0.32499044939392074, -2.290672702745146, 0.20048457286640609)
f : (0.15577524714807378, -2.223486179943928, 1.1837709942527581)
g : (0.2922781933159392, -1.2573051297979703, 1.4025428480784883)
h : (0.7422822321936917, -0.7396992521962781, 0.674820015905488)
i : (0.35065746853412816, 0.16891381427370322, 0.5297257709175892)
j : (-0.6088399660659862, 0.10107125976262521, 0.25629925283053406)
k : (-0.16186203159667756, 0.06435366881916343, -0.6374918550984155)
l : (0.6482172216527566, -0.3780741480152068, -0.2527461854073687)
m : (0.9150253860832762, -1.719907482383657, 0.7715238330856048)
n : (0.6096738565354636, 0.6185597725598251, -0.3251011255612808)
o : (-0.1412003030782074, 0.9844270107648461, 0.22474354380698158)
p : (-0.8471214162861322, 0.7680191752712041, -0.44967697090490133)
q : (-0.03652596458939639, 0.9913388315413441, -0.9910302241619141)
r : (0.41320481481136895, 1.5990042063003567, -0.33644255365583997)
s : (-0.5787098830410031, 1.7187110654172337, -0.294305870530447)
t : (-0.9103694120540529, 1.4333747213365886, -1.1935194867315886)
u : (-0.0778459563143089, 1.9822917498252774, -1.1187211479913297)
v : (-0.9675509125436272, 2.393872702689749, -0.9211706225550248)
show/hide computer existence proof
(see shape-existence, preprint)
Attempting to prove existence
Starting realization:
Abstract data:
mode: maximal_simplices
data: [['q', 'p', 'k'], ['l', 'i', 'h'], ['h', 'g', 'm'], ['o', 'j', 'i'], ['q', 't', 'p'], ['o', 'j', 'p'], ['n', 'o', 'r'], ['u', 's', 'v'], ['t', 'q', 'u'], ['v', 't', 's'], ['b', 'i', 'h'], ['n', 'l', 'k'], ['f', 'a', 'g'], ['b', 'g', 'h'], ['l', 'd', 'h'], ['l', 'k', 'c'], ['d', 'm', 'h'], ['o', 'p', 's'], ['d', 'e', 'm'], ['a', 'g', 'b'], ['l', 'i', 'n'], ['j', 'k', 'c'], ['n', 'o', 'i'], ['s', 'o', 'r'], ['l', 'd', 'c'], ['n', 'q', 'k'], ['d', 'e', 'a'], ['n', 'q', 'r'], ['u', 's', 'r'], ['j', 'b', 'c'], ['d', 'a', 'c'], ['t', 'p', 's'], ['v', 't', 'u'], ['a', 'b', 'c'], ['f', 'g', 'm'], ['e', 'f', 'm'], ['u', 'q', 'r'], ['e', 'a', 'f'], ['k', 'j', 'p'], ['j', 'b', 'i']]
Coordinate Data:
e : [17332015563703639689 / 100000000000000000000, 284178553567780175027 / 100000000000000000000, 1630884981454854237 / 5000000000000000000]
n : [-2227265030090128771 / 20000000000000000000, -1348938792543378939 / 20000000000000000000, 17035253894373154899 / 20000000000000000000]
t : [140868001708501010713 / 100000000000000000000, -4411309442019662441 / 5000000000000000000, 172018105588896531167 / 100000000000000000000]
i : [14765313649682900153 / 100000000000000000000, 477748773323691127 / 1250000000000000000, -306420176021231187 / 100000000000000000000]
h : [-6099290679068363479 / 25000000000000000000, 129081208512893416877 / 100000000000000000000, -1481584467481111373 / 10000000000000000000]
q : [26741828481017677791 / 50000000000000000000, -44022599860868794303 / 100000000000000000000, 151769179331929115057 / 100000000000000000000]
u : [57615656134526601099 / 100000000000000000000, -8944868230578882233 / 6250000000000000000, 164538271714870648073 / 100000000000000000000]
s : [107702048807196019243 / 100000000000000000000, -116759823248457750737 / 100000000000000000000, 82096743968782389571 / 100000000000000000000]
d : [-501361762335467683 / 10000000000000000000, 191012913552558916597 / 100000000000000000000, 30633969343051973127 / 50000000000000000000]
v : [146586151757458431461 / 100000000000000000000, -18427598697570931341 / 10000000000000000000, 4524475599101255343 / 3125000000000000000]
o : [31975545405458227299 / 50000000000000000000, -21665708891609495399 / 50000000000000000000, 30191802535039534107 / 100000000000000000000]
r : [8510579021958820341 / 100000000000000000000, -26197284334192516767 / 25000000000000000000, 86310412281321696213 / 100000000000000000000]
p : [16817900266463616253 / 12500000000000000000, -21690634233854803479 / 100000000000000000000, 97633854006227828597 / 100000000000000000000]
a : [69035896915225087093 / 100000000000000000000, 41366744258448568299 / 20000000000000000000, -2024763941724326473 / 50000000000000000000]
k : [8252157957845433659 / 12500000000000000000, 24337958205674633803 / 50000000000000000000, 116415342425579239777 / 100000000000000000000]
c : [75670605488614537321 / 100000000000000000000, 65969698217718701139 / 50000000000000000000, 309404478215477527 / 500000000000000000]
m : [-41671478105231910207 / 100000000000000000000, 22710203153163132197 / 10000000000000000000, -24486226392822781727 / 100000000000000000000]
b : [17959814910455192003 / 25000000000000000000, 112138410240796106421 / 100000000000000000000, -36064199868225943043 / 100000000000000000000]
j : [22143011421938866627 / 20000000000000000000, 45004157317003092461 / 100000000000000000000, 3379528954085536263 / 12500000000000000000]
l : [-14990661662179947907 / 100000000000000000000, 18583739618957257447 / 20000000000000000000, 19485193864118640479 / 25000000000000000000]
f : [17126767894144167661 / 50000000000000000000, 277459901287658420437 / 100000000000000000000, -16427735627384528741 / 25000000000000000000]
g : [2060324117150179927 / 10000000000000000000, 90420898136531308987 / 50000000000000000000, -43794063946055560043 / 50000000000000000000]
Desired square lengths:
default : 1
Checking inequality 1:
d = 3
|V| = 22
|E| = 60
Success: d|V| >= |E|
Checking self-intersection:
Square collision distance = 124999999999999999997416621560245590864007138903595219523339558744876465774675965193343616636822897111875755874191000321 / 250000000000000000006058565956738010572662472812238042063105817963998432323646422500000000000000000000000000000000000000
Collision distance in [707106781186547524384969358307 / 1000000000000000000000000000000, 176776695296636881096242339577 / 250000000000000000000000000000] ~ [0.70711, 0.70711]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [4553 / 10000, 911 / 2000] ~ [0.4553, 0.4555]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 3999868967862883405778667951131937567968659 / 100000000000000000000000000000000000000000000000000000000000000000000000000000000
rho in [999983620848722127430616182589 / 5000000000000000000000000000000000000000000000000, 999983620853722127430616182589 / 5000000000000000000000000000000000000000000000000] ~ [0.0, 0.0]
sigma_min ^ 2 / (16 * E ^ .5) in [2591226125000000000000000000 / 1549193338482966754071706159913, 3241878906250000000000000000 / 1936491673103708442589632699891] ~ [0.00167, 0.00167]
Success: rho < sigma_min ^ 2 / (16 * E ^ .5)
Checking inequality 4:
LHS NUM := sigma_min - [sigma_min ^ 2 - 16 * rho * |E| ^ .5 ] ^ .5 in [-199999999999972791781093113 / 1000000000000000000000000000000, 40000000000005444034136679 / 200000000000000000000000000000] ~ [-0.0002, 0.0002]
LHS DEN := 8 * |E| ^ .5 in [1936491673103708442589632699891 / 31250000000000000000000000000, 1549193338482966754071706159913 / 25000000000000000000000000000] ~ [61.96773, 61.96773]
LHS := (LHS NUM) / (LHS DEN) in [-66666666666657597260364371 / 20655911179772890054289415465504, 66666666666675740056894465 / 20655911179772890054289415465504] ~ [-0.0, 0.0]
CD / |V| ^ .5 in [707106781186547524384969358307 / 4690415759823429554565630113545, 176776695296636881096242339577 / 1172603939955857388641407528386] ~ [0.15076, 0.15076]
Success: LHS < CD / |V| ^ .5
Success: existence proven