show/hide visualization coordinates
a : (0.8937163101166666, 0.23100092588333337, 0.0691278603833334)
b : (-0.029848091783333253, 0.2726370724833334, 0.4503051717833334)
c : (0.7164543544166667, -0.11769464041666666, 0.9894475590833335)
d : (1.606015007216667, 0.28247485688333335, 0.7691141061833334)
e : (1.3468483874166668, -0.6031091523166666, 0.3836618575833334)
f : (0.3653317388166667, -0.6090114606166667, 0.19237690728333345)
g : (0.10301567741666673, 0.04744714238333331, -0.5149084676166665)
h : (-0.7174752709833333, 0.5399902123833333, -0.2247436999166666)
i : (-0.6013840611833332, -0.42361772411666665, 0.01605114028333343)
j : (-0.7807138579833333, -0.16342313861666663, -0.9327062701166666)
k : (-1.3992285693833333, 0.6221203982833332, -0.9517008206166666)
l : (-1.5027316240833333, -0.07881449221666664, -0.24602534431666656)
show/hide computer existence proof
(see shape-existence, preprint)
Attempting to prove existence
Starting realization:
Abstract data:
mode: maximal_simplices
data: [['i', 'b', 'f'], ['c', 'b', 'a'], ['h', 'i', 'l'], ['c', 'd', 'e'], ['h', 'l', 'k'], ['c', 'd', 'a'], ['h', 'b', 'g'], ['h', 'i', 'b'], ['e', 'a', 'f'], ['g', 'i', 'f'], ['b', 'a', 'g'], ['j', 'i', 'l'], ['j', 'k', 'l'], ['h', 'j', 'g'], ['c', 'b', 'f'], ['h', 'j', 'k'], ['g', 'a', 'f'], ['c', 'e', 'f'], ['j', 'i', 'g'], ['d', 'e', 'a']]
Coordinate Data:
a : [14005555893 / 10000000000, 349326297 / 500000000, 2847193031 / 5000000000]
e : [9268438333 / 5000000000, -677287421 / 5000000000, 4419863017 / 5000000000]
k : [-4461946451 / 5000000000, 1362215083 / 1250000000, -1128475187 / 2500000000]
i : [-47272391 / 500000000, 5504243 / 125000000, 5163618861 / 10000000000]
d : [1320533929 / 625000000, 30005061 / 40000000, 317356213 / 250000000]
g : [3049274783 / 5000000000, 1030197621 / 2000000000, -72988609 / 5000000000]
c : [764558521 / 625000000, 3499570277 / 10000000000, 14897583049 / 10000000000]
l : [-9958923449 / 10000000000, 3888371759 / 10000000000, 508570803 / 2000000000]
j : [-684686447 / 2500000000, 608457059 / 2000000000, -4323955243 / 10000000000]
f : [436085509 / 500000000, -56543917 / 400000000, 6926876531 / 10000000000]
h : [-1053179959 / 5000000000, 2015283761 / 2000000000, 2755670459 / 10000000000]
b : [2384955937 / 5000000000, 3701443703 / 5000000000, 1188269897 / 1250000000]
Desired square lengths:
default : 1
Checking inequality 1:
d = 3
|V| = 12
|E| = 30
Success: d|V| >= |E|
Checking self-intersection:
Square collision distance = 499999829274346313648136918496858487243492018717060535473689 / 1000002047686016886952494984524551895156600000000000000000000
Collision distance in [70710593 / 100000000, 35355297 / 50000000] ~ [0.70711, 0.70711]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [601 / 1000, 1503 / 2500] ~ [0.601, 0.6012]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 52309657365621822217039265999 / 2500000000000000000000000000000000000000
rho in [457426091 / 100000000000000, 458426091 / 100000000000000] ~ [0.0, 0.0]
sigma_min ^ 2 / (16 * E ^ .5) in [9030025 / 2190890232, 2259009 / 547722557] ~ [0.00412, 0.00412]
Success: rho < sigma_min ^ 2 / (16 * E ^ .5)
Checking inequality 4:
LHS NUM := sigma_min - [sigma_min ^ 2 - 16 * rho * |E| ^ .5 ] ^ .5 in [3337 / 25000000, 53433 / 100000000] ~ [0.00013, 0.00053]
LHS DEN := 8 * |E| ^ .5 in [547722557 / 12500000, 273861279 / 6250000] ~ [43.8178, 43.8178]
LHS := (LHS NUM) / (LHS DEN) in [3337 / 1095445116, 53433 / 4381780456] ~ [0.0, 1e-05]
CD / |V| ^ .5 in [70710593 / 346410162, 70710594 / 346410161] ~ [0.20412, 0.20412]
Success: LHS < CD / |V| ^ .5
Success: existence proven