show/hide visualization coordinates
a : (0.29788111885, 0.7414868087416667, 0.646580441425)
b : (0.47562833905, 0.26805020924166667, -0.21612675787500002)
c : (-0.45950575325, 0.34149009384166673, 0.130472164125)
d : (0.017103462849999973, -0.20225691805833335, 0.821256386625)
e : (0.5826263914500001, 0.28275810614166674, 1.488297797125)
f : (0.97259238625, 0.004283245241666733, 0.610585842825)
g : (0.48179924195, -0.6869993212583332, 0.08025528312500002)
h : (-0.03354790485000003, -0.4194516795583333, -0.7338918642750001)
i : (-0.26374359704999994, 0.5491371402416667, -0.827943133275)
j : (-0.97548473285, -0.11363305815833324, -0.595219650075)
k : (-0.51733786525, -0.6565955295583332, 0.108551052825)
l : (-0.5780110871499999, -0.1082690968583333, -1.512817562575)
show/hide computer existence proof
(see shape-existence, preprint)
Attempting to prove existence
Starting realization:
Abstract data:
mode: maximal_simplices
data: [['l', 'i', 'h'], ['g', 'f', 'd'], ['a', 'c', 'd'], ['f', 'e', 'd'], ['c', 'k', 'd'], ['a', 'b', 'c'], ['g', 'b', 'h'], ['a', 'b', 'f'], ['c', 'b', 'i'], ['c', 'j', 'k'], ['k', 'g', 'd'], ['b', 'h', 'i'], ['c', 'j', 'i'], ['a', 'e', 'd'], ['g', 'b', 'f'], ['k', 'g', 'h'], ['j', 'l', 'i'], ['a', 'f', 'e'], ['j', 'l', 'h'], ['j', 'k', 'h']]
Coordinate Data:
d : [549494989 / 1000000000, 3397504217 / 5000000000, -3559872839 / 10000000000]
b : [113712641 / 1250000000, 2091937161 / 10000000000, 3406979303 / 5000000000]
c : [10261042051 / 10000000000, 271507663 / 2000000000, 1673984693 / 5000000000]
g : [847992099 / 10000000000, 5821216233 / 5000000000, 962534549 / 2500000000]
h : [6001463567 / 10000000000, 8966956049 / 10000000000, 1199160967 / 1000000000]
i : [8303420489 / 10000000000, -718932149 / 10000000000, 323303059 / 250000000]
f : [-253746209 / 625000000, 4729606801 / 10000000000, -1453167401 / 10000000000]
e : [-40069849 / 2500000000, 121553637 / 625000000, -319696467 / 312500000]
k : [10839363171 / 10000000000, 11338394549 / 10000000000, 3567180499 / 10000000000]
l : [1144609539 / 1000000000, 2927565111 / 5000000000, 19780866653 / 10000000000]
j : [15420831847 / 10000000000, 1181753967 / 2000000000, 1325610941 / 1250000000]
a : [268717333 / 1000000000, -1321214417 / 5000000000, -1813113387 / 10000000000]
Desired square lengths:
default : 1
Checking inequality 1:
d = 3
|V| = 12
|E| = 30
Success: d|V| >= |E|
Checking self-intersection:
Square collision distance = 217013888744589423336561149640035252730634162002977471529 / 434027777686403663892875797723111164025000000000000000000
Collision distance in [35355339 / 50000000, 70710679 / 100000000] ~ [0.70711, 0.70711]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [8471 / 10000, 8473 / 10000] ~ [0.8471, 0.8473]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 4485830989767274266341 / 5000000000000000000000000000000000000000
rho in [37887543 / 40000000000000000, 437887543 / 40000000000000000] ~ [0.0, 0.0]
sigma_min ^ 2 / (16 * E ^ .5) in [71757841 / 8763560928, 71791729 / 8763560912] ~ [0.00819, 0.00819]
Success: rho < sigma_min ^ 2 / (16 * E ^ .5)
Checking inequality 4:
LHS NUM := sigma_min - [sigma_min ^ 2 - 16 * rho * |E| ^ .5 ] ^ .5 in [-4999 / 25000000, 20057 / 100000000] ~ [-0.0002, 0.0002]
LHS DEN := 8 * |E| ^ .5 in [547722557 / 12500000, 273861279 / 6250000] ~ [43.8178, 43.8178]
LHS := (LHS NUM) / (LHS DEN) in [-4999 / 1095445114, 20057 / 4381780456] ~ [-0.0, 0.0]
CD / |V| ^ .5 in [1309457 / 6415003, 70710679 / 346410161] ~ [0.20412, 0.20412]
Success: LHS < CD / |V| ^ .5
Success: existence proven