show/hide visualization coordinates
a : (-1.0633113080714285, -0.47218891665, 0.37208965598571425)
b : (-0.25999826247142854, -0.6073715076500001, -0.2079221456142858)
c : (-0.5720496499714286, -1.3429408493500001, 0.39337772408571425)
d : (-1.5587851279714284, -1.32148783115, 0.5542901530857143)
e : (-0.9321831778714286, -0.9512056367500001, 1.2400460625857144)
f : (-0.15291091427142856, -0.52273574455, 0.7827185984857142)
g : (-0.4120972056714286, 0.27474344414999996, 0.23787970698571426)
h : (0.04705157552857142, 0.23561449845, -0.6496174773142857)
i : (0.5133070200285714, -0.09805359605000002, 0.16969421608571425)
j : (0.3588395056285714, 0.88224105295, 0.04655945978571424)
k : (0.44055096772857144, 1.11337350025, -0.9229254825142857)
l : (1.0248958846285714, 0.40512423794999997, -0.5267890206142858)
m : (1.1691394499285714, 1.36487802245, -0.2858193510142858)
n : (1.3975512428285715, 1.04000932595, -1.2035821000142857)
show/hide computer existence proof
(see shape-existence, preprint)
Attempting to prove existence
Starting realization:
Abstract data:
mode: maximal_simplices
data: [['a', 'f', 'g'], ['i', 'j', 'l'], ['a', 'd', 'c'], ['j', 'g', 'h'], ['m', 'l', 'j'], ['a', 'b', 'c'], ['f', 'i', 'g'], ['b', 'h', 'g'], ['j', 'h', 'k'], ['f', 'b', 'c'], ['n', 'm', 'k'], ['e', 'a', 'd'], ['i', 'j', 'g'], ['b', 'h', 'i'], ['f', 'b', 'i'], ['n', 'l', 'k'], ['m', 'j', 'k'], ['l', 'h', 'i'], ['a', 'b', 'g'], ['e', 'c', 'f'], ['e', 'a', 'f'], ['e', 'c', 'd'], ['m', 'l', 'n'], ['l', 'h', 'k']]
Coordinate Data:
l : [-632675303 / 1000000000, 13381361 / 625000000, 9451477349 / 10000000000]
a : [14555318897 / 10000000000, 4493616661 / 5000000000, 462690583 / 10000000000]
g : [8043177873 / 10000000000, 758954857 / 5000000000, 1804790073 / 10000000000]
i : [-4729939 / 39062500, 1311470029 / 2500000000, 1243322491 / 5000000000]
h : [3451690061 / 10000000000, 1909199171 / 10000000000, 2669940479 / 2500000000]
m : [-7769188683 / 10000000000, -9383436069 / 10000000000, 7041780653 / 10000000000]
n : [-2513326653 / 2500000000, -383421819 / 625000000, 16219408143 / 10000000000]
e : [2648807519 / 2000000000, 13777400523 / 10000000000, -8216873483 / 10000000000]
b : [6522188441 / 10000000000, 323095601 / 312500000, 6262808599 / 10000000000]
c : [2410675579 / 2500000000, 17694752649 / 10000000000, 124904951 / 5000000000]
f : [5451314959 / 10000000000, 9492701601 / 10000000000, -1821799421 / 5000000000]
k : [-483303861 / 10000000000, -6868390847 / 10000000000, 838302623 / 625000000]
d : [2438757137 / 1250000000, 17480222467 / 10000000000, -339828597 / 2500000000]
j : [8345269 / 250000000, -2278533187 / 5000000000, 743598509 / 2000000000]
Desired square lengths:
default : 1
Checking inequality 1:
d = 3
|V| = 14
|E| = 36
Success: d|V| >= |E|
Checking self-intersection:
Square collision distance = 31249997633383260171109295086501503638233852654098334940809 / 62500022265526058887358240831863953638675000000000000000000
Collision distance in [35355331 / 50000000, 70710663 / 100000000] ~ [0.70711, 0.70711]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [467 / 1000, 292 / 625] ~ [0.467, 0.4672]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 3750079825117902057045033967 / 10000000000000000000000000000000000000000
rho in [612378953 / 1000000000000000, 622378953 / 1000000000000000] ~ [0.0, 0.0]
sigma_min ^ 2 / (16 * E ^ .5) in [5452225 / 2400000004, 5329 / 2343750] ~ [0.00227, 0.00227]
Success: rho < sigma_min ^ 2 / (16 * E ^ .5)
Checking inequality 4:
LHS NUM := sigma_min - [sigma_min ^ 2 - 16 * rho * |E| ^ .5 ] ^ .5 in [-13709 / 100000000, 13199 / 50000000] ~ [-0.00014, 0.00026]
LHS DEN := 8 * |E| ^ .5 in [48, 600000001 / 12500000] ~ [48.0, 48.0]
LHS := (LHS NUM) / (LHS DEN) in [-13709 / 4800000000, 13199 / 2400000000] ~ [-0.0, 1e-05]
CD / |V| ^ .5 in [70710662 / 374165739, 70710663 / 374165738] ~ [0.18898, 0.18898]
Success: LHS < CD / |V| ^ .5
Success: existence proven