show/hide visualization coordinates
a : (-0.067902721528267, -0.03010998286461405, -1.1098272478971487)
b : (0.932097278471733, -0.03010998286461405, -1.1098272478971487)
c : (0.432097278471733, -0.8951587617602622, -1.0687102181996122)
d : (-0.3603796052979632, -0.7470877535904189, -0.4770554495800755)
e : (-1.000260764909342, -0.028074343296117743, -0.7482967026950029)
f : (-0.5626612014524577, 0.8328892278930932, -1.0076195731624278)
g : (0.432097278471733, 0.8359154209198245, -1.1098272478971487)
h : (0.7917877578754559, 0.46623254683888377, -0.25311415027486106)
i : (0.8692374195706084, -0.5307414578754467, -0.24645203145448935)
j : (0.35624219689683884, -1.3879754425619533, -0.20188974905800827)
k : (-0.17837760203393963, -0.9072009613498204, 0.49311929318994596)
l : (-0.8903265858563225, -0.2611357137365456, 0.2179314659506686)
m : (-0.8812248028071926, 0.6966022084545552, -0.06956676003063977)
n : (0.018177626907809066, 1.0997276873023725, -0.23857894221426057)
o : (0.557372569279477, 0.9498933683786114, 0.5901661880842326)
p : (0.7355938443786735, -0.03387599184097218, 0.6110233929585152)
q : (0.8061318703804631, -1.031367723617664, 0.6169082824993157)
r : (0.2689349656626237, -0.5639563517511281, 1.319009482477934)
s : (-0.7128476343045398, -0.42623203579870067, 1.188108988983247)
t : (-1.0563224144135486, 0.46333484567967065, 0.8869514906440665)
u : (-0.41029370865260273, 1.1922005250788479, 0.6602319883360097)
v : (-0.07917304511097221, 0.3362306723623985, 1.0573147472368842)
show/hide computer existence proof
(see shape-existence, preprint)
Attempting to prove existence
Starting realization:
Abstract data:
mode: maximal_simplices
data: [['o', 'p', 'h'], ['d', 'k', 'l'], ['d', 'e', 'l'], ['k', 'j', 'q'], ['i', 'p', 'h'], ['f', 'e', 'm'], ['d', 'a', 'c'], ['i', 'j', 'q'], ['m', 't', 'l'], ['i', 'j', 'c'], ['f', 'g', 'a'], ['i', 'b', 'c'], ['v', 't', 'u'], ['e', 'm', 'l'], ['r', 'v', 's'], ['g', 'b', 'h'], ['r', 'k', 's'], ['r', 'v', 'p'], ['f', 'm', 'n'], ['s', 't', 'l'], ['k', 's', 'l'], ['b', 'a', 'c'], ['g', 'b', 'a'], ['o', 'v', 'u'], ['r', 'q', 'p'], ['m', 'n', 'u'], ['o', 'v', 'p'], ['m', 't', 'u'], ['o', 'n', 'u'], ['i', 'b', 'h'], ['g', 'n', 'h'], ['r', 'k', 'q'], ['i', 'q', 'p'], ['f', 'e', 'a'], ['v', 's', 't'], ['d', 'e', 'a'], ['d', 'k', 'j'], ['d', 'j', 'c'], ['f', 'g', 'n'], ['o', 'n', 'h']]
Coordinate Data:
a : [-179790501382815847871778373513 / 10000000000000000000000000000000000000000000000000000000000, -52417735115466700858884442437 / 5000000000000000000000000000000000000000000000000000000000, 460227092151547526156913388383 / 500000000000000000000000000000000000000000000000000000000000000000000000000]
h : [859690479403722864174277588367 / 1000000000000000000000000000000, 248171264851748909815318600143 / 500000000000000000000000000000, 85671309762228759031684681557 / 100000000000000000000000000000]
p : [803496565906940544870661242287 / 1000000000000000000000000000000, -188300448817906654356754543 / 50000000000000000000000000000, 86042532042783190879075838731 / 50000000000000000000000000000]
o : [625275290807744047798871540033 / 1000000000000000000000000000000, 490001675621612705532107831987 / 500000000000000000000000000000, 169999343598138123354904814893 / 100000000000000000000000000000]
s : [-644944912776272779075044453313 / 1000000000000000000000000000000, -198061026467043310408524564383 / 500000000000000000000000000000, 11489681184401978124573694641 / 5000000000000000000000000000]
m : [-406661040639462816257706990647 / 500000000000000000000000000000, 726712191319169294939464970951 / 1000000000000000000000000000000, 2600651219666272419900191343 / 2500000000000000000000000000]
q : [218508647977182516671843166211 / 250000000000000000000000000000, -100125774075304982409743659171 / 100000000000000000000000000000, 172673553039646448459888736083 / 100000000000000000000000000000]
r : [13473507487635627432986734001 / 40000000000000000000000000000, -5338463688865140838662978299 / 10000000000000000000000000000, 121441836518754134726609563497 / 50000000000000000000000000000]
k : [-110474880505672629818296320777 / 1000000000000000000000000000000, -877090978485206326868017492609 / 1000000000000000000000000000000, 20036831763588682461329155997 / 12500000000000000000000000000]
g : [500000000000000000000000000007 / 1000000000000000000000000000000, 433012701892219323381861585381 / 500000000000000000000000000000, -18671760283806931674861372843 / 50000000000000000000000000000000000000000000000000000000000000000000000000]
c : [500000000000000000000000000059 / 1000000000000000000000000000000, -173009755779129623391202493149 / 200000000000000000000000000000, 20558514848768241071466894627 / 500000000000000000000000000000]
f : [-247379239962095329712998824259 / 500000000000000000000000000000, 431499605378853648169522450557 / 500000000000000000000000000000, 102207674734721028878153447163 / 1000000000000000000000000000000]
u : [-171195493562167860649297151033 / 500000000000000000000000000000, 61115525397173100556634561191 / 50000000000000000000000000000, 22125740452914479835934024707 / 12500000000000000000000000000]
b : [100000000000000000000000000001 / 100000000000000000000000000000, 152597364288222349637584884937 / 100000000000000000000000000000000000000000000000000000000000, -547018977908442252416304151181 / 1000000000000000000000000000000000000000000000000000000000000000000000000000]
j : [106036229606276449152373988397 / 250000000000000000000000000000, -33946636492433478961009851857 / 25000000000000000000000000000, 907937498839140400230239426089 / 1000000000000000000000000000000]
i : [468570070549437699449941515289 / 500000000000000000000000000000, -62578934376354071061851347827 / 125000000000000000000000000000, 431687608221329661023590969741 / 500000000000000000000000000000]
l : [-82242386432805552201551392221 / 100000000000000000000000000000, -231025730871931563742949957597 / 1000000000000000000000000000000, 132775871384781725819071972933 / 100000000000000000000000000000]
n : [86080348436076058230663066897 / 1000000000000000000000000000000, 56491883508349331126278818011 / 50000000000000000000000000000, 174249661136577633635109215079 / 200000000000000000000000000000]
d : [-73119220942424055351665382201 / 250000000000000000000000000000, -716977770725804844891619289089 / 1000000000000000000000000000000, 632771798317073252450218205081 / 1000000000000000000000000000000]
t : [-494209846442640742160217235067 / 500000000000000000000000000000, 6168060356803558184455938773 / 12500000000000000000000000000, 99838936927060759242914239167 / 50000000000000000000000000000]
e : [-466179021690537479698867914819 / 500000000000000000000000000000, 1017819784248154596972423591 / 500000000000000000000000000000, 361530545202145701427902259921 / 1000000000000000000000000000000]
v : [-5635161791352609565354754997 / 500000000000000000000000000000, 22896290951688282346339854727 / 62500000000000000000000000000, 216714199513403296656938492221 / 100000000000000000000000000000]
Desired square lengths:
default : 1
Checking inequality 1:
d = 3
|V| = 22
|E| = 60
Success: d|V| >= |E|
Checking self-intersection:
Square collision distance = 5593672648476315437440301925014838941175497283976275810972487987989601777993339335981768227871427520269740472755046881 / 9063818438557829100487462860330280199089546285563849720021132454888920253008962500000000000000000000000000000000000000
Collision distance in [785584534103681 / 1000000000000000, 392792267051841 / 500000000000000] ~ [0.78558, 0.78558]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [47571516002872489999 / 100000000000000000000, 47571516002872490001 / 100000000000000000000] ~ [0.47572, 0.47572]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 74292246348031125346707149679662057985349234964079306583715153825991220313522173046671776756729926123178118475708392162853170638622867508587436523511949973649487607232941089240861733401872304642146271728816993934117851081100632308365961063558690609 / 200000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000
rho in [96366647723701 / 5000000000000000000000000000000000000000, 5000000000096366647723701 / 5000000000000000000000000000000000000000] ~ [0.0, 0.0]
sigma_min ^ 2 / (16 * E ^ .5) in [2263049134811553407902788166794355020001 / 1239354670786373440000000000000000000000000, 754349711603851136031024743601948326667 / 413118223595457760000000000000000000000000] ~ [0.00183, 0.00183]
Success: rho < sigma_min ^ 2 / (16 * E ^ .5)
Checking inequality 4:
LHS NUM := sigma_min - [sigma_min ^ 2 - 16 * rho * |E| ^ .5 ] ^ .5 in [-7127510001 / 100000000000000000000, 2872490001 / 100000000000000000000] ~ [-0.0, 0.0]
LHS DEN := 8 * |E| ^ .5 in [7745966692414833 / 125000000000000, 3872983346207417 / 62500000000000] ~ [61.96773, 61.96773]
LHS := (LHS NUM) / (LHS DEN) in [-2375836667 / 2065591117977288800000, 957496667 / 2065591117977288800000] ~ [-0.0, 0.0]
CD / |V| ^ .5 in [60429579546437 / 360801212294110, 261861511367894 / 1563471919941143] ~ [0.16749, 0.16749]
Success: LHS < CD / |V| ^ .5
Success: existence proven