show/hide visualization coordinates
a : (0.12173124475000002, 0.2385938073833333, -0.41775341915833336)
b : (0.32111735325000007, -0.49845621471666673, -1.0635106836583335)
c : (-0.61536491595, -0.16296693251666672, -0.9612957100583335)
d : (-0.7545420711499999, 0.02043307038333325, 0.011840538441666604)
e : (-0.15313061384999999, 0.7056523801833332, 0.42266745634166664)
f : (0.7833516554500002, 0.3701630979833333, 0.32045248274166666)
g : (0.72759989005, -0.5105355971166667, -0.14993198665833338)
h : (-0.22738102534999996, -0.7791413894166668, -0.27587792575833336)
i : (-1.21627449585, -0.7531319802166667, -0.42221047265833334)
j : (0.044827129050000025, -0.26761453211666675, 0.5391331140416666)
k : (0.35564737055, 0.3913076635833333, 1.2241238566416666)
l : (0.61241847905, 1.2456966265833334, 0.7723627497416665)
show/hide computer existence proof
(see shape-existence, preprint)
Attempting to prove existence
Starting realization:
Abstract data:
mode: maximal_simplices
data: [['c', 'b', 'a'], ['h', 'j', 'd'], ['j', 'd', 'e'], ['c', 'd', 'a'], ['h', 'c', 'b'], ['h', 'b', 'g'], ['e', 'a', 'f'], ['j', 'k', 'f'], ['h', 'c', 'i'], ['b', 'a', 'g'], ['l', 'e', 'k'], ['e', 'l', 'f'], ['h', 'j', 'g'], ['g', 'a', 'f'], ['d', 'e', 'a'], ['g', 'j', 'f'], ['c', 'd', 'i'], ['k', 'l', 'f'], ['h', 'd', 'i'], ['j', 'e', 'k']]
Coordinate Data:
a : [5828079999 / 10000000000, 887313519 / 1250000000, -81430287 / 1250000000]
e : [3079461413 / 10000000000, 294227347 / 250000000, 7752766459 / 10000000000]
k : [8167241257 / 10000000000, 4312823357 / 5000000000, 7883665231 / 5000000000]
i : [-7551977407 / 10000000000, -704687431 / 2500000000, -696012831 / 10000000000]
d : [-73366329 / 250000000, 2458450391 / 5000000000, 5694527 / 15625000]
g : [2971691613 / 2500000000, -392785893 / 10000000000, 2026772029 / 10000000000]
c : [-192860201 / 1250000000, 3082900753 / 10000000000, -1217373041 / 2000000000]
j : [2529519421 / 5000000000, 2036424757 / 10000000000, 2229355759 / 2500000000]
l : [5367476171 / 5000000000, 2146192043 / 1250000000, 11249719393 / 10000000000]
f : [6222142053 / 5000000000, 4207100529 / 5000000000, 6730616723 / 10000000000]
h : [1168478649 / 5000000000, -384855477 / 1250000000, 383656319 / 5000000000]
b : [1955485271 / 2500000000, -271992069 / 10000000000, -7109014941 / 10000000000]
Desired square lengths:
default : 1
Checking inequality 1:
d = 3
|V| = 12
|E| = 30
Success: d|V| >= |E|
Checking self-intersection:
Square collision distance = 13888888877961910986436718574665715370809622785450606921801 / 27777777764999175372373752767053090256600000000000000000000
Collision distance in [35355339 / 50000000, 70710679 / 100000000] ~ [0.70711, 0.70711]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [7663 / 10000, 1533 / 2000] ~ [0.7663, 0.7665]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 9403678567006582956617 / 10000000000000000000000000000000000000000
rho in [48486283 / 50000000000000000, 548486283 / 50000000000000000] ~ [0.0, 0.0]
sigma_min ^ 2 / (16 * E ^ .5) in [58721569 / 8763560928, 58752225 / 8763560912] ~ [0.0067, 0.0067]
Success: rho < sigma_min ^ 2 / (16 * E ^ .5)
Checking inequality 4:
LHS NUM := sigma_min - [sigma_min ^ 2 - 16 * rho * |E| ^ .5 ] ^ .5 in [-3999 / 20000000, 20063 / 100000000] ~ [-0.0002, 0.0002]
LHS DEN := 8 * |E| ^ .5 in [547722557 / 12500000, 273861279 / 6250000] ~ [43.8178, 43.8178]
LHS := (LHS NUM) / (LHS DEN) in [-19995 / 4381780456, 20063 / 4381780456] ~ [-0.0, 0.0]
CD / |V| ^ .5 in [1309457 / 6415003, 70710679 / 346410161] ~ [0.20412, 0.20412]
Success: LHS < CD / |V| ^ .5
Success: existence proven