show/hide visualization coordinates
a : (-0.3505886910615385, -0.12843659067692312, -0.4645545250538462)
b : (-0.5997814510615385, -1.000280510776923, -0.04290164605384622)
c : (-0.8423482738615384, -0.14030215877692312, 0.40609564594615377)
d : (-0.7633522586615384, 0.711387739123077, -0.11196221505384621)
e : (0.1757409048384615, 0.7217954832230769, -0.4554672424538462)
f : (0.5148134718384615, -0.07076244387692315, -0.9623022461538462)
g : (0.3372327963384615, -0.8462103634769231, -0.3563768210538462)
h : (0.15366795943846145, -1.5213176142769231, 0.35813990294615383)
i : (0.05944272263846151, -0.5456326103769231, 0.5560297153461538)
j : (-0.0439270518615385, 0.4486957924230769, 0.5310154757461538)
k : (-0.1164032317615385, 1.396952003823077, 0.22189194644615384)
l : (0.7816604733384614, 0.964468952523077, 0.30214153514615383)
m : (0.6938426298384616, 0.009642321123076891, 0.01825047424615378)
show/hide computer existence proof
(see shape-existence, preprint)
Attempting to prove existence
Starting realization:
Abstract data:
mode: maximal_simplices
data: [['b', 'a', 'c'], ['m', 'g', 'f'], ['b', 'g', 'a'], ['g', 'a', 'f'], ['d', 'a', 'e'], ['b', 'h', 'g'], ['m', 'e', 'l'], ['m', 'i', 'j'], ['e', 'a', 'f'], ['j', 'd', 'c'], ['b', 'i', 'h'], ['b', 'i', 'c'], ['d', 'a', 'c'], ['m', 'e', 'f'], ['j', 'd', 'k'], ['i', 'h', 'g'], ['j', 'l', 'k'], ['m', 'j', 'l'], ['k', 'e', 'l'], ['k', 'd', 'e'], ['m', 'i', 'g'], ['i', 'j', 'c']]
Coordinate Data:
k : [3902616493 / 10000000000, 8780214721 / 5000000000, 5718129293 / 10000000000]
m : [12005075109 / 10000000000, 737466523 / 2000000000, 3681714571 / 10000000000]
b : [-9311657 / 100000000, -801486963 / 1250000000, 383774171 / 1250000000]
f : [10214783529 / 10000000000, 576656993 / 2000000000, -6123812633 / 10000000000]
e : [6824057859 / 10000000000, 2702216059 / 2500000000, -263865649 / 2500000000]
c : [-419604241 / 1250000000, 273485977 / 1250000000, 472510393 / 625000000]
a : [15607619 / 100000000, 2306543497 / 10000000000, -573167711 / 5000000000]
h : [1320665681 / 2000000000, -11622266739 / 10000000000, 3540304429 / 5000000000]
g : [4219488387 / 5000000000, -4871194231 / 10000000000, -32279191 / 5000000000]
l : [1610406693 / 1250000000, 13235598929 / 10000000000, 326031259 / 500000000]
j : [1156844573 / 2500000000, 126216677 / 156250000, 4404682293 / 5000000000]
d : [-160429611 / 625000000, 2140957359 / 2000000000, 1189793839 / 5000000000]
i : [5661076037 / 10000000000, -18654167 / 100000000, 4529753491 / 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 = 4999999984251723779913421488492151356948376296917720244369 / 9999999998011271350202149918480828289000000000000000000000
Collision distance in [35355339 / 50000000, 70710679 / 100000000] ~ [0.70711, 0.70711]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [3607 / 5000, 451 / 625] ~ [0.7214, 0.7216]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 4267348584496613032870811 / 10000000000000000000000000000000000000000
rho in [206575617 / 10000000000000000, 306575617 / 10000000000000000] ~ [0.0, 0.0]
sigma_min ^ 2 / (16 * E ^ .5) in [13010449 / 2297825060, 406802 / 71807033] ~ [0.00566, 0.00567]
Success: rho < sigma_min ^ 2 / (16 * E ^ .5)
Checking inequality 4:
LHS NUM := sigma_min - [sigma_min ^ 2 - 16 * rho * |E| ^ .5 ] ^ .5 in [-19869 / 100000000, 5049 / 25000000] ~ [-0.0002, 0.0002]
LHS DEN := 8 * |E| ^ .5 in [71807033 / 1562500, 114891253 / 2500000] ~ [45.9565, 45.9565]
LHS := (LHS NUM) / (LHS DEN) in [-19869 / 4595650112, 5049 / 1148912528] ~ [-0.0, 0.0]
CD / |V| ^ .5 in [35355339 / 180277564, 70710679 / 360555127] ~ [0.19612, 0.19612]
Success: LHS < CD / |V| ^ .5
Success: existence proven