show/hide visualization coordinates
a : (-0.24370614563846152, -0.5921245058846154, -0.1373458932538461)
b : (0.2648501985615385, -0.35647704038461536, 0.690809112746154)
c : (-0.7324365742384615, -0.2838472967846154, 0.678808329846154)
d : (-0.7618082252384615, 0.26294622681538465, -0.15794381625384613)
e : (-0.5150171028384615, -0.19286624838461539, -1.0131216599538462)
f : (0.44458125696153844, -0.4153981666846154, -0.8409283294538461)
g : (0.6925343137615385, -0.9214293469846153, -0.01482195605384612)
h : (0.7936266074615383, 0.07309751281538462, -0.04121631045384616)
i : (0.028381603861538485, 0.5629167987153847, 0.3764883030461538)
j : (-0.19762019123846153, 0.2795873584153847, 1.3085009674461539)
k : (-0.8964811430384615, 0.7012375642153847, 0.7307428093461539)
l : (0.09476565696153855, 0.4947477152153846, -0.6189744640538462)
m : (1.0283297446615385, 0.3876094289153846, -0.960997092953846)
show/hide computer existence proof
(see shape-existence, preprint)
Attempting to prove existence
Starting realization:
Abstract data:
mode: maximal_simplices
data: [['b', 'a', 'c'], ['m', 'l', 'f'], ['m', 'h', 'f'], ['b', 'j', 'c'], ['b', 'g', 'a'], ['g', 'a', 'f'], ['d', 'a', 'e'], ['b', 'h', 'g'], ['h', 'g', 'f'], ['b', 'i', 'j'], ['i', 'h', 'l'], ['e', 'a', 'f'], ['e', 'l', 'f'], ['k', 'd', 'c'], ['b', 'i', 'h'], ['d', 'a', 'c'], ['m', 'h', 'l'], ['i', 'd', 'l'], ['d', 'l', 'e'], ['i', 'k', 'j'], ['i', 'k', 'd'], ['j', 'k', 'c']]
Coordinate Data:
k : [-807519193 / 2000000000, 2853021639 / 2500000000, 11269667251 / 10000000000]
m : [950657057 / 625000000, 8275805203 / 10000000000, -1411932943 / 2500000000]
b : [7575717451 / 10000000000, 83494051 / 1000000000, 2174066057 / 2000000000]
f : [1874605607 / 2000000000, 245729247 / 10000000000, -4447044137 / 10000000000]
e : [-222955563 / 10000000000, 247104843 / 1000000000, -3084488721 / 5000000000]
c : [-2397150277 / 10000000000, 780618973 / 5000000000, 1343790307 / 1250000000]
a : [2490154009 / 10000000000, -304306829 / 2000000000, 103551209 / 400000000]
h : [643174077 / 500000000, 2565343021 / 5000000000, 3550076053 / 10000000000]
g : [11852558603 / 10000000000, -1203645639 / 2500000000, 3814019597 / 10000000000]
l : [1174974407 / 2000000000, 4673594033 / 5000000000, -2227505483 / 10000000000]
j : [2951013553 / 10000000000, 3597792249 / 5000000000, 266363263 / 156250000]
d : [-2690866787 / 10000000000, 3514586591 / 5000000000, 476560199 / 2000000000]
i : [325689469 / 625000000, 10028878901 / 10000000000, 1931780547 / 2500000000]
Desired square lengths:
default : 1
Checking inequality 1:
d = 3
|V| = 13
|E| = 33
Success: d|V| >= |E|
Checking self-intersection:
Square collision distance = 408163265144768273288480618906149894123031162624834558329 / 816326537812861020393196246075099173924000000000000000000
Collision distance in [70710677 / 100000000, 35355339 / 50000000] ~ [0.70711, 0.70711]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [3599 / 5000, 18 / 25] ~ [0.7198, 0.72]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 6857895479100752952002171 / 2500000000000000000000000000000000000000
rho in [523751677 / 10000000000000000, 623751677 / 10000000000000000] ~ [0.0, 0.0]
sigma_min ^ 2 / (16 * E ^ .5) in [12952801 / 2297825060, 405000 / 71807033] ~ [0.00564, 0.00564]
Success: rho < sigma_min ^ 2 / (16 * E ^ .5)
Checking inequality 4:
LHS NUM := sigma_min - [sigma_min ^ 2 - 16 * rho * |E| ^ .5 ] ^ .5 in [-9833 / 50000000, 20399 / 100000000] ~ [-0.0002, 0.0002]
LHS DEN := 8 * |E| ^ .5 in [71807033 / 1562500, 114891253 / 2500000] ~ [45.9565, 45.9565]
LHS := (LHS NUM) / (LHS DEN) in [-9833 / 2297825056, 20399 / 4595650112] ~ [-0.0, 0.0]
CD / |V| ^ .5 in [70710677 / 360555128, 70710678 / 360555127] ~ [0.19612, 0.19612]
Success: LHS < CD / |V| ^ .5
Success: existence proven