show/hide visualization coordinates
a : (0.5043389137076923, -0.33219893691538455, -0.35805346523846154)
b : (0.1640929479076923, -0.9145842601153846, 0.3802283357615384)
c : (-0.3664195919923077, -0.8129410783153845, -0.4613327781384616)
d : (-0.3012610906923077, 0.15829788938461548, -0.6903507651384617)
e : (0.6085401041076923, 0.5583810055846155, -0.8007830399384617)
f : (1.0252674366076924, 0.39250554598461546, 0.09298631686153846)
g : (1.0945464858076923, -0.5502517540153846, 0.41919037656153846)
h : (0.32215135530769234, 0.020069437684615443, 0.6987248092615385)
i : (-0.5711900043923077, -0.23859561081538455, 0.3312556159615384)
j : (-1.1873221042923077, -0.24189420061538452, -0.4563803127384615)
k : (-0.9060754632923076, 0.6251911203846154, -0.04520714893846156)
l : (0.08536173680769232, 0.7288440094846155, 0.03421801336153846)
m : (-0.4720307255923077, 0.6071768322846154, 0.8555040423615384)
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', 'g', 'a'], ['g', 'a', 'f'], ['d', 'a', 'e'], ['b', 'h', 'g'], ['h', 'g', 'f'], ['m', 'i', 'k'], ['m', 'i', 'h'], ['m', 'k', 'l'], ['e', 'a', 'f'], ['k', 'd', 'l'], ['j', 'd', 'c'], ['e', 'l', 'f'], ['b', 'i', 'h'], ['b', 'i', 'c'], ['d', 'a', 'c'], ['m', 'h', 'l'], ['j', 'd', 'k'], ['d', 'l', 'e'], ['i', 'k', 'j'], ['h', 'l', 'f'], ['i', 'j', 'c']]
Coordinate Data:
k : [1736274303 / 1250000000, -527244477 / 2500000000, 294095217 / 625000000]
e : [-1004769 / 8000000, -36021919 / 250000000, 6130641191 / 5000000000]
b : [398563789 / 1250000000, 13288775897 / 10000000000, 3609349 / 80000000]
f : [-216929383 / 400000000, 54469459 / 2500000000, 1661794407 / 5000000000]
m : [9549747047 / 10000000000, -1928835027 / 10000000000, -4301588441 / 10000000000]
c : [8493635711 / 10000000000, 12272344079 / 10000000000, 2216694941 / 2500000000]
a : [-106974673 / 5000000000, 1492984533 / 2000000000, 1566797327 / 2000000000]
h : [803963119 / 5000000000, 3942238919 / 10000000000, -273379611 / 1000000000]
g : [-6116025067 / 10000000000, 2411362709 / 2500000000, 61548217 / 10000000000]
l : [3975822423 / 10000000000, -3145506799 / 10000000000, 3911271849 / 10000000000]
j : [8351330417 / 5000000000, 3280937651 / 5000000000, 881725511 / 1000000000]
d : [3921025349 / 5000000000, 1279977201 / 5000000000, 5578479817 / 5000000000]
i : [2108267967 / 2000000000, 1632222351 / 2500000000, 940895823 / 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 = 137434603688741887479514017667932392162252506134263664513121 / 245305501176315920099907870669647330687500000000000000000000
Collision distance in [74850447 / 100000000, 4678153 / 6250000] ~ [0.7485, 0.7485]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [191 / 250, 3821 / 5000] ~ [0.764, 0.7642]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 97182749811328421404407 / 2000000000000000000000000000000000000000
rho in [348537569 / 50000000000000000, 848537569 / 50000000000000000] ~ [0.0, 0.0]
sigma_min ^ 2 / (16 * E ^ .5) in [729620 / 114891253, 14600041 / 2297825056] ~ [0.00635, 0.00635]
Success: rho < sigma_min ^ 2 / (16 * E ^ .5)
Checking inequality 4:
LHS NUM := sigma_min - [sigma_min ^ 2 - 16 * rho * |E| ^ .5 ] ^ .5 in [-19959 / 100000000, 20103 / 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 [-19959 / 4595650112, 20103 / 4595650112] ~ [-0.0, 0.0]
CD / |V| ^ .5 in [74850447 / 360555128, 74850448 / 360555127] ~ [0.2076, 0.2076]
Success: LHS < CD / |V| ^ .5
Success: existence proven