show/hide visualization coordinates
a : (-0.18972277553076927, -0.030404908007692466, -0.5880614766384615)
b : (-0.6693852233307693, -0.022959126107692462, 0.28936002786153836)
c : (-0.9830520415307693, 0.5641012019923075, -0.45694640933846165)
d : (-0.15880426803076936, 0.9200840435923076, -0.8972779028384616)
e : (0.6149023592692306, 0.5317094555923075, -0.3967349635384616)
f : (0.6795504724692307, -0.4652369101076925, -0.3529335325384616)
g : (-0.17862117293076935, -0.8429335175076924, -0.005245885738461631)
h : (-0.21581547593076927, -0.6040481411076926, 0.9650892937615384)
i : (0.3187055833692307, 0.047133055692307524, 0.42634047826153837)
j : (-0.19799089923076935, 0.8380819486923076, 0.09858356566153836)
k : (0.4119852922692307, 1.5082233507923075, -0.3243106848384616)
l : (0.6499230539692307, -0.8878992689076926, 0.5528692860615384)
m : (-0.08167490483076928, -1.5558511846076926, 0.6892682038615384)
show/hide computer existence proof
(see shape-existence, preprint)
Attempting to prove existence
Starting realization:
Abstract data:
mode: maximal_simplices
data: [['b', 'a', 'c'], ['b', 'j', 'c'], ['i', 'l', 'f'], ['b', 'g', 'a'], ['g', 'a', 'f'], ['d', 'a', 'e'], ['b', 'h', 'g'], ['b', 'i', 'j'], ['i', 'h', 'l'], ['e', 'a', 'f'], ['k', 'e', 'j'], ['m', 'h', 'g'], ['j', 'd', 'c'], ['b', 'i', 'h'], ['d', 'a', 'c'], ['m', 'h', 'l'], ['l', 'm', 'g'], ['j', 'd', 'k'], ['i', 'j', 'e'], ['k', 'd', 'e'], ['g', 'l', 'f'], ['i', 'e', 'f']]
Coordinate Data:
k : [28131237 / 2000000000, -4611884569 / 5000000000, 1699053937 / 2000000000]
e : [-377702897 / 2000000000, 270684907 / 5000000000, 1152439059 / 1250000000]
b : [10954361341 / 10000000000, 6088055631 / 10000000000, 1179281279 / 5000000000]
f : [-2534995617 / 10000000000, 10510833471 / 10000000000, 4390749081 / 5000000000]
m : [1269314539 / 2500000000, 2677122027 / 1250000000, -820259601 / 5000000000]
c : [14091029523 / 10000000000, 4349047 / 200000000, 982162693 / 1000000000]
a : [6157736863 / 10000000000, 123250269 / 200000000, 11132777603 / 10000000000]
h : [6418663867 / 10000000000, 11898945781 / 10000000000, -4398730101 / 10000000000]
g : [6046720837 / 10000000000, 2857559909 / 2000000000, 2652310847 / 5000000000]
l : [-279840179 / 1250000000, 14737457059 / 10000000000, -34566253 / 1250000000]
j : [62404181 / 100000000, -2522355117 / 10000000000, 213316359 / 500000000]
d : [1462137947 / 2500000000, -1671188033 / 5000000000, 2844988373 / 2000000000]
i : [536726637 / 5000000000, 5387133813 / 10000000000, 494379027 / 5000000000]
Desired square lengths:
default : 1
Checking inequality 1:
d = 3
|V| = 13
|E| = 33
Success: d|V| >= |E|
Checking self-intersection:
Square collision distance = 499999999662295877922000680184903413436932987289158950424161 / 999999999786149730235845953028688684601800000000000000000000
Collision distance in [35355339 / 50000000, 70710679 / 100000000] ~ [0.70711, 0.70711]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [1559 / 2000, 7797 / 10000] ~ [0.7795, 0.7797]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 3205123793613850105533 / 2000000000000000000000000000000000000000
rho in [126592333 / 100000000000000000, 1126592333 / 100000000000000000] ~ [0.0, 0.0]
sigma_min ^ 2 / (16 * E ^ .5) in [12152405 / 1838260048, 60793209 / 9191300224] ~ [0.00661, 0.00661]
Success: rho < sigma_min ^ 2 / (16 * E ^ .5)
Checking inequality 4:
LHS NUM := sigma_min - [sigma_min ^ 2 - 16 * rho * |E| ^ .5 ] ^ .5 in [-19993 / 100000000, 20067 / 100000000] ~ [-0.0002, 0.0002]
LHS DEN := 8 * |E| ^ .5 in [71807033 / 1562500, 114891253 / 2500000] ~ [45.9565, 45.9565]
LHS := (LHS NUM) / (LHS DEN) in [-19993 / 4595650112, 20067 / 4595650112] ~ [-0.0, 0.0]
CD / |V| ^ .5 in [35355339 / 180277564, 70710679 / 360555127] ~ [0.19612, 0.19612]
Success: LHS < CD / |V| ^ .5
Success: existence proven