show/hide visualization coordinates
a : (-0.12589609242896221, 0.8868093695824006, -0.2581635801457941)
b : (-0.5943577512573286, 0.8280046870551236, -1.1396882159448407)
c : (-1.0943864026517807, 1.1262565510112612, -0.3266585895281058)
d : (-0.635684843287498, 1.1475329465876016, 0.5616770421044739)
e : (0.32434131284480744, 0.8773141762204217, 0.6346948185912967)
f : (0.8306499366017797, 0.6049454934300809, -0.18351473778431515)
g : (0.3808227095544736, 0.6157819819985283, -1.0765645887570576)
h : (-0.29039705432558444, -0.12439833978515025, -1.116528570303061)
i : (-1.0865649738292655, 0.15948518993972405, -0.5821815056492666)
j : (-1.2979376797550684, 0.42644994274664916, 0.3580585700486061)
k : (-0.3965741618586099, 0.18964108124883755, 0.7206401080803031)
l : (0.5486585267487346, -0.04596330329773035, 0.946528882415293)
m : (1.2802336926560274, 0.5933215568928312, 0.70964780643232)
n : (1.0513931202514197, -0.266833204831313, 0.25383449124197566)
o : (0.5689154222426859, -0.2548411230157416, -0.6219916678203817)
p : (0.030756866774727387, -1.0479860723504748, -0.9071345416949427)
q : (-0.9309433257096305, -0.8101377984978243, -0.7708960067613072)
r : (-0.9040919713131095, -0.47334576685497665, 0.17030011105312343)
s : (-0.09626712944523147, -0.7634732568806374, 0.6833742425317508)
t : (0.850095740506427, -0.9985464700427423, 0.9050449506338905)
u : (1.5003005363466069, -0.2784574397854198, 1.14733715432501)
v : (0.5260606697285742, -1.065900293679571, -0.03859943966761015)
w : (-0.43912714839419736, -1.325659907691882, -0.06921673340135914)
show/hide computer existence proof
(see shape-existence, preprint)
Attempting to prove existence
Starting realization:
Abstract data:
mode: maximal_simplices
data: [['q', 'r', 'w'], ['t', 'u', 'n'], ['j', 'r', 'i'], ['l', 'u', 'm'], ['g', 'o', 'f'], ['q', 'r', 'i'], ['p', 'q', 'w'], ['r', 's', 'w'], ['h', 'q', 'i'], ['r', 's', 'k'], ['l', 's', 'k'], ['f', 'e', 'm'], ['j', 'i', 'c'], ['j', 'd', 'k'], ['o', 'v', 'n'], ['a', 'f', 'e'], ['e', 'd', 'k'], ['h', 'i', 'b'], ['g', 'a', 'f'], ['l', 'e', 'm'], ['l', 'u', 't'], ['h', 'o', 'p'], ['l', 's', 't'], ['o', 'n', 'f'], ['o', 'p', 'v'], ['t', 'v', 'n'], ['n', 'f', 'm'], ['i', 'b', 'c'], ['s', 'v', 'w'], ['h', 'p', 'q'], ['a', 'b', 'c'], ['g', 'a', 'b'], ['a', 'd', 'c'], ['u', 'n', 'm'], ['t', 's', 'v'], ['a', 'd', 'e'], ['g', 'b', 'h'], ['j', 'd', 'c'], ['l', 'k', 'e'], ['j', 'r', 'k'], ['p', 'v', 'w'], ['g', 'o', 'h']]
Coordinate Data:
s : [7035350562208138211 / 12500000000000000000, 133049923743633412073 / 100000000000000000000, -2333378176496520567 / 12500000000000000000]
b : [21218373335774966627 / 20000000000000000000, -407779228905354737 / 1562500000000000000, 81819610217843480499 / 50000000000000000000]
j : [176449859528648801743 / 100000000000000000000, 3514400945226187691 / 25000000000000000000, 6932270918171150271 / 50000000000000000000]
m : [-16273455542492157341 / 20000000000000000000, -2629557633713457589 / 100000000000000000000, -21294381802029082579 / 100000000000000000000]
k : [43156753869501473813 / 50000000000000000000, 9434622482671476733 / 25000000000000000000, -5598402991706850763 / 25000000000000000000]
q : [6987521206205251071 / 5000000000000000000, 6885818895267605163 / 5000000000000000000, 126759999517333626133 / 100000000000000000000]
u : [-51686981040759362603 / 50000000000000000000, 84548342034111640113 / 100000000000000000000, -508307160869516231 / 781250000000000000]
g : [171476411953892023 / 2000000000000000000, -4875600144283169451 / 100000000000000000000, 78663428858454327871 / 50000000000000000000]
c : [78047365909160019097 / 50000000000000000000, -13980764261389114437 / 25000000000000000000, 41168128897006746237 / 50000000000000000000]
w : [90568806392561701167 / 100000000000000000000, 189268588824757845451 / 100000000000000000000, 56592072181338820969 / 100000000000000000000]
i : [155312588936068525221 / 100000000000000000000, 8150815812319452273 / 20000000000000000000, 215777098812259151 / 200000000000000000]
f : [-36408902107036001873 / 100000000000000000000, -1895975643719210041 / 50000000000000000000, 34010936309817211031 / 50000000000000000000]
t : [-38353482497500739101 / 100000000000000000000, 78278622529921945709 / 50000000000000000000, -40834096222186138693 / 100000000000000000000]
p : [21790202437834610773 / 50000000000000000000, 40375301322654283279 / 25000000000000000000, 140383853010697184501 / 100000000000000000000]
a : [11849140159207636299 / 20000000000000000000, -15989169451335198149 / 50000000000000000000, 37743378427891163183 / 50000000000000000000]
l : [-8209761121731497379 / 100000000000000000000, 6129892838534269871 / 10000000000000000000, -22491244700163191909 / 50000000000000000000]
r : [27413057736890583059 / 20000000000000000000, 10403717474106732321 / 10000000000000000000, 16320193867945285491 / 50000000000000000000]
o : [-10235450671126630829 / 100000000000000000000, 82186710357143818253 / 100000000000000000000, 2796739140581027141 / 2500000000000000000]
e : [14221960268661215437 / 100000000000000000000, -15514409783236252021 / 50000000000000000000, -3449770754481689767 / 25000000000000000000]
n : [-58483220472000005779 / 100000000000000000000, 83385918538700963647 / 100000000000000000000, 24286949717005346069 / 100000000000000000000]
v : [-5949975419715468783 / 100000000000000000000, 32658525484705352129 / 20000000000000000000, 10706068561592786021 / 20000000000000000000]
h : [75695796985700398349 / 100000000000000000000, 17285608008521171357 / 25000000000000000000, 161323255871508998139 / 100000000000000000000]
d : [22044915176378351287 / 20000000000000000000, -14512674150797625573 / 25000000000000000000, -1624326342311120387 / 25000000000000000000]
Desired square lengths:
default : 1
Checking inequality 1:
d = 3
|V| = 23
|E| = 63
Success: d|V| >= |E|
Checking self-intersection:
Square collision distance = 108346485309660672746191454033203848101957276485855053296736555771110705289743571456501266138993162633010263126173739001 / 247012041280239595918257804133539984496097947461348962770950870084813784896360130000000000000000000000000000000000000000
Collision distance in [662290234647763899891559190929 / 1000000000000000000000000000000, 66229023464776389989155919093 / 100000000000000000000000000000] ~ [0.66229, 0.66229]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [751 / 10000, 753 / 10000] ~ [0.0751, 0.0753]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 3289775775697574715863007881444637125634851 / 25000000000000000000000000000000000000000000000000000000000000000000000000000000
rho in [1813773904238776591143962566617 / 5000000000000000000000000000000000000000000000000, 1813773904243776591143962566617 / 5000000000000000000000000000000000000000000000000] ~ [0.0, 0.0]
sigma_min ^ 2 / (16 * E ^ .5) in [176250312500000000000000000 / 3968626966596885885752423630459, 118126875000000000000000000 / 2645751311064590590501615753639] ~ [4e-05, 4e-05]
Success: rho < sigma_min ^ 2 / (16 * E ^ .5)
Checking inequality 4:
LHS NUM := sigma_min - [sigma_min ^ 2 - 16 * rho * |E| ^ .5 ] ^ .5 in [-199999999999694100737203857 / 1000000000000000000000000000000, 625000000000958480962409 / 3125000000000000000000000000] ~ [-0.0002, 0.0002]
LHS DEN := 8 * |E| ^ .5 in [7937253933193771771504847260917 / 125000000000000000000000000000, 3968626966596885885752423630459 / 62500000000000000000000000000] ~ [63.49803, 63.49803]
LHS := (LHS NUM) / (LHS DEN) in [-66666666666564700245734619 / 21166010488516724724012926029112, 25000000000038339238496360 / 7937253933193771771504847260917] ~ [-0.0, 0.0]
CD / |V| ^ .5 in [662290234647763899891559190929 / 4795831523312719541597438064163, 331145117323881949945779595465 / 2397915761656359770798719032081] ~ [0.1381, 0.1381]
Success: LHS < CD / |V| ^ .5
Success: existence proven