show/hide visualization coordinates
a : (-0.7577993171076922, -0.5946573279538463, -0.4665276070769231)
b : (-0.4909622829076923, -0.11648879675384621, 0.37022439262307694)
c : (-1.3757419893076923, 0.07502635944615382, -0.054612748176923076)
d : (-1.7476156934076923, -0.7103100019538462, -0.5495417180769231)
e : (-1.2862224755076923, 0.022784498646153784, -1.0492278606769232)
f : (-0.5322280760076923, 0.3790764900461538, -0.4973712396769231)
g : (0.1884203676923077, -0.29639486295384615, -0.34115545427692306)
h : (0.4647286141923077, -0.27289355965384615, 0.6196282190230769)
i : (0.20126661279230768, 0.5721353004461538, 0.15431944992307692)
j : (1.0605686764923077, 0.11838963674615383, -0.0817062707769231)
k : (1.4573515158923076, -0.29191527645384624, 0.7393965103230768)
l : (0.9626137038923077, 0.5748185746461538, 0.8026497305230769)
m : (1.8556203432923077, 0.5404289657461538, 0.35392459632307693)
show/hide computer existence proof
(see shape-existence, preprint)
Attempting to prove existence
Starting realization:
Abstract data:
mode: maximal_simplices
data: [['d', 'e', 'c'], ['b', 'a', 'c'], ['j', 'g', 'h'], ['b', 'g', 'a'], ['g', 'a', 'f'], ['d', 'a', 'e'], ['b', 'h', 'g'], ['h', 'l', 'k'], ['i', 'j', 'g'], ['m', 'k', 'l'], ['i', 'h', 'l'], ['e', 'a', 'f'], ['b', 'i', 'h'], ['d', 'a', 'c'], ['f', 'e', 'c'], ['i', 'j', 'l'], ['b', 'c', 'f'], ['m', 'j', 'l'], ['m', 'j', 'k'], ['b', 'i', 'f'], ['h', 'j', 'k'], ['i', 'g', 'f']]
Coordinate Data:
k : [-4758148909 / 5000000000, 7628715377 / 10000000000, -3399437803 / 10000000000]
e : [1119965131 / 625000000, 2240858813 / 5000000000, 14486805907 / 10000000000]
b : [996684017 / 1000000000, 293722529 / 500000000, 146141687 / 5000000000]
f : [10379498101 / 10000000000, 57424857 / 625000000, 8968239697 / 10000000000]
m : [-3374746523 / 2500000000, -138945409 / 2000000000, 455281337 / 10000000000]
c : [9407318617 / 5000000000, 1979649509 / 5000000000, 2270327391 / 5000000000]
a : [789700657 / 625000000, 2664033973 / 2500000000, 8659803371 / 10000000000]
h : [409931199 / 10000000000, 7438498209 / 10000000000, -220175489 / 1000000000]
g : [99156677 / 312500000, 3836755621 / 5000000000, 7406081843 / 10000000000]
l : [-2284459849 / 5000000000, -519311567 / 5000000000, -806394001 / 2000000000]
j : [-346779339 / 625000000, 705133249 / 2000000000, 601448751 / 1250000000]
d : [901334971 / 400000000, 1476582829 / 1250000000, 9489944481 / 10000000000]
i : [3044551213 / 10000000000, -126473799 / 1250000000, 2451332801 / 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 = 7812454176386218547611823289771765465915157212769830596161 / 15625235182939557277441368928687821453076562500000000000000
Collision distance in [35354969 / 50000000, 70709939 / 100000000] ~ [0.7071, 0.7071]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [5251 / 10000, 5253 / 10000] ~ [0.5251, 0.5253]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 11757280463717719094875114317103 / 10000000000000000000000000000000000000000
rho in [34288891 / 1000000000000, 34298891 / 1000000000000] ~ [3e-05, 3e-05]
sigma_min ^ 2 / (16 * E ^ .5) in [27573001 / 9191300240, 27594009 / 9191300224] ~ [0.003, 0.003]
Success: rho < sigma_min ^ 2 / (16 * E ^ .5)
Checking inequality 4:
LHS NUM := sigma_min - [sigma_min ^ 2 - 16 * rho * |E| ^ .5 ] ^ .5 in [280841 / 100000000, 160523 / 50000000] ~ [0.00281, 0.00321]
LHS DEN := 8 * |E| ^ .5 in [71807033 / 1562500, 114891253 / 2500000] ~ [45.9565, 45.9565]
LHS := (LHS NUM) / (LHS DEN) in [280841 / 4595650120, 160523 / 2297825056] ~ [6e-05, 7e-05]
CD / |V| ^ .5 in [35354969 / 180277564, 70709939 / 360555127] ~ [0.19611, 0.19611]
Success: LHS < CD / |V| ^ .5
Success: existence proven