show/hide visualization coordinates
a : (0.07722288349166662, 0.5946752499, 0.1613808527583333)
b : (-0.7571245568083333, 0.043436714399999965, 0.16072793295833332)
c : (-0.42372145870833333, 0.4448400644, 1.0137916602583332)
d : (0.5502165397916665, 0.22429876240000002, 0.9608170665583333)
e : (1.0711707750916666, 0.48561439009999996, 0.14821579595833334)
f : (0.5138305572916666, 0.07810298449999997, -0.5751833561416666)
g : (-0.41385298760833344, 0.43192655739999997, -0.6943979468416668)
h : (-0.9790617464083333, -0.3928485837, -0.7112806795416666)
i : (-0.12411824740833344, -0.6168441988000001, -0.24341576424166667)
j : (-0.13290720580833348, -0.47377450070000005, 0.7462578268583333)
k : (0.7322499941916666, -0.4501766785, 0.24531255875833333)
l : (-0.11390454710833342, -0.3692507614, -1.2122259473416668)
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'], ['h', 'i', 'l'], ['c', 'd', 'a'], ['h', 'b', 'g'], ['h', 'i', 'b'], ['e', 'a', 'f'], ['j', 'i', 'k'], ['g', 'l', 'f'], ['j', 'd', 'k'], ['b', 'a', 'g'], ['j', 'c', 'b'], ['d', 'e', 'k'], ['j', 'i', 'b'], ['e', 'k', 'f'], ['i', 'l', 'f'], ['g', 'a', 'f'], ['j', 'c', 'd'], ['d', 'e', 'a']]
Coordinate Data:
a : [5469208251 / 10000000000, -92659799 / 1250000000, 3000267951 / 10000000000]
e : [-894054133 / 2000000000, 174665103 / 5000000000, 3131918519 / 10000000000]
k : [-135132857 / 1250000000, 2426810223 / 2500000000, 2160950891 / 10000000000]
i : [187065489 / 250000000, 2274783219 / 2000000000, 7048234121 / 10000000000]
g : [5189983481 / 5000000000, 886208533 / 10000000000, 11558055947 / 10000000000]
d : [92408961 / 1250000000, 2962486483 / 10000000000, -4994094187 / 10000000000]
c : [10478651673 / 10000000000, 757073463 / 10000000000, -1380960031 / 2500000000]
l : [7380482557 / 10000000000, 8897981721 / 10000000000, 1046020997 / 625000000]
j : [946313643 / 1250000000, 4971609557 / 5000000000, -284850179 / 1000000000]
f : [1103131513 / 10000000000, 2212222131 / 5000000000, 259147751 / 250000000]
h : [320641091 / 200000000, 1141744993 / 1250000000, 5863441637 / 5000000000]
b : [6906341327 / 5000000000, 4771106963 / 10000000000, 3006797149 / 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 = 2913135049555833026118155432476911164750948447263705352283 / 5013068329574623831144206162736489115187500000000000000000
Collision distance in [19057613 / 25000000, 76230453 / 100000000] ~ [0.7623, 0.7623]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [923 / 1250, 3693 / 5000] ~ [0.7384, 0.7386]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 556915359791677501295001 / 10000000000000000000000000000000000000000
rho in [746267619 / 100000000000000000, 1746267619 / 100000000000000000] ~ [0.0, 0.0]
sigma_min ^ 2 / (16 * E ^ .5) in [1703858 / 273861279, 13638249 / 2190890228] ~ [0.00622, 0.00622]
Success: rho < sigma_min ^ 2 / (16 * E ^ .5)
Checking inequality 4:
LHS NUM := sigma_min - [sigma_min ^ 2 - 16 * rho * |E| ^ .5 ] ^ .5 in [-4989 / 25000000, 2513 / 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 [-4989 / 1095445114, 2513 / 547722557] ~ [-0.0, 0.0]
CD / |V| ^ .5 in [38115226 / 173205081, 76230453 / 346410161] ~ [0.22006, 0.22006]
Success: LHS < CD / |V| ^ .5
Success: existence proven