show/hide visualization coordinates
a : (0.5072441947, -0.3855883908923077, 0.1774770606307693)
b : (0.0778128777, 0.40109394920769237, 0.6210079379307692)
c : (0.2956341749, -0.4162804896923077, 1.1543492082307694)
d : (-0.0408827464, -1.1359256869923078, 0.5470048635307693)
e : (0.27112585180000004, -1.1651589322923077, -0.40262456606923075)
f : (0.05697593820000002, -0.23560137449230767, -0.7027288196692307)
g : (0.5443738559, 0.5147388467076923, -0.25614979696923074)
h : (-0.18598233530000002, 1.1450564893076924, 0.007060199030769265)
i : (-0.5902528315, 0.23728800610769235, -0.10484040786923071)
j : (-0.6011876155, -0.32617047859230763, 0.7212316019307693)
k : (-0.6153716161, -0.7595780259923076, -0.1798548045692307)
l : (-0.20016633560000002, 0.7116489416076923, -0.8940262080692307)
m : (0.4806765872, 1.4144771460076924, -0.6879062680692307)
show/hide computer existence proof
(see shape-existence, preprint)
Attempting to prove existence
Starting realization:
Abstract data:
mode: maximal_simplices
data: [['b', 'a', 'c'], ['b', 'j', 'c'], ['i', 'l', 'f'], ['b', 'g', 'a'], ['g', 'a', 'f'], ['d', 'a', 'e'], ['b', 'h', 'g'], ['b', 'i', 'j'], ['i', 'h', 'l'], ['e', 'a', 'f'], ['m', 'h', 'g'], ['k', 'e', 'f'], ['j', 'd', 'c'], ['b', 'i', 'h'], ['d', 'a', 'c'], ['m', 'h', 'l'], ['l', 'm', 'g'], ['j', 'd', 'k'], ['i', 'k', 'j'], ['k', 'd', 'e'], ['g', 'l', 'f'], ['i', 'k', 'f']]
Coordinate Data:
k : [5044435879 / 5000000000, 160183623 / 125000000, 1697301667 / 2500000000]
e : [1223897079 / 10000000000, 16870498903 / 10000000000, 9016904283 / 10000000000]
b : [157851341 / 500000000, 150996261 / 1250000000, -1219420757 / 10000000000]
f : [673079243 / 2000000000, 302996933 / 400000000, 12017946819 / 10000000000]
m : [-34864411 / 400000000, -223146547 / 250000000, 11869721303 / 10000000000]
c : [122351731 / 1250000000, 9381714477 / 10000000000, -327641673 / 500000000]
a : [-22745727 / 200000000, 9074793489 / 10000000000, 200993001 / 625000000]
h : [115899579 / 200000000, -6231655313 / 10000000000, 615007079 / 1250000000]
g : [-754291481 / 5000000000, 71521113 / 10000000000, 472009787 / 625000000]
l : [5936818953 / 10000000000, -474394959 / 2500000000, 13930920703 / 10000000000]
j : [1243378969 / 1250000000, 4240307183 / 5000000000, -2221657397 / 10000000000]
d : [4343983061 / 10000000000, 331563329 / 200000000, -479390013 / 10000000000]
i : [1229710489 / 1250000000, 2846029519 / 10000000000, 6039062701 / 10000000000]
Desired square lengths:
default : 1
Checking inequality 1:
d = 3
|V| = 13
|E| = 33
Success: d|V| >= |E|
Checking self-intersection:
Square collision distance = 868055554377219177721114195172568009632764131616868073321 / 1736111112729247604854815961803774359187500000000000000000
Collision distance in [35355339 / 50000000, 70710679 / 100000000] ~ [0.70711, 0.70711]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [7371 / 10000, 7373 / 10000] ~ [0.7371, 0.7373]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 22979226084265085928529 / 500000000000000000000000000000000000000
rho in [338963317 / 50000000000000000, 838963317 / 50000000000000000] ~ [0.0, 0.0]
sigma_min ^ 2 / (16 * E ^ .5) in [54331641 / 9191300240, 54361129 / 9191300224] ~ [0.00591, 0.00591]
Success: rho < sigma_min ^ 2 / (16 * E ^ .5)
Checking inequality 4:
LHS NUM := sigma_min - [sigma_min ^ 2 - 16 * rho * |E| ^ .5 ] ^ .5 in [-9979 / 50000000, 4021 / 20000000] ~ [-0.0002, 0.0002]
LHS DEN := 8 * |E| ^ .5 in [71807033 / 1562500, 114891253 / 2500000] ~ [45.9565, 45.9565]
LHS := (LHS NUM) / (LHS DEN) in [-9979 / 2297825056, 20105 / 4595650112] ~ [-0.0, 0.0]
CD / |V| ^ .5 in [35355339 / 180277564, 70710679 / 360555127] ~ [0.19612, 0.19612]
Success: LHS < CD / |V| ^ .5
Success: existence proven