show/hide visualization coordinates
a : (0.15228558048016483, -0.7113400947659881, -0.8048300884842555)
b : (-0.5871255830804682, -0.04490623169926655, -0.9004179400129769)
c : (0.2460917344687238, 0.051186642881294264, -1.4449499052739463)
d : (1.0040806868478307, -0.18853734832601265, -0.8383321045865092)
e : (0.7037625179260347, -0.6004878814763531, 0.021961889146220437)
f : (-0.011406375355085707, -1.298606103664293, -0.012161444984661374)
g : (-0.7824033437662672, -0.9619629363122896, -0.5527491368312099)
h : (-0.9867313975986838, -0.1602712834538611, 0.00898081621934449)
i : (-0.8921716611447537, 0.7547419059474699, -0.38320449643701593)
j : (-0.24938557915323167, 0.8649947138641165, -1.1412746588523976)
k : (0.7242456633556958, 0.7665844028691319, -0.9354650033442261)
l : (0.8831269523493652, 0.3821200835467069, -0.026100432242154414)
m : (0.8098501107900293, -0.0698698849087227, 0.862907763955579)
n : (-0.017407471050498335, -0.6117721285213519, 0.7146281239001708)
o : (-0.8701112116816017, -1.055530617049091, 0.43899297633495105)
p : (-0.8956117410466309, -0.2297411637992759, 1.0023946997113309)
q : (-0.5085774687117117, 0.5551264765339765, 0.5184657181490648)
r : (0.07245902123916237, 0.941941977518877, -0.1976141416035807)
s : (0.424477332646508, 0.8437311724616225, 0.7332122365163816)
t : (0.8228647923627275, 0.5896045293323029, 1.6145221032446972)
u : (-0.04231255987730809, 0.1829937690210094, 1.3210330254751943)
show/hide computer existence proof
(see shape-existence, preprint)
Attempting to prove existence
Starting realization:
Abstract data:
mode: maximal_simplices
data: [['s', 'u', 't'], ['k', 'l', 'd'], ['s', 'q', 'r'], ['f', 'e', 'n'], ['j', 'r', 'i'], ['s', 'm', 't'], ['g', 'o', 'f'], ['p', 'h', 'q'], ['c', 'b', 'a'], ['b', 'g', 'h'], ['p', 'u', 'n'], ['q', 'i', 'r'], ['s', 'm', 'l'], ['h', 'q', 'i'], ['c', 'd', 'k'], ['j', 'r', 'k'], ['p', 'o', 'n'], ['m', 't', 'u'], ['s', 'u', 'q'], ['o', 'h', 'g'], ['o', 'f', 'n'], ['b', 'j', 'i'], ['m', 'l', 'e'], ['m', 'n', 'u'], ['p', 'u', 'q'], ['c', 'a', 'd'], ['e', 'a', 'd'], ['f', 'e', 'a'], ['b', 'g', 'a'], ['s', 'l', 'r'], ['p', 'o', 'h'], ['g', 'f', 'a'], ['c', 'j', 'k'], ['i', 'b', 'h'], ['l', 'e', 'd'], ['m', 'e', 'n'], ['l', 'r', 'k'], ['c', 'b', 'j']]
Coordinate Data:
b : [109461690354886398649 / 100000000000000000000, 2174081275795083317 / 4000000000000000000, 2052398583409390383 / 1562500000000000000]
m : [-30235879032163360301 / 100000000000000000000, 888256206497229609 / 1562500000000000000, -702797829041478351 / 1562500000000000000]
g : [128989466423466290931 / 100000000000000000000, 14605770235617939283 / 10000000000000000000, 96586629020024269673 / 100000000000000000000]
a : [17760286999411545319 / 50000000000000000000, 120995418201549240957 / 100000000000000000000, 30448681046332208647 / 25000000000000000000]
c : [26139958599967195483 / 100000000000000000000, 2796421527301312633 / 6250000000000000000, 18580670586429791657 / 10000000000000000000]
k : [-10837717144365007353 / 50000000000000000000, -1674814472622672523 / 6250000000000000000, 2697164313426517759 / 2000000000000000000]
t : [-15768673594716585879 / 50000000000000000000, -1819808841655973087 / 20000000000000000000, -15017561873445802207 / 12500000000000000000]
s : [8301398782188776357 / 100000000000000000000, -34511708521211818351 / 100000000000000000000, -8002377078683719077 / 25000000000000000000]
u : [27490194017285189639 / 50000000000000000000, 31562031822849488231 / 100000000000000000000, -45395793605308064087 / 50000000000000000000]
i : [69983149080657474783 / 50000000000000000000, -3201597733724570607 / 12500000000000000000, 39816082490302440833 / 50000000000000000000]
l : [-7512712637619390109 / 20000000000000000000, 11649400370279736449 / 100000000000000000000, 343138738758740091 / 781250000000000000]
q : [50803439459005369229 / 50000000000000000000, -1130247785689444781 / 20000000000000000000, -5267428239001596159 / 50000000000000000000]
o : [137760253214999735419 / 100000000000000000000, 155414470429859529689 / 100000000000000000000, -2587582296591818491 / 100000000000000000000]
p : [140310306151502652851 / 100000000000000000000, 72835525104878017691 / 100000000000000000000, -14731938658557447589 / 25000000000000000000]
n : [26244939575944703273 / 50000000000000000000, 11103862157708560829 / 10000000000000000000, -15075548526556897441 / 50000000000000000000]
d : [-49658936637943485203 / 100000000000000000000, 34357571778775845679 / 50000000000000000000, 6257246289777710171 / 5000000000000000000]
r : [10875807480730834251 / 25000000000000000000, -22166394513468633323 / 50000000000000000000, 61073129497261352667 / 100000000000000000000]
h : [2988445436134158973 / 2000000000000000000, 65888537070336538591 / 100000000000000000000, 404136337149688363 / 1000000000000000000]
f : [1297244239558703677 / 2500000000000000000, 2808156548302808111 / 1562500000000000000, 42527859835369425591 / 100000000000000000000]
e : [-98135598728819481 / 500000000000000000, 27477549218146436823 / 25000000000000000000, 39115526422281241281 / 100000000000000000000]
j : [37843844981081370639 / 50000000000000000000, -9159515665365303921 / 25000000000000000000, 77719590611071529457 / 50000000000000000000]
Desired square lengths:
default : 1
Checking inequality 1:
d = 3
|V| = 21
|E| = 57
Success: d|V| >= |E|
Checking self-intersection:
Square collision distance = 1666666666666666666528534653538839890560663896318725807552461401945265240427863036385586972976901315723425416774471867 / 3333333333333333333244803932392271692518102843192943425969138545897532093367599500000000000000000000000000000000000000
Collision distance in [707106781186547524380932098111 / 1000000000000000000000000000000, 11048543456039805068452064033 / 15625000000000000000000000000] ~ [0.70711, 0.70711]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [4479 / 10000, 4481 / 10000] ~ [0.4479, 0.4481]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 655297505468698897731981807661356111869733 / 20000000000000000000000000000000000000000000000000000000000000000000000000000000
rho in [452526762146691613257257352543 / 2500000000000000000000000000000000000000000000000, 452526762149191613257257352543 / 2500000000000000000000000000000000000000000000000] ~ [0.0, 0.0]
sigma_min ^ 2 / (16 * E ^ .5) in [12538400625000000000000000000 / 7549834435270749697236684806947, 6274800312500000000000000000 / 3774917217635374848618342403473] ~ [0.00166, 0.00166]
Success: rho < sigma_min ^ 2 / (16 * E ^ .5)
Checking inequality 4:
LHS NUM := sigma_min - [sigma_min ^ 2 - 16 * rho * |E| ^ .5 ] ^ .5 in [-7999999999999024074374331 / 40000000000000000000000000000, 50000000000006102258775183 / 250000000000000000000000000000] ~ [-0.0002, 0.0002]
LHS DEN := 8 * |E| ^ .5 in [3774917217635374848618342403473 / 62500000000000000000000000000, 7549834435270749697236684806947 / 125000000000000000000000000000] ~ [60.39868, 60.39868]
LHS := (LHS NUM) / (LHS DEN) in [-66666666666658533953119425 / 20132891827388665859297826151856, 16666666666668700752925061 / 5033222956847166464824456537964] ~ [-0.0, 0.0]
CD / |V| ^ .5 in [707106781186547524380932098111 / 4582575694955840006588047193729, 11048543456039805068452064033 / 71602745233685000102938237402] ~ [0.1543, 0.1543]
Success: LHS < CD / |V| ^ .5
Success: existence proven