show/hide visualization coordinates
a : (-0.3765237623416667, 0.45188083874166673, 0.25610670015000003)
b : (-0.32183369894166663, -0.5462296818583333, 0.28411358085000005)
c : (-0.6800258506416668, -0.04284566215833324, 1.07043597715)
d : (-0.10762774884166665, 0.7717023499416668, 1.16462699965)
e : (0.5700386215583334, 0.7229443833416667, 0.43087571285000004)
f : (0.22802120735833337, 0.6778666675416667, -0.50773607475)
g : (-0.42415686194166663, -0.07547905165833324, -0.59219904295)
h : (0.11295729805833338, -0.9171464559583333, -0.5364822610499999)
i : (0.5364721635583334, -0.15459638725833325, -0.04745000094999996)
j : (0.30728486975833336, -0.10595957575833326, 0.92471646875)
k : (0.46585075305833334, -0.1315290410583333, -1.04468643925)
l : (-0.3104569906416666, -0.6506083838583332, -1.40232162045)
show/hide computer existence proof
(see shape-existence, preprint)
Attempting to prove existence
Starting realization:
Abstract data:
mode: maximal_simplices
data: [['c', 'b', 'a'], ['i', 'k', 'f'], ['h', 'l', 'g'], ['j', 'd', 'e'], ['h', 'k', 'l'], ['c', 'd', 'a'], ['h', 'b', 'g'], ['h', 'i', 'b'], ['e', 'a', 'f'], ['g', 'k', 'f'], ['l', 'k', 'g'], ['b', 'a', 'g'], ['j', 'c', 'b'], ['j', 'i', 'b'], ['h', 'i', 'k'], ['g', 'a', 'f'], ['i', 'e', 'f'], ['j', 'c', 'd'], ['d', 'e', 'a'], ['j', 'i', 'e']]
Coordinate Data:
a : [8485728191 / 10000000000, -104486607 / 5000000000, 3645659847 / 10000000000]
e : [-30621739 / 312500000, -145980433 / 500000000, 47449243 / 250000000]
k : [61983037 / 10000000000, 351570349 / 625000000, 16653591241 / 10000000000]
i : [-161057767 / 2500000000, 2927899523 / 5000000000, 3340613429 / 5000000000]
g : [8962059187 / 10000000000, 506462569 / 1000000000, 6064358639 / 5000000000]
d : [724596007 / 1250000000, -1703594163 / 5000000000, -1359885787 / 2500000000]
c : [5760374537 / 5000000000, 947658359 / 2000000000, -4497632923 / 10000000000]
l : [3912530237 / 5000000000, 2703979753 / 2500000000, 20229943053 / 10000000000]
j : [164764187 / 1000000000, 5369430931 / 10000000000, -3040437839 / 10000000000]
f : [1220139247 / 5000000000, -1234415751 / 5000000000, 2821021899 / 2500000000]
h : [3590917587 / 10000000000, 13481299733 / 10000000000, 11571549459 / 10000000000]
b : [7938827557 / 10000000000, 1221516499 / 1250000000, 657342 / 1953125]
Desired square lengths:
default : 1
Checking inequality 1:
d = 3
|V| = 12
|E| = 30
Success: d|V| >= |E|
Checking self-intersection:
Square collision distance = 19999999999031459155559551369980893397341931076125028640169 / 40000000000044762442202360426475758928776000000000000000000
Collision distance in [35355339 / 50000000, 70710679 / 100000000] ~ [0.70711, 0.70711]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [8789 / 10000, 8791 / 10000] ~ [0.8789, 0.8791]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 6648450230183878920937 / 5000000000000000000000000000000000000000
rho in [57656093 / 50000000000000000, 557656093 / 50000000000000000] ~ [0.0, 0.0]
sigma_min ^ 2 / (16 * E ^ .5) in [4543913 / 515503584, 77281681 / 8763560912] ~ [0.00881, 0.00882]
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, 2507 / 12500000] ~ [-0.0002, 0.0002]
LHS DEN := 8 * |E| ^ .5 in [547722557 / 12500000, 273861279 / 6250000] ~ [43.8178, 43.8178]
LHS := (LHS NUM) / (LHS DEN) in [-19995 / 4381780456, 2507 / 547722557] ~ [-0.0, 0.0]
CD / |V| ^ .5 in [1309457 / 6415003, 70710679 / 346410161] ~ [0.20412, 0.20412]
Success: LHS < CD / |V| ^ .5
Success: existence proven