show/hide visualization coordinates
a : (0.22824901117692314, -0.5315983065692308, -0.20343514496153842)
b : (-0.6160795553230769, -0.050938288169230794, -0.44023720806153843)
c : (0.2029440549769232, 0.07135067003076917, -1.0008134641615385)
d : (0.7965847330769231, 0.29087219913076917, -0.2266035144615384)
e : (1.0141010023769232, -0.4494398724692308, 0.40949766863846154)
f : (0.10873143447692318, -0.6534784480692308, 0.7818875308384616)
g : (-0.6474689563230769, -0.8514759694692309, 0.15822259223846163)
h : (-0.5496552797230768, 0.0629254693307692, 0.5510361468384617)
i : (-0.09461873842307683, 0.7121492750307692, -0.05843099216153841)
j : (-0.4946194303230768, 0.7872884529307691, -0.9718605442615385)
k : (0.4670012031769231, 1.0199637041307692, -0.8264370565615384)
l : (0.4119653513769232, 0.2956007194307692, 0.6964596334384616)
m : (-0.8271348305230768, -0.7032196052692308, 1.1307143526384615)
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', 'g', 'f'], ['m', 'h', 'f'], ['b', 'j', 'c'], ['b', 'g', 'a'], ['g', 'a', 'f'], ['d', 'a', 'e'], ['b', 'h', 'g'], ['b', 'i', 'j'], ['i', 'h', 'l'], ['e', 'a', 'f'], ['m', 'h', 'g'], ['e', 'l', 'f'], ['k', 'd', 'c'], ['b', 'i', 'h'], ['d', 'a', 'c'], ['i', 'd', 'l'], ['d', 'l', 'e'], ['i', 'k', 'j'], ['i', 'k', 'd'], ['j', 'k', 'c'], ['h', 'l', 'f']]
Coordinate Data:
k : [1907918329 / 2000000000, 3492342479 / 2500000000, -3785295309 / 10000000000]
m : [-850442173 / 2500000000, -1631231589 / 5000000000, 15786218783 / 10000000000]
b : [-64560797 / 500000000, 3260349993 / 10000000000, 9587897 / 1250000000]
f : [2978446979 / 5000000000, -1382525803 / 5000000000, 2459590113 / 2000000000]
e : [15010589637 / 10000000000, -14493317 / 200000000, 8574051943 / 10000000000]
c : [6899020163 / 10000000000, 179329583 / 400000000, -1105811877 / 2000000000]
a : [286082789 / 400000000, -1546250191 / 10000000000, 2444723807 / 10000000000]
h : [-1224557 / 19531250, 274936723 / 625000000, 399577469 / 400000000]
g : [-32102199 / 200000000, -237251341 / 500000000, 6061301179 / 10000000000]
l : [8989233127 / 10000000000, 6725740069 / 10000000000, 11443671591 / 10000000000]
j : [-7661469 / 1000000000, 2910654351 / 2500000000, -2619765093 / 5000000000]
d : [100276773 / 78125000, 3339227433 / 5000000000, 138315007 / 625000000]
i : [3923392229 / 10000000000, 17425961 / 16000000, 778953067 / 2000000000]
Desired square lengths:
default : 1
Checking inequality 1:
d = 3
|V| = 13
|E| = 33
Success: d|V| >= |E|
Checking self-intersection:
Square collision distance = 30517578112631433507889015206573615040388989441621581969 / 61035156487492336494745298418770630342187500000000000000
Collision distance in [70710677 / 100000000, 35355339 / 50000000] ~ [0.70711, 0.70711]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [7347 / 10000, 7349 / 10000] ~ [0.7347, 0.7349]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 561166939915382443287131 / 1250000000000000000000000000000000000000
rho in [211880521 / 10000000000000000, 311880521 / 10000000000000000] ~ [0.0, 0.0]
sigma_min ^ 2 / (16 * E ^ .5) in [53978409 / 9191300240, 54007801 / 9191300224] ~ [0.00587, 0.00588]
Success: rho < sigma_min ^ 2 / (16 * E ^ .5)
Checking inequality 4:
LHS NUM := sigma_min - [sigma_min ^ 2 - 16 * rho * |E| ^ .5 ] ^ .5 in [-4967 / 25000000, 5049 / 25000000] ~ [-0.0002, 0.0002]
LHS DEN := 8 * |E| ^ .5 in [71807033 / 1562500, 114891253 / 2500000] ~ [45.9565, 45.9565]
LHS := (LHS NUM) / (LHS DEN) in [-4967 / 1148912528, 5049 / 1148912528] ~ [-0.0, 0.0]
CD / |V| ^ .5 in [70710677 / 360555128, 70710678 / 360555127] ~ [0.19612, 0.19612]
Success: LHS < CD / |V| ^ .5
Success: existence proven