show/hide visualization coordinates
a : (-0.8199709968076245, 0.030977972754304806, -0.9101742735886056)
b : (-0.17322857836839023, 0.7670868696203161, -1.1098438409895348)
c : (-0.11862452832167214, -0.09622411627864424, -1.6115534575454271)
d : (-0.8041190298121288, -0.8073093913068684, -1.455172448262378)
e : (-0.7676004496925601, -0.8589943473843821, -0.4571769279210711)
f : (-1.1703215922423398, -0.0779482368719191, 0.020088883337973096)
g : (-0.6204831060445992, 0.7231100568403989, -0.21651891275185753)
h : (0.3631854377450011, 0.8932077762030803, -0.2753658483259511)
i : (0.4604099593573498, 0.05385134869511665, -0.8101818727664296)
j : (0.07931467058417108, -0.8532514554122504, -0.9888740204826596)
k : (0.06748980294072987, -1.251389084587215, -0.07162454474546764)
l : (-0.21646281530863154, -0.32792517462900284, 0.1864167651140644)
m : (-0.6455762645902934, 0.3950871742792897, 0.7278175325421391)
n : (-0.15830786315448375, 1.239313105574112, 0.5045417347234311)
o : (0.7964021681311572, 0.9663515871638289, 0.6229510486717993)
p : (0.8734030737057348, 0.11855402875688087, 0.09825098149064038)
q : (0.8742781199462742, -0.7539229197790024, -0.39040350643266775)
r : (0.6163532063351242, -0.7219308386396682, 0.5752316450003437)
s : (-0.05123697535049421, -0.27579980724581077, 1.1712941015805378)
t : (0.11269887452760047, 0.7018285139447543, 1.303081440619097)
u : (0.8765677045584375, 0.08996316943945515, 1.0978371698081146)
v : (0.4258291818616366, 0.045363768863222576, 1.9893783509239094)
show/hide computer existence proof
(see shape-existence, preprint)
Attempting to prove existence
Starting realization:
Abstract data:
mode: maximal_simplices
data: [['q', 'i', 'j'], ['t', 'v', 's'], ['a', 'c', 'b'], ['d', 'j', 'e'], ['r', 'u', 's'], ['h', 'o', 'n'], ['d', 'a', 'c'], ['h', 'o', 'p'], ['r', 's', 'l'], ['u', 't', 'o'], ['g', 'h', 'n'], ['u', 'o', 'p'], ['u', 'v', 's'], ['q', 'j', 'k'], ['a', 'g', 'b'], ['i', 'h', 'b'], ['g', 'h', 'b'], ['m', 't', 's'], ['f', 'm', 'l'], ['e', 'a', 'f'], ['i', 'c', 'j'], ['q', 'k', 'r'], ['r', 'u', 'p'], ['t', 'u', 'v'], ['i', 'h', 'p'], ['r', 'q', 'p'], ['g', 'm', 'n'], ['f', 'm', 'g'], ['q', 'i', 'p'], ['r', 'k', 'l'], ['m', 's', 'l'], ['m', 't', 'n'], ['i', 'c', 'b'], ['t', 'o', 'n'], ['e', 'k', 'l'], ['d', 'a', 'e'], ['a', 'f', 'g'], ['e', 'j', 'k'], ['e', 'f', 'l'], ['d', 'j', 'c']]
Coordinate Data:
k : [42140212153498451083 / 100000000000000000000, 185524097914929714573 / 100000000000000000000, 33815145194805968693 / 50000000000000000000]
c : [30375822639869325041 / 50000000000000000000, 4375475067754539261 / 6250000000000000000, 54107222087306611 / 24414062500000000]
f : [33184270334361082911 / 20000000000000000000, 68180013143400104481 / 100000000000000000000, 58458947581267865073 / 100000000000000000000]
v : [6306274261407779117 / 100000000000000000000, 11169762513977187793 / 20000000000000000000, -69234999588662884779 / 50000000000000000000]
a : [5235451685133355387 / 4000000000000000000, 57287392180777723977 / 100000000000000000000, 151485263273925735489 / 100000000000000000000]
m : [113446818906600782171 / 100000000000000000000, 20876472028279229957 / 100000000000000000000, -2462783467829746831 / 20000000000000000000]
e : [125649237416827450619 / 100000000000000000000, 36571156048661599239 / 25000000000000000000, 21237105741434457387 / 20000000000000000000]
j : [10239431347288582233 / 25000000000000000000, 145710334997433247907 / 100000000000000000000, 3187104759266622579 / 2000000000000000000]
p : [-19225557461501023467 / 50000000000000000000, 24264893290260056927 / 50000000000000000000, 50642737766001137459 / 100000000000000000000]
i : [2848196511836458253 / 100000000000000000000, 13750013646674132551 / 25000000000000000000, 28297204638341624757 / 20000000000000000000]
o : [-30751024365544277653 / 100000000000000000000, -7249993852034935633 / 20000000000000000000, -365453790422951211 / 20000000000000000000]
l : [22571351673099071 / 32000000000000000, 23294426729777119647 / 25000000000000000000, 41826159403658728301 / 100000000000000000000]
r : [-6373064092970495357 / 50000000000000000000, 132578273320175018531 / 100000000000000000000, 588934283006159827 / 20000000000000000000]
d : [129301095428784327849 / 100000000000000000000, 70558064293447519527 / 50000000000000000000, 205985080741302987667 / 100000000000000000000]
u : [-605743406379254793 / 1562500000000000000, 1605902266008208813 / 3125000000000000000, -7705606416522859 / 15625000000000000]
h : [12570648673071326467 / 100000000000000000000, -14467794082049920761 / 50000000000000000000, 44002210373830141707 / 50000000000000000000]
b : [66212050284410456437 / 100000000000000000000, -8161748752911707641 / 50000000000000000000, 85726110007009326041 / 50000000000000000000]
q : [-38538619547055987809 / 100000000000000000000, 67888740717054223967 / 50000000000000000000, 99508186558331950369 / 100000000000000000000]
s : [843951405978450933 / 1562500000000000000, 1759303403615785569 / 2000000000000000000, -14165393560747155261 / 25000000000000000000]
n : [32359989381509905363 / 50000000000000000000, -15886530275300750553 / 25000000000000000000, 5006831221361028691 / 50000000000000000000]
g : [110937503052031362551 / 100000000000000000000, -11925816227831690571 / 100000000000000000000, 82119727190250924759 / 100000000000000000000]
t : [37619304994811394457 / 100000000000000000000, -489883096913361497 / 5000000000000000000, -69840308146844532193 / 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 = 714285714285714285690099678398792700149904812759749244284303573380756024934542034626577371129131477350366523522137567 / 1428571428571428571411796839836625672958399685020884343678294875616937036061074100000000000000000000000000000000000000
Collision distance in [35355339059327376219651219201 / 50000000000000000000000000000, 707106781186547524393024384021 / 1000000000000000000000000000000] ~ [0.70711, 0.70711]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [5269 / 10000, 5271 / 10000] ~ [0.5269, 0.5271]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 4188542758728953632114912935611634326795511 / 100000000000000000000000000000000000000000000000000000000000000000000000000000000
rho in [2046592963617571326696074101583 / 10000000000000000000000000000000000000000000000000, 2046592963627571326696074101583 / 10000000000000000000000000000000000000000000000000] ~ [0.0, 0.0]
sigma_min ^ 2 / (16 * E ^ .5) in [3470295125000000000000000000 / 1549193338482966754071706159913, 482351406250000000000000000 / 215165741455967604732181411099] ~ [0.00224, 0.00224]
Success: rho < sigma_min ^ 2 / (16 * E ^ .5)
Checking inequality 4:
LHS NUM := sigma_min - [sigma_min ^ 2 - 16 * rho * |E| ^ .5 ] ^ .5 in [-199999999999975939531885241 / 1000000000000000000000000000000, 50000000000006017400238827 / 250000000000000000000000000000] ~ [-0.0002, 0.0002]
LHS DEN := 8 * |E| ^ .5 in [1936491673103708442589632699891 / 31250000000000000000000000000, 1549193338482966754071706159913 / 25000000000000000000000000000] ~ [61.96773, 61.96773]
LHS := (LHS NUM) / (LHS DEN) in [-199999999999975939531885241 / 61967733539318670162868246396512, 50000000000006017400238827 / 15491933384829667540717061599128] ~ [-0.0, 0.0]
CD / |V| ^ .5 in [141421356237309504878604876804 / 938083151964685910913126022709, 707106781186547524393024384021 / 4690415759823429554565630113544] ~ [0.15076, 0.15076]
Success: LHS < CD / |V| ^ .5
Success: existence proven