show/hide visualization coordinates
a : (-0.04376512599999993, 0.17726008264000004, 0.54771964558)
b : (0.35604847140000007, 0.27222729184, -0.36394384301999994)
c : (-0.6041999800999999, 0.50653366414, -0.21220908981999997)
d : (-0.3122833453999999, -0.44948737456, -0.18377580251999998)
e : (0.6041999801, -0.50653366406, 0.21220908978000003)
show/hide computer existence proof
(see shape-existence, preprint)
Attempting to prove existence
Starting realization:
Abstract data:
mode: maximal_simplices
data: [['a', 'e', 'b'], ['d', 'c', 'b'], ['a', 'e', 'd'], ['d', 'e', 'b'], ['a', 'c', 'd'], ['a', 'c', 'b']]
Coordinate Data:
b : [10661715609 / 10000000000, 701284203 / 1250000000, -75437119 / 10000000000]
e : [1642903837 / 1250000000, -435467187 / 2000000000, 5686092209 / 10000000000]
c : [529615547 / 5000000000, 7953337347 / 10000000000, 1441910413 / 10000000000]
a : [1332715927 / 2000000000, 1165150383 / 2500000000, 9041197767 / 10000000000]
d : [3978397441 / 10000000000, -20085913 / 125000000, 863121643 / 5000000000]
Desired square lengths:
default : 1
Checking inequality 1:
d = 3
|V| = 5
|E| = 9
Success: d|V| >= |E|
Checking self-intersection:
Square collision distance = 4999999997801308906291118416991496984007970078211221629009 / 9999999999305875411455376606539571907640000000000000000000
Collision distance in [35355339 / 50000000, 70710679 / 100000000] ~ [0.70711, 0.70711]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [15579 / 10000, 15581 / 10000] ~ [1.5579, 1.5581]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 519523019009078645743 / 2500000000000000000000000000000000000000
rho in [56982619 / 125000000000000000, 1306982619 / 125000000000000000] ~ [0.0, 0.0]
sigma_min ^ 2 / (16 * E ^ .5) in [242705241 / 4800000016, 242767561 / 4800000000] ~ [0.05056, 0.05058]
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, 20017 / 100000000] ~ [-0.0002, 0.0002]
LHS DEN := 8 * |E| ^ .5 in [24, 300000001 / 12500000] ~ [24.0, 24.0]
LHS := (LHS NUM) / (LHS DEN) in [-1 / 120000, 20017 / 2400000000] ~ [-1e-05, 1e-05]
CD / |V| ^ .5 in [35355339 / 111803399, 70710679 / 223606797] ~ [0.31623, 0.31623]
Success: LHS < CD / |V| ^ .5
Success: existence proven