show/hide visualization coordinates
a : (-0.5679068116999999, 0.21501014622499998, 0.0790726893)
b : (0.2972336952000001, 0.006832448524999979, 0.5353554409)
c : (0.29735818580000006, 0.35228323962499997, -0.40308141659999996)
d : (-0.02668506929999992, -0.5741258343750001, -0.2113467136)
show/hide computer existence proof
(see shape-existence, preprint)
Attempting to prove existence
Starting realization:
Abstract data:
mode: maximal_simplices
data: [['a', 'c', 'd'], ['a', 'b', 'd'], ['a', 'c', 'b'], ['d', 'c', 'b']]
Coordinate Data:
d : [2833097891 / 5000000000, 12883601383 / 10000000000, 4393233761 / 5000000000]
a : [5539206603 / 5000000000, 4992241577 / 10000000000, 5882273493 / 10000000000]
b : [2427008137 / 10000000000, 3537009277 / 5000000000, 1319445977 / 10000000000]
c : [2425763231 / 10000000000, 3619510643 / 10000000000, 1337976819 / 1250000000]
Desired square lengths:
default : 1
Checking inequality 1:
d = 3
|V| = 4
|E| = 6
Success: d|V| >= |E|
Checking self-intersection:
Square collision distance = 499999999925487550081908656790837135405879001937919168003481 / 999999999988808696339483520336223459183700000000000000000000
Collision distance in [35355339 / 50000000, 70710679 / 100000000] ~ [0.70711, 0.70711]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [9999 / 5000, 2] ~ [1.9998, 2.0]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 3490187677861761763 / 80000000000000000000000000000000000000
rho in [208871601 / 1000000000000000000, 10208871601 / 1000000000000000000] ~ [0.0, 0.0]
sigma_min ^ 2 / (16 * E ^ .5) in [99980001 / 979795900, 12500000 / 122474487] ~ [0.10204, 0.10206]
Success: rho < sigma_min ^ 2 / (16 * E ^ .5)
Checking inequality 4:
LHS NUM := sigma_min - [sigma_min ^ 2 - 16 * rho * |E| ^ .5 ] ^ .5 in [-1 / 5000, 20011 / 100000000] ~ [-0.0002, 0.0002]
LHS DEN := 8 * |E| ^ .5 in [122474487 / 6250000, 9797959 / 500000] ~ [19.59592, 19.59592]
LHS := (LHS NUM) / (LHS DEN) in [-1250 / 122474487, 20011 / 1959591792] ~ [-1e-05, 1e-05]
CD / |V| ^ .5 in [23570226 / 66666667, 70710679 / 200000000] ~ [0.35355, 0.35355]
Success: LHS < CD / |V| ^ .5
Success: existence proven