show/hide visualization coordinates
a : (0.2354691742956228, -0.568398744400165, 0.6953249272448168)
b : (0.6352504856493413, 0.13066350491106282, 0.10246164226232801)
c : (-0.10268376393829443, 0.3719488914479899, 0.7327269875965439)
d : (-0.5268374133461661, -0.33481699007363486, 1.298921009475038)
e : (-0.5546591692700831, -1.1777450268627707, 0.761614509707798)
f : (0.2858470262354295, -1.4948541773148751, 0.32230696138157855)
g : (0.9667127713107473, -0.8117613839817175, 0.05809857226545667)
h : (1.0808290116906745, -0.2040821951655648, -0.7278425751249147)
i : (0.5808791262935766, 0.6618385415221486, -0.7430540795093123)
j : (0.27886482088431014, 1.0648207701846164, 0.12088612832360746)
k : (-0.5925080936119069, 1.2307465519704217, 0.5825980285613399)
l : (-1.0646993871923207, 0.45113369463526565, 0.9939849206040603)
m : (-0.9367064642221619, -0.333033396257712, 0.38677837812448557)
n : (-0.35266841829893586, -0.9128728638741361, -0.18127597905313664)
o : (0.578805154734737, -1.0437684181121945, -0.5207216103707223)
p : (1.1309941611615442, -1.7801250160164297, -0.129740457494684)
q : (1.562076452919084, -1.0801985341821159, -0.6991884162759123)
r : (0.08087912629357669, -0.20417124713456647, -0.7378535073531243)
s : (-0.4191208737064233, 0.6618385415221486, -0.7430540795093123)
t : (0.08087912629357669, 1.5278639453065872, -0.7430540795093123)
u : (-0.11796045005687883, 1.9827055535348017, 0.12503689170346488)
v : (-0.8389732071310766, 1.4815906684343905, -0.35352812589295896)
w : (-1.080602976827315, 0.5788152956565263, 0.002297225511815437)
x : (-0.9100662201606573, -0.19813796575008125, -0.6037232726689415)
show/hide computer existence proof
(see shape-existence, preprint)
Attempting to prove existence
Starting realization:
Abstract data:
mode: maximal_simplices
data: [['w', 'k', 'l'], ['n', 'r', 'x'], ['q', 'p', 'g'], ['q', 'h', 'g'], ['q', 'p', 'o'], ['u', 't', 'j'], ['f', 'a', 'g'], ['m', 'd', 'l'], ['a', 'e', 'd'], ['b', 'a', 'g'], ['b', 'i', 'j'], ['w', 's', 'v'], ['k', 'j', 'c'], ['b', 'h', 'g'], ['r', 'h', 'o'], ['u', 'k', 'v'], ['q', 'h', 'o'], ['f', 'a', 'e'], ['k', 'c', 'l'], ['w', 's', 'x'], ['m', 'e', 'd'], ['i', 's', 'r'], ['f', 'p', 'o'], ['b', 'c', 'j'], ['a', 'd', 'c'], ['n', 'r', 'o'], ['f', 'n', 'e'], ['u', 't', 'v'], ['m', 'n', 'x'], ['i', 't', 'j'], ['x', 's', 'r'], ['f', 'p', 'g'], ['m', 'n', 'e'], ['i', 'r', 'h'], ['b', 'a', 'c'], ['i', 's', 't'], ['w', 'k', 'v'], ['u', 'k', 'j'], ['w', 'm', 'l'], ['m', 'w', 'x'], ['f', 'n', 'o'], ['d', 'c', 'l'], ['b', 'i', 'h'], ['s', 't', 'v']]
Coordinate Data:
s : [-722667833566733766117834632779 / 100000000000000000000000000000000000000000000000000000000000000, 400605664612815143506158966053 / 100000000000000000000000000000000000000000000000000000000000000, 79674838738509674469003958979 / 2500000000000000000000000000000000000000000000000000000000000000000000000000000000]
v : [-209926166712326647119526311861 / 500000000000000000000000000000, 409876063456120927438200942011 / 500000000000000000000000000000, 389525953616353375663985171489 / 1000000000000000000000000000000]
r : [500000000000000000000000000001 / 1000000000000000000000000000000, -27062805895522345573035953907 / 31250000000000000000000000000, 5200572156188074158371618339 / 1000000000000000000000000000000]
k : [-173387219905483620985847380051 / 1000000000000000000000000000000, 71113501306034151941107395991 / 125000000000000000000000000000, 66282605403532610138262754991 / 50000000000000000000000000000]
h : [149994988539709779336160459177 / 100000000000000000000000000000, -17318414733754267407399468707 / 20000000000000000000000000000, 15211504384397700457828956711 / 1000000000000000000000000000000]
m : [-2587927952578692767466780977 / 5000000000000000000000000000, -19897438755597212422184731581 / 20000000000000000000000000000, 112983245763379798676966029331 / 100000000000000000000000000000]
d : [-107716539639742731572464440559 / 1000000000000000000000000000000, -199331106319156702503967944737 / 200000000000000000000000000000, 51049377224608765317763208081 / 25000000000000000000000000000]
p : [155011503486796763190273701327 / 100000000000000000000000000000, -244196355753857819731889946657 / 100000000000000000000000000000, 306656811007314152181695273381 / 500000000000000000000000000000]
o : [997926028441160385995565917443 / 1000000000000000000000000000000, -170560695963434306875762906277 / 100000000000000000000000000000, 11116623456929501514914757717 / 50000000000000000000000000000]
g : [69291682250858534749067546653 / 50000000000000000000000000000, -36839998137596650553778442489 / 25000000000000000000000000000, 801152651774769029825180361523 / 1000000000000000000000000000000]
a : [654590048002046099181523626849 / 1000000000000000000000000000000, -123023728592231367743191184273 / 100000000000000000000000000000, 719189503377064591129169239 / 500000000000000000000000000]
w : [-26459284124835673101877911771 / 40000000000000000000000000000, -8302324586562227050607114523 / 100000000000000000000000000000, 186337826255281945523281889543 / 250000000000000000000000000000]
t : [1 / 2, 866025403784438646763723170753 / 1000000000000000000000000000000, -849773994223524357298133659789 / 10000000000000000000000000000000000000000000000000000000000000000000000000000000000]
l : [-322789256742948658087050198979 / 500000000000000000000000000000, -210704846886882981167945432723 / 1000000000000000000000000000000, 86851950005668634141743126581 / 50000000000000000000000000000]
n : [8306556925935932573288571007 / 125000000000000000000000000000, -157471140539628467066372636589 / 100000000000000000000000000000, 561778100456175708322501240771 / 1000000000000000000000000000000]
x : [-245472673227116959850724447987 / 500000000000000000000000000000, -859976507272229799043502956859 / 1000000000000000000000000000000, 139330806840370782403728122309 / 1000000000000000000000000000000]
f : [704967899941852835572127247971 / 1000000000000000000000000000000, -13479329492731398699751353963 / 6250000000000000000000000000, 1331701301113613663990846623 / 1250000000000000000000000000]
e : [-27107659112731950158771823771 / 200000000000000000000000000000, -2299479460481149088754729933 / 1250000000000000000000000000, 75233429460855516519804465063 / 50000000000000000000000000000]
b : [3294910497986764747991533499 / 3125000000000000000000000000, -2124700146444343095649971291 / 4000000000000000000000000000, 169103144354328075756623962303 / 200000000000000000000000000000]
i : [1, -52542919832780578488869785643 / 5000000000000000000000000000000000000000000000000000000000000, 6450398335029556720522577411 / 50000000000000000000000000000000000000000000000000000000000000000000000000000000]
u : [75290105912386125202561699337 / 250000000000000000000000000000, 132086701201265306598597967541 / 100000000000000000000000000000, 868090971212777265617149645911 / 1000000000000000000000000000000]
q : [24764966582818843828210490269 / 12500000000000000000000000000, -43550926892606614389954317171 / 25000000000000000000000000000, 21932831616699989861618758749 / 500000000000000000000000000000]
c : [316437109768128901382424111787 / 1000000000000000000000000000000, -289889650074158667524634212431 / 1000000000000000000000000000000, 73789053355292816237229323987 / 50000000000000000000000000000]
j : [697985694590733422159553012817 / 1000000000000000000000000000000, 201491114331233928572162775287 / 500000000000000000000000000000, 863940207832919836816118746429 / 1000000000000000000000000000000]
Desired square lengths:
default : 1
Checking inequality 1:
d = 3
|V| = 24
|E| = 66
Success: d|V| >= |E|
Checking self-intersection:
Square collision distance = 3317796453061575766445377241319145541090735914986872016580459282754255694956217609126807593774044703252587420631028801 / 9469464556084736848110931452107844744682556666237970437096673777743116378330239200000000000000000000000000000000000000
Collision distance in [591918832678810017461841437789 / 1000000000000000000000000000000, 59191883267881001746184143779 / 100000000000000000000000000000] ~ [0.59192, 0.59192]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [31996246290335905999 / 100000000000000000000, 31996246290335906001 / 100000000000000000000] ~ [0.31996, 0.31996]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 5773808581109515188052361227732455830341573460868690321423720805650517535499429481173031205550622116956649906022609265757877970906627268124380399991079659934024296206082737467546609641771745866139736172052347027240137986504659452140058106405010626735449642802702606413259566469 / 10000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000
rho in [600718766411824942958143572537 / 25000000000000000000000000000000000000000000000000000000, 600743766411824942958143572537 / 25000000000000000000000000000000000000000000000000000000] ~ [0.0, 0.0]
sigma_min ^ 2 / (16 * E ^ .5) in [14419151784110341214770391834650199831 / 18307692179461319122163117900320000000000, 1023759776671834226376682805421507812001 / 1299846144741753657673581370922560000000000] ~ [0.00079, 0.00079]
Success: rho < sigma_min ^ 2 / (16 * E ^ .5)
Checking inequality 4:
LHS NUM := sigma_min - [sigma_min ^ 2 - 16 * rho * |E| ^ .5 ] ^ .5 in [-9664094001 / 100000000000000000000, 335906001 / 100000000000000000000] ~ [-0.0, 0.0]
LHS DEN := 8 * |E| ^ .5 in [4062019202317980180229941784133 / 62500000000000000000000000000, 8124038404635960360459883568267 / 125000000000000000000000000000] ~ [64.99231, 64.99231]
LHS := (LHS NUM) / (LHS DEN) in [-6040058750625000000 / 4062019202317980180229941784133, 209941250625000000 / 4062019202317980180229941784133] ~ [-0.0, 0.0]
CD / |V| ^ .5 in [591918832678810017461841437789 / 4898979485566356196394568149412, 591918832678810017461841437790 / 4898979485566356196394568149411] ~ [0.12082, 0.12082]
Success: LHS < CD / |V| ^ .5
Success: existence proven