show/hide visualization coordinates
a : (0.6632052349769231, 0.38246583543846147, 0.035308339761538465)
b : (0.5846181788769231, -0.6060530061615385, 0.1643609406615384)
c : (0.795187936776923, -0.23506308176153845, -0.7400874300384617)
d : (0.04068861397692308, 0.42120797163846146, -0.7463387050384616)
e : (0.0960470137769231, 1.1927005608384615, -0.11251330743846155)
f : (0.07464805377692307, 0.7214871905384614, 0.7692463228615384)
g : (0.7323678931769231, -0.009049905161538474, 0.9528768386615385)
h : (-0.1980090172230769, -0.23485794086153855, 0.6640697516615384)
i : (-0.25145914802307695, -1.1467596538615386, 0.2571565566615384)
j : (-0.13363528772307692, -0.5390103929615385, -0.5281830975384616)
k : (-0.8877800272230769, 0.05499081223846147, -0.8082335893384616)
l : (-0.5663625042230769, 0.4608114759384615, 0.04733660846153842)
m : (-0.9495169409230768, -0.46286986586153855, 0.0450007706615384)
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'], ['b', 'g', 'a'], ['g', 'a', 'f'], ['d', 'a', 'e'], ['b', 'h', 'g'], ['h', 'g', 'f'], ['m', 'i', 'h'], ['b', 'i', 'j'], ['m', 'k', 'l'], ['m', 'i', 'j'], ['e', 'a', 'f'], ['k', 'd', 'l'], ['j', 'd', 'c'], ['e', 'l', 'f'], ['b', 'i', 'h'], ['d', 'a', 'c'], ['m', 'h', 'l'], ['j', 'd', 'k'], ['d', 'l', 'e'], ['m', 'j', 'k'], ['h', 'l', 'f']]
Coordinate Data:
k : [13549896851 / 10000000000, 707650459 / 1250000000, 13451014977 / 10000000000]
e : [3711626441 / 10000000000, -2857946907 / 5000000000, 3246906079 / 5000000000]
b : [-117408521 / 1000000000, 47936101 / 39062500, 3725069677 / 10000000000]
f : [3925616041 / 10000000000, -1003760111 / 10000000000, -464756829 / 2000000000]
m : [3541816497 / 2500000000, 10839810453 / 10000000000, 4918671377 / 10000000000]
c : [-3279782789 / 10000000000, 2140435653 / 2500000000, 1596194173 / 1250000000]
a : [-1959955771 / 10000000000, 7457667 / 31250000, 2507797843 / 5000000000]
h : [6652186751 / 10000000000, 8559691203 / 10000000000, -1272018433 / 10000000000]
g : [-2651582353 / 10000000000, 3150805423 / 5000000000, -4160089303 / 10000000000]
l : [10335721621 / 10000000000, 320599407 / 2000000000, 4895312999 / 10000000000]
j : [375528091 / 625000000, 2900303931 / 2500000000, 10650510059 / 10000000000]
d : [4265210439 / 10000000000, 999516039 / 5000000000, 6416033067 / 5000000000]
i : [7186688059 / 10000000000, 17678708333 / 10000000000, 2797113517 / 10000000000]
Desired square lengths:
default : 1
Checking inequality 1:
d = 3
|V| = 13
|E| = 33
Success: d|V| >= |E|
Checking self-intersection:
Square collision distance = 9764199964032655449787764734032518531542940846716429569 / 16195972741537286102134559276179682052000000000000000000
Collision distance in [15529047 / 20000000, 19411309 / 25000000] ~ [0.77645, 0.77645]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [3687 / 5000, 461 / 625] ~ [0.7374, 0.7376]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 985594587469608956738739 / 10000000000000000000000000000000000000000
rho in [198554233 / 20000000000000000, 398554233 / 20000000000000000] ~ [0.0, 0.0]
sigma_min ^ 2 / (16 * E ^ .5) in [13593969 / 2297825060, 425042 / 71807033] ~ [0.00592, 0.00592]
Success: rho < sigma_min ^ 2 / (16 * E ^ .5)
Checking inequality 4:
LHS NUM := sigma_min - [sigma_min ^ 2 - 16 * rho * |E| ^ .5 ] ^ .5 in [-19939 / 100000000, 161 / 800000] ~ [-0.0002, 0.0002]
LHS DEN := 8 * |E| ^ .5 in [71807033 / 1562500, 114891253 / 2500000] ~ [45.9565, 45.9565]
LHS := (LHS NUM) / (LHS DEN) in [-19939 / 4595650112, 20125 / 4595650112] ~ [-0.0, 0.0]
CD / |V| ^ .5 in [77645235 / 360555128, 77645236 / 360555127] ~ [0.21535, 0.21535]
Success: LHS < CD / |V| ^ .5
Success: existence proven