show/hide visualization coordinates
a : (-0.06352844063967944, 0.6989269660318513, -0.524903829169019)
b : (-1.0605948325983494, 0.6285678644880311, -0.4947673586313771)
c : (-0.538623748918615, 0.7020468691656243, 0.35502498286964745)
d : (0.4372265511049934, 0.9163914669753637, 0.31292290057417893)
e : (0.9354825912095746, 0.7418875127347415, -0.5363646175571598)
f : (0.4564151868499482, 0.08752602222715894, -1.1214333843024247)
g : (-0.5264762582070461, -0.050039836893781775, -0.9989587271765893)
h : (-1.4717651448672266, -0.24922017136551933, -0.740586679314435)
i : (-1.0799859078727643, -0.11815168763582318, 0.170088939132021)
j : (-0.25942610858647236, -0.1783020374115729, 0.7384757363195484)
k : (0.016179177865189687, 0.6721930993385405, 1.186470991254579)
l : (0.9856206738817714, 0.9146589017615364, 1.1491411043473736)
m : (1.311230147424759, 0.431052798985145, 0.33667350001075214)
n : (0.9699448787049372, -0.23520679764388697, -0.3263668571731516)
o : (0.12278180839024255, -0.6940314121505067, -0.5943121975279183)
p : (-0.8062590191175014, -0.9920351220171981, -0.813576717524691)
q : (-1.4841053760643852, -0.9984585155047234, -0.07840118991924738)
r : (-0.5100619421248027, -0.9393014506511363, 0.14009327334491672)
s : (0.45203518825532013, -0.762197547695215, 0.34746569019950296)
t : (0.6992453629407556, -0.028472369923978724, 0.9803436350171149)
u : (1.4146652123693497, -0.5478345528146511, 0.5129708052263755)
show/hide computer existence proof
(see shape-existence, preprint)
Attempting to prove existence
Starting realization:
Abstract data:
mode: maximal_simplices
data: [['j', 't', 's'], ['j', 'c', 'k'], ['q', 'h', 'p'], ['t', 'm', 'u'], ['a', 'g', 'f'], ['n', 's', 'u'], ['t', 's', 'u'], ['m', 'e', 'n'], ['t', 'm', 'l'], ['q', 'i', 'r'], ['m', 'e', 'd'], ['o', 'g', 'f'], ['q', 'h', 'i'], ['o', 'n', 'f'], ['j', 't', 'k'], ['o', 'p', 'r'], ['c', 'i', 'b'], ['j', 'i', 'r'], ['a', 'c', 'b'], ['j', 'c', 'i'], ['e', 'n', 'f'], ['m', 'n', 'u'], ['m', 'l', 'd'], ['j', 's', 'r'], ['l', 'k', 'd'], ['h', 'i', 'b'], ['l', 't', 'k'], ['a', 'e', 'f'], ['c', 'k', 'd'], ['o', 'g', 'p'], ['a', 'c', 'd'], ['h', 'g', 'p'], ['o', 'n', 's'], ['a', 'g', 'b'], ['o', 's', 'r'], ['h', 'g', 'b'], ['q', 'p', 'r'], ['a', 'e', 'd']]
Coordinate Data:
a : [48624666896214611549 / 100000000000000000000, -848328888877251359 / 5000000000000000000, 109352252390285996421 / 100000000000000000000]
l : [-28145122277965233951 / 50000000000000000000, -38539771350513531187 / 100000000000000000000, -29026120480676634101 / 50000000000000000000]
o : [14996820996611205699 / 50000000000000000000, 122329260040690768357 / 100000000000000000000, 116293089226175921153 / 100000000000000000000]
h : [189448337318969331863 / 100000000000000000000, 1556962719243840819 / 2000000000000000000, 130920537404827593931 / 100000000000000000000]
k : [2540869065357981389 / 6250000000000000000, -3573297777053486779 / 25000000000000000000, -15446307413018453581 / 25000000000000000000]
c : [96134197724108177967 / 100000000000000000000, -863928404546115843 / 5000000000000000000, 266992139830241773 / 1250000000000000000]
n : [-437781320305976357 / 800000000000000000, 19111699647507202623 / 25000000000000000000, 11187319398837405213 / 12500000000000000000]
u : [-49597349202344148103 / 50000000000000000000, 107709574107105219303 / 100000000000000000000, 5564788950746540057 / 100000000000000000000]
f : [-673939170549629597 / 20000000000000000000, 44173516602924217053 / 100000000000000000000, 84502603951813273933 / 50000000000000000000]
b : [148331306092081615293 / 100000000000000000000, -9930667623163003591 / 100000000000000000000, 13292325667065224983 / 12500000000000000000]
j : [34107216845446954881 / 50000000000000000000, 14151264513359480923 / 20000000000000000000, -135885633268566087 / 800000000000000000]
p : [122897724743996801683 / 100000000000000000000, 19016203878419991683 / 12500000000000000000, 138219541225853184269 / 100000000000000000000]
q : [95341180219342587453 / 50000000000000000000, 38192992594028113701 / 25000000000000000000, 16175497116327207051 / 25000000000000000000]
r : [46639008522363475189 / 50000000000000000000, 146856263890753744403 / 100000000000000000000, 21426271069446207671 / 50000000000000000000]
g : [47459724326475644041 / 50000000000000000000, 57930102515018293203 / 100000000000000000000, 78378871095521509747 / 50000000000000000000]
t : [-27652713461828887523 / 100000000000000000000, 11154671163607595963 / 20000000000000000000, -20586247014163703233 / 50000000000000000000]
d : [-725416139126335083 / 50000000000000000000, -4839128483987031257 / 12500000000000000000, 25569579415966191201 / 100000000000000000000]
s : [-2931695993285343539 / 100000000000000000000, 64572936797580801443 / 50000000000000000000, 11057650226716894621 / 50000000000000000000]
e : [-51276436288710781703 / 100000000000000000000, -4252526489566808437 / 20000000000000000000, 55249165614550029709 / 50000000000000000000]
m : [-88851191910229228939 / 100000000000000000000, 4910419463562807259 / 50000000000000000000, 11597259736154435089 / 50000000000000000000]
i : [150270413619523088943 / 100000000000000000000, 64741287589222433613 / 100000000000000000000, 19926487780090993517 / 50000000000000000000]
Desired square lengths:
default : 1
Checking inequality 1:
d = 3
|V| = 21
|E| = 57
Success: d|V| >= |E|
Checking self-intersection:
Square collision distance = 128075838231991261493266525247881395500585765585364541326065225790685461490780650123599789509925067755088568094407807 / 219111725957687288095961840151489500544064159448185346231053403611437465226129520000000000000000000000000000000000000
Collision distance in [764541023392786340660130986391 / 1000000000000000000000000000000, 95567627924098292582516373299 / 125000000000000000000000000000] ~ [0.76454, 0.76454]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [1411 / 2500, 2823 / 5000] ~ [0.5644, 0.5646]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 354758880887488780825838958841500400668917 / 12500000000000000000000000000000000000000000000000000000000000000000000000000000
rho in [1684657545942174636661547324967 / 10000000000000000000000000000000000000000000000000, 1684657545952174636661547324967 / 10000000000000000000000000000000000000000000000000] ~ [0.0, 0.0]
sigma_min ^ 2 / (16 * E ^ .5) in [19909210000000000000000000000 / 7549834435270749697236684806947, 3320553750000000000000000000 / 1258305739211791616206114134491] ~ [0.00264, 0.00264]
Success: rho < sigma_min ^ 2 / (16 * E ^ .5)
Checking inequality 4:
LHS NUM := sigma_min - [sigma_min ^ 2 - 16 * rho * |E| ^ .5 ] ^ .5 in [-19999999999998197819971379 / 100000000000000000000000000000, 200000000000018028186466433 / 1000000000000000000000000000000] ~ [-0.0002, 0.0002]
LHS DEN := 8 * |E| ^ .5 in [3774917217635374848618342403473 / 62500000000000000000000000000, 7549834435270749697236684806947 / 125000000000000000000000000000] ~ [60.39868, 60.39868]
LHS := (LHS NUM) / (LHS DEN) in [-99999999999990989099856895 / 30199337741082998788946739227784, 200000000000018028186466433 / 60398675482165997577893478455568] ~ [-0.0, 0.0]
CD / |V| ^ .5 in [764541023392786340660130986391 / 4582575694955840006588047193729, 95567627924098292582516373299 / 572821961869480000823505899216] ~ [0.16684, 0.16684]
Success: LHS < CD / |V| ^ .5
Success: existence proven