show/hide visualization coordinates
a : (-0.44058534345384615, 0.03953055978461528, -0.33189701755384615)
b : (-0.5318114270538462, 0.5083345305846153, 0.5466817429461538)
c : (-0.2539144060538461, 1.0197715674846153, -0.26646363315384614)
d : (0.40629065044615387, 0.4135689333846153, -0.7099133481538461)
e : (0.12052362294615387, -0.5151091453153847, -0.9463329584538461)
f : (-0.18980309695384612, -0.8936117165153847, -0.07430478775384619)
g : (-0.9065305799538462, -0.4113577442153847, 0.4294142025461538)
h : (0.05243318994615387, -0.29116015501538467, 0.6862040532461539)
i : (0.43186857674615386, 0.5409079511846153, 0.28161604844615384)
j : (-0.01511317775384613, 1.3590195455846152, 0.6434181077461538)
k : (0.6495693386461538, -0.3514819101153847, -0.11366450195384614)
l : (1.084711861946154, -0.25742450051538474, -1.0090996967538461)
m : (-0.40763920945384613, -1.1609879163153847, 0.8643417888461538)
show/hide computer existence proof
(see shape-existence, preprint)
Attempting to prove existence
Starting realization:
Abstract data:
mode: maximal_simplices
data: [['d', 'l', 'e'], ['c', 'a', 'd'], ['h', 'g', 'b'], ['k', 'f', 'e'], ['m', 'f', 'g'], ['i', 'h', 'k'], ['a', 'g', 'b'], ['a', 'f', 'g'], ['c', 'j', 'i'], ['k', 'l', 'e'], ['i', 'h', 'b'], ['k', 'd', 'l'], ['a', 'f', 'e'], ['k', 'h', 'f'], ['k', 'd', 'i'], ['c', 'j', 'b'], ['c', 'd', 'i'], ['i', 'j', 'b'], ['a', 'd', 'e'], ['c', 'a', 'b'], ['m', 'h', 'g'], ['m', 'h', 'f']]
Coordinate Data:
g : [3623491247 / 2500000000, 1755940503 / 2000000000, 155291861 / 2000000000]
i : [1109973421 / 10000000000, -742954439 / 10000000000, 1127220423 / 5000000000]
f : [3663345079 / 5000000000, 6801121119 / 5000000000, 726706151 / 1250000000]
m : [9505051283 / 10000000000, 4069001059 / 2500000000, -1786408279 / 5000000000]
e : [4223422959 / 10000000000, 4908608263 / 5000000000, 2906786183 / 2000000000]
c : [7967803249 / 10000000000, -2765795301 / 5000000000, 3867618831 / 5000000000]
l : [-5418459431 / 10000000000, 3620185039 / 5000000000, 7580799149 / 5000000000]
j : [2789895483 / 5000000000, -8924070383 / 10000000000, -1363579747 / 10000000000]
a : [9834512623 / 10000000000, 170832779 / 400000000, 4194785753 / 5000000000]
d : [341438171 / 2500000000, 530435739 / 10000000000, 3042433703 / 2500000000]
b : [10746773459 / 10000000000, -417220233 / 10000000000, -396216099 / 10000000000]
k : [-533517099 / 5000000000, 4090472087 / 5000000000, 124144927 / 200000000]
h : [4904327289 / 10000000000, 7577726623 / 10000000000, -895719601 / 5000000000]
Desired square lengths:
default : 1
Checking inequality 1:
d = 3
|V| = 13
|E| = 33
Success: d|V| >= |E|
Checking self-intersection:
Square collision distance = 19999999992536855801882620290573753353499243274829165891089 / 39999999998783207124686816057056644154952000000000000000000
Collision distance in [35355339 / 50000000, 70710679 / 100000000] ~ [0.70711, 0.70711]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [8813 / 10000, 1763 / 2000] ~ [0.8813, 0.8815]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 9258357297484970841873 / 10000000000000000000000000000000000000000
rho in [48110179 / 50000000000000000, 548110179 / 50000000000000000] ~ [0.0, 0.0]
sigma_min ^ 2 / (16 * E ^ .5) in [77668969 / 9191300240, 1807075 / 213751168] ~ [0.00845, 0.00845]
Success: rho < sigma_min ^ 2 / (16 * E ^ .5)
Checking inequality 4:
LHS NUM := sigma_min - [sigma_min ^ 2 - 16 * rho * |E| ^ .5 ] ^ .5 in [-3999 / 20000000, 10029 / 50000000] ~ [-0.0002, 0.0002]
LHS DEN := 8 * |E| ^ .5 in [71807033 / 1562500, 114891253 / 2500000] ~ [45.9565, 45.9565]
LHS := (LHS NUM) / (LHS DEN) in [-465 / 106875584, 10029 / 2297825056] ~ [-0.0, 0.0]
CD / |V| ^ .5 in [35355339 / 180277564, 70710679 / 360555127] ~ [0.19612, 0.19612]
Success: LHS < CD / |V| ^ .5
Success: existence proven