show/hide visualization coordinates
a : (-0.836772391975, 0.33678229935625, 0.40488881161874996)
b : (-0.3279838352750001, 0.5619575273562499, 1.23581011281875)
c : (0.07116179012499996, 0.7506102621562499, 0.33854034891874996)
d : (-0.5619157462750001, 0.8075710444562499, -0.4334496614812501)
e : (-0.6790111954750001, -0.18554971674374998, -0.43313320758125007)
f : (-1.2377027541749999, -0.57330384184375, 0.30001776711874995)
g : (-0.655127317375, -0.37127202284375005, 1.08728460881875)
h : (0.26790641302499996, -0.11360066344375008, 0.80160282021875)
i : (0.707583503725, 0.09725270225624999, -0.07145454238125004)
j : (0.42159296212499997, 0.90623885965625, -0.5850253972812501)
k : (-0.10432541097500003, 0.24993192995624997, -1.1260170765812503)
l : (0.28968649042499994, -0.42425164934375004, -0.50132883798125)
m : (-0.25801181677500007, -0.76990761294375, 0.26061110621874994)
n : (0.739444632925, -0.83362899194375, 0.29247930721874993)
o : (1.2748845547249998, -0.5949069977437501, -0.5176487148812501)
p : (0.8885901212249999, 0.15607687165624995, -1.0531774447812499)
show/hide computer existence proof
(see shape-existence, preprint)
Attempting to prove existence
Starting realization:
Abstract data:
mode: maximal_simplices
data: [['c', 'j', 'i'], ['k', 'p', 'l'], ['o', 'n', 'i'], ['c', 'h', 'i'], ['d', 'a', 'e'], ['a', 'g', 'b'], ['m', 'n', 'l'], ['o', 'n', 'l'], ['a', 'c', 'b'], ['a', 'f', 'g'], ['m', 'h', 'n'], ['p', 'o', 'i'], ['f', 'e', 'm'], ['p', 'j', 'k'], ['d', 'j', 'k'], ['h', 'n', 'i'], ['m', 'g', 'h'], ['d', 'a', 'c'], ['b', 'g', 'h'], ['d', 'e', 'k'], ['k', 'e', 'l'], ['a', 'e', 'f'], ['e', 'm', 'l'], ['d', 'c', 'j'], ['p', 'j', 'i'], ['b', 'h', 'c'], ['p', 'o', 'l'], ['f', 'm', 'g']]
Coordinate Data:
n : [-2513436257 / 10000000000, 14083234071 / 10000000000, 1810191029 / 10000000000]
j : [665080451 / 10000000000, -663088889 / 2000000000, 5292619037 / 5000000000]
p : [-200244557 / 500000000, 837235087 / 2000000000, 15266758549 / 10000000000]
k : [2962132091 / 5000000000, 811906213 / 2500000000, 15995154867 / 10000000000]
o : [-314713419 / 400000000, 11696014129 / 10000000000, 7929177 / 8000000]
e : [11671122027 / 10000000000, 7602441319 / 10000000000, 9066316177 / 10000000000]
g : [5716141623 / 5000000000, 472983219 / 500000000, -6137861987 / 10000000000]
b : [326433937 / 400000000, 63684439 / 5000000000, -7623117027 / 10000000000]
l : [124009073 / 625000000, 1997892129 / 2000000000, 9748272481 / 10000000000]
m : [93264103 / 125000000, 13446020281 / 10000000000, 2128873039 / 10000000000]
d : [2100033507 / 2000000000, -2328766293 / 10000000000, 2267370179 / 2500000000]
c : [4169392171 / 10000000000, -175915847 / 1000000000, 337395153 / 2500000000]
a : [1656091749 / 1250000000, 1189560579 / 5000000000, 137219197 / 2000000000]
i : [-438964993 / 2000000000, 4774417129 / 10000000000, 217981181 / 400000000]
h : [1100972971 / 5000000000, 3441475393 / 5000000000, -3281044101 / 10000000000]
f : [8629018807 / 5000000000, 1147998257 / 1000000000, 173480643 / 1000000000]
Desired square lengths:
default : 1
Checking inequality 1:
d = 3
|V| = 16
|E| = 42
Success: d|V| >= |E|
Checking self-intersection:
Square collision distance = 3738827787423108791144211203232749902950155491448718152049 / 9660381303761349232306310017401526796900000000000000000000
Collision distance in [62211489 / 100000000, 6221149 / 10000000] ~ [0.62211, 0.62211]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [3703 / 10000, 741 / 2000] ~ [0.3703, 0.3705]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 5032636287460519609321094041861 / 10000000000000000000000000000000000000000
rho in [11216769 / 500000000000, 11221769 / 500000000000] ~ [2e-05, 2e-05]
sigma_min ^ 2 / (16 * E ^ .5) in [1958887 / 1481312160, 13727025 / 10369185104] ~ [0.00132, 0.00132]
Success: rho < sigma_min ^ 2 / (16 * E ^ .5)
Checking inequality 4:
LHS NUM := sigma_min - [sigma_min ^ 2 - 16 * rho * |E| ^ .5 ] ^ .5 in [59053 / 20000000, 335579 / 100000000] ~ [0.00295, 0.00336]
LHS DEN := 8 * |E| ^ .5 in [648074069 / 12500000, 64807407 / 1250000] ~ [51.84593, 51.84593]
LHS := (LHS NUM) / (LHS DEN) in [59053 / 1036918512, 335579 / 5184592552] ~ [6e-05, 6e-05]
CD / |V| ^ .5 in [62211489 / 400000001, 6221149 / 40000000] ~ [0.15553, 0.15553]
Success: LHS < CD / |V| ^ .5
Success: existence proven