show/hide visualization coordinates
a : (-0.08360826275454547, -0.14013997429090908, 0.7474933391545455)
b : (0.7057187034454545, 0.2198063683090909, 0.2500984618545455)
c : (0.3756226879454545, 0.6875656190090909, 1.0699996196545456)
d : (-0.16501939755454553, 0.7111037685090909, 0.2290762132545455)
e : (-0.8738456404545454, 0.45658404270909086, 0.8869401783545455)
f : (-0.7777320634545455, -0.05443045389090917, 0.03275848315454549)
g : (0.11134755984545452, -0.45987009619090913, -0.17974172014545453)
h : (1.0059168320454546, -0.25523930489090907, -0.5770730416454545)
i : (0.061304507445454515, 0.06338132550909087, -0.49840785744545446)
j : (-0.6503021279545456, -0.5614161290909091, -0.8197244455454545)
k : (0.29059720144545453, -0.6673451656909092, -1.1414192306454547)
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'], ['f', 'i', 'd'], ['a', 'b', 'c'], ['f', 'a', 'e'], ['f', 'i', 'j'], ['f', 'a', 'g'], ['i', 'b', 'h'], ['i', 'b', 'd'], ['g', 'j', 'k'], ['b', 'd', 'c'], ['f', 'g', 'j'], ['g', 'k', 'h'], ['a', 'b', 'g'], ['i', 'j', 'k'], ['f', 'd', 'e'], ['a', 'd', 'e'], ['i', 'k', 'h']]
Coordinate Data:
f : [6103053437 / 5000000000, 6143983709 / 10000000000, 331288207 / 1000000000]
e : [3291810661 / 2500000000, 1033838743 / 10000000000, -2614467441 / 5000000000]
k : [60912569 / 400000000, 12273130827 / 10000000000, 1881832401 / 1250000000]
g : [3315310641 / 10000000000, 2549595033 / 2500000000, 5437884103 / 10000000000]
i : [763148233 / 2000000000, 993173183 / 2000000000, 2156136369 / 2500000000]
h : [-5630382081 / 10000000000, 8152072219 / 10000000000, 4705598659 / 5000000000]
j : [10931807519 / 10000000000, 11213840461 / 10000000000, 11837711357 / 10000000000]
d : [1215796043 / 2000000000, -302271703 / 2000000000, 1349704769 / 10000000000]
b : [-525680159 / 2000000000, 3401615487 / 10000000000, 1139482283 / 10000000000]
c : [525437 / 7812500, -63798851 / 500000000, -1411905859 / 2000000000]
a : [5264868867 / 10000000000, 7001078913 / 10000000000, -383446649 / 1000000000]
Desired square lengths:
default : 1
Checking inequality 1:
d = 3
|V| = 11
|E| = 27
Success: d|V| >= |E|
Checking self-intersection:
Square collision distance = 81881561366711675596687955488932039352031569781757609009 / 298588840140572576570698811392138766600000000000000000000
Collision distance in [13091707 / 25000000, 52366829 / 100000000] ~ [0.52367, 0.52367]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [3119 / 5000, 78 / 125] ~ [0.6238, 0.624]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 2601366819217232075229257919 / 5000000000000000000000000000000000000000
rho in [721299773 / 1000000000000000, 731299773 / 1000000000000000] ~ [0.0, 0.0]
sigma_min ^ 2 / (16 * E ^ .5) in [9728161 / 2078460972, 1216800 / 259807621] ~ [0.00468, 0.00468]
Success: rho < sigma_min ^ 2 / (16 * E ^ .5)
Checking inequality 4:
LHS NUM := sigma_min - [sigma_min ^ 2 - 16 * rho * |E| ^ .5 ] ^ .5 in [-3039 / 20000000, 12437 / 50000000] ~ [-0.00015, 0.00025]
LHS DEN := 8 * |E| ^ .5 in [259807621 / 6250000, 519615243 / 12500000] ~ [41.56922, 41.56922]
LHS := (LHS NUM) / (LHS DEN) in [-15195 / 4156921936, 12437 / 2078460968] ~ [-0.0, 1e-05]
CD / |V| ^ .5 in [13091707 / 82915620, 52366829 / 331662479] ~ [0.15789, 0.15789]
Success: LHS < CD / |V| ^ .5
Success: existence proven