show/hide visualization coordinates
a : (-0.3988952431727272, 0.19269451026363632, 0.6886854716909089)
b : (-0.4262005190727272, -0.01600901503636365, -0.28891218900909105)
c : (-0.7352854007727272, -0.6957010846363637, 0.3762833831909089)
d : (-1.1078594224727272, -0.2843291837363637, 1.2081257222909092)
e : (-0.17176961327272722, -0.6360017088363636, 1.2002286873909092)
f : (0.2372258162272728, -0.47500959673636367, 0.302005806190909)
g : (0.3433722085272728, 0.49681824036363637, 0.09156918729090902)
h : (0.04210646672727281, 0.6696637283636364, -0.846174583609091)
i : (0.5018267731272729, -0.18882816763636368, -0.618910350509091)
j : (1.0177375008272729, 0.6677781234636364, -0.626765194909091)
k : (0.6977414333272728, 0.2689241541636363, -1.486135940009091)
show/hide computer existence proof
(see shape-existence, preprint)
Attempting to prove existence
Starting realization:
Abstract data:
mode: maximal_simplices
data: [['a', 'd', 'c'], ['b', 'g', 'h'], ['a', 'b', 'c'], ['f', 'a', 'e'], ['f', 'i', 'b'], ['f', 'a', 'g'], ['f', 'c', 'e'], ['i', 'g', 'j'], ['i', 'b', 'h'], ['f', 'b', 'c'], ['a', 'b', 'g'], ['f', 'i', 'g'], ['j', 'k', 'h'], ['i', 'j', 'k'], ['g', 'j', 'h'], ['d', 'c', 'e'], ['a', 'd', 'e'], ['i', 'k', 'h']]
Coordinate Data:
f : [8580686971 / 10000000000, 47909109 / 10000000000, 1138229357 / 1250000000]
e : [1122683169 / 2500000000, -390503003 / 2500000000, 4522015917 / 2500000000]
k : [6592921571 / 5000000000, 3743623309 / 5000000000, -4387791303 / 5000000000]
g : [4821075447 / 5000000000, 244154687 / 250000000, 7001468667 / 10000000000]
i : [561334827 / 500000000, 14548617 / 50000000, -103326711 / 10000000000]
h : [1657373369 / 2500000000, 287366059 / 250000000, -1187984521 / 5000000000]
j : [16385803817 / 10000000000, 11475786311 / 10000000000, -36375031 / 2000000000]
d : [-608770677 / 1250000000, 1954713239 / 10000000000, 18167034017 / 10000000000]
b : [973211809 / 5000000000, 2318957463 / 5000000000, 399581863 / 1250000000]
c : [-1144425199 / 10000000000, -215900577 / 1000000000, 4924305313 / 5000000000]
a : [2219476377 / 10000000000, 6724950179 / 10000000000, 12972631511 / 10000000000]
Desired square lengths:
default : 1
Checking inequality 1:
d = 3
|V| = 11
|E| = 27
Success: d|V| >= |E|
Checking self-intersection:
Square collision distance = 166666666416823190766362989416074675186729010492369372040443 / 333333416496256174378647431725004801159300000000000000000000
Collision distance in [70710669 / 100000000, 7071067 / 10000000] ~ [0.70711, 0.70711]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [6271 / 10000, 6273 / 10000] ~ [0.6271, 0.6273]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 1444103504321703141772807701 / 10000000000000000000000000000000000000000
rho in [190006809 / 500000000000000, 195006809 / 500000000000000] ~ [0.0, 0.0]
sigma_min ^ 2 / (16 * E ^ .5) in [39325441 / 8313843888, 39350529 / 8313843872] ~ [0.00473, 0.00473]
Success: rho < sigma_min ^ 2 / (16 * E ^ .5)
Checking inequality 4:
LHS NUM := sigma_min - [sigma_min ^ 2 - 16 * rho * |E| ^ .5 ] ^ .5 in [-8741 / 50000000, 11293 / 50000000] ~ [-0.00017, 0.00023]
LHS DEN := 8 * |E| ^ .5 in [259807621 / 6250000, 519615243 / 12500000] ~ [41.56922, 41.56922]
LHS := (LHS NUM) / (LHS DEN) in [-8741 / 2078460968, 11293 / 2078460968] ~ [-0.0, 1e-05]
CD / |V| ^ .5 in [23570223 / 110554160, 70710670 / 331662479] ~ [0.2132, 0.2132]
Success: LHS < CD / |V| ^ .5
Success: existence proven