show/hide visualization coordinates
a : (-0.3940242440044191, 0.44447636431514365, 0.665067751513817)
b : (-0.6785448537032686, -0.2947503680377299, 0.054664720040767834)
c : (0.04091388398973117, -0.45358198768734925, 0.7307946198060971)
d : (0.4323443711314968, 0.32826481445225125, 1.2160757256818981)
e : (0.43981392676559683, 0.9425070741518018, 0.4269935676414194)
f : (-0.44746285151578336, 1.2677647197433388, 0.09996546073489598)
g : (-1.168516064161619, 0.5769501085613568, 0.04651045619269922)
h : (-1.354249116698814, -0.10763318850802928, -0.6583646693216179)
i : (-0.8447199502867486, -0.9680545810103249, -0.6657846356177859)
j : (-0.1407953844619121, -1.1372983689951925, 0.024031822475849673)
k : (0.5653808486701327, -1.30480462466502, 0.7119684344328747)
l : (1.0123336931176472, -0.44769605477439955, 0.968089605483476)
m : (1.280546797404813, 0.4800636384067677, 0.7086215296108784)
n : (1.101190421596022, 0.6445078195211809, -0.26132145930875167)
o : (0.13122979993209316, 0.7104738486507038, -0.49546858276365857)
p : (-0.8542491166988139, 0.7583922152764093, -0.6583646693216179)
q : (-1.354249116698814, 1.5167836692833525, -0.24022306353568967)
r : (-1.854249116698814, 0.7583922152764093, -0.6583646693216179)
s : (-0.3647852879439109, -0.10155012720344458, -0.8030171077761863)
t : (0.12083013263782971, -0.9670285473452351, -0.9259999015405561)
u : (0.825393075882961, -1.0630592145656002, -0.2228859918794191)
v : (1.5272924590714676, -1.1547695039382146, 0.4834612872282342)
w : (1.3666197197626069, -0.2678349144310792, 0.05041243919975125)
x : (0.611955972910515, -0.1605150064770975, -0.5968626696557573)
show/hide computer existence proof
(see shape-existence, preprint)
Attempting to prove existence
Starting realization:
Abstract data:
mode: maximal_simplices
data: [['b', 'i', 'h'], ['a', 'b', 'c'], ['x', 's', 'o'], ['s', 'i', 't'], ['p', 'o', 'f'], ['j', 'b', 'i'], ['a', 'g', 'f'], ['g', 'q', 'r'], ['m', 'l', 'd'], ['x', 'n', 'w'], ['x', 's', 't'], ['v', 'w', 'u'], ['a', 'e', 'f'], ['i', 's', 'h'], ['p', 'q', 'f'], ['e', 'o', 'f'], ['v', 'l', 'w'], ['l', 'k', 'c'], ['x', 'u', 't'], ['a', 'e', 'd'], ['j', 'u', 't'], ['a', 'd', 'c'], ['m', 'e', 'n'], ['p', 'q', 'r'], ['x', 'n', 'o'], ['m', 'e', 'd'], ['p', 'h', 'r'], ['s', 'p', 'h'], ['m', 'n', 'w'], ['b', 'g', 'h'], ['m', 'l', 'w'], ['j', 'i', 't'], ['g', 'h', 'r'], ['j', 'k', 'u'], ['v', 'k', 'u'], ['j', 'b', 'c'], ['a', 'b', 'g'], ['j', 'k', 'c'], ['g', 'q', 'f'], ['s', 'p', 'o'], ['v', 'l', 'k'], ['e', 'n', 'o'], ['d', 'l', 'c'], ['x', 'w', 'u']]
Coordinate Data:
p : [279180651970909395993016098489 / 100000000000000000000000000000000000000000000000000000000000000000000000, -437003909808378329917676827547 / 1000000000000000000000000000000000000000000000000000000000000000000000, 207923275836560160553542203877 / 100000000000000000000000000000000000000000000000000000000000000000000000000000000000000]
g : [125706778985122077664746493 / 400000000000000000000000000, 36288421343010511303308325691 / 200000000000000000000000000000, -704875125514317116080417109027 / 1000000000000000000000000000000]
v : [-238154157577028158783648012721 / 100000000000000000000000000000, 191316171921462398723830206437 / 100000000000000000000000000000, -57091297827492601203800536051 / 50000000000000000000000000000]
j : [-713453732236901820292757021211 / 1000000000000000000000000000000, 9478452921358009847101495281 / 5000000000000000000000000000, -682396491797467581319211172017 / 1000000000000000000000000000000]
s : [-244731914377451482553791576977 / 500000000000000000000000000000, 3359149775311929215664582357 / 3906250000000000000000000000, 144652438454568485881721492553 / 1000000000000000000000000000000]
r : [1, 11213692593565336528015488877 / 2500000000000000000000000000000000000000000000000000000000000000000, 165776496433996119133373476367 / 1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000]
e : [-64703152173220535356139273163 / 50000000000000000000000000000, -46028714718848109078192452047 / 250000000000000000000000000000, -54267911848151864230711664053 / 50000000000000000000000000000]
c : [-895163000688544990425018634697 / 1000000000000000000000000000000, 121197420296375858545632381419 / 100000000000000000000000000000, -347289822281928749726447861 / 250000000000000000000000000]
a : [-14382027271699835793066604873 / 31250000000000000000000000000, 62783170192253138727114557867 / 200000000000000000000000000000, -132343242083543478397795476581 / 100000000000000000000000000000]
i : [-9529166412065299102216163801 / 1000000000000000000000000000000, 172644679628673434821366278981 / 100000000000000000000000000000, 741996629616805775479746541 / 100000000000000000000000000000]
w : [-27760860455767762014406980677 / 12500000000000000000000000000, 102622712970748856964223495493 / 100000000000000000000000000000, -44298569282585568268956907507 / 62500000000000000000000000000]
h : [1 / 2, 866025403784438646763723170753 / 1000000000000000000000000000000, -170211365780005550749370402101 / 100000000000000000000000000000000000000000000000000000000000000000000000000000000000000]
t : [-975079249336643626608191476649 / 1000000000000000000000000000000, 172542076262164436803074687307 / 100000000000000000000000000000, 267635232218938271559119617551 / 1000000000000000000000000000000]
f : [-406786265183030496275466102529 / 1000000000000000000000000000000, -509372504466929458213001018253 / 1000000000000000000000000000000, -75833013005651379049165367329 / 100000000000000000000000000000]
m : [-106739795705181359125637373747 / 50000000000000000000000000000, 139164288434820806333998154913 / 500000000000000000000000000000, -17087327486656203908168150823 / 12500000000000000000000000000]
q : [1 / 2, -758391454006943177828569072111 / 1000000000000000000000000000000, -418141605785928208369375873151 / 1000000000000000000000000000000]
d : [-128659348783031072897609996499 / 100000000000000000000000000000, 3441019206593264755941931713 / 8000000000000000000000000000, -93722019750175799333079171561 / 50000000000000000000000000000]
l : [-93329140490823050359291432323 / 50000000000000000000000000000, 120608827005080889338440972877 / 100000000000000000000000000000, -32529085496101878488371828273 / 20000000000000000000000000000]
n : [-195543953829483603636335672061 / 100000000000000000000000000000, 56942197877614205557368635853 / 500000000000000000000000000000, -397043210012866177739728751689 / 1000000000000000000000000000000]
u : [-41991054814544369326880663477 / 25000000000000000000000000000, 36429028596840190162186711629 / 20000000000000000000000000000, -17419147097687951209078650803 / 40000000000000000000000000000]
o : [-985478916630907081994185643877 / 1000000000000000000000000000000, 47918366625705529771739940863 / 1000000000000000000000000000000, -81448043278979636150944196423 / 500000000000000000000000000000]
b : [-10981516437221585702142591159 / 62500000000000000000000000000, 13164282291426740128634752221 / 12500000000000000000000000000, -178257347340596430794250991901 / 250000000000000000000000000000]
k : [-8872687283555916211865561651 / 6250000000000000000000000000, 103159841997071466772834660427 / 50000000000000000000000000000, -137033310375449257008739071549 / 100000000000000000000000000000]
x : [-146620508960932889200709587733 / 100000000000000000000000000000, 459453610876753407316240456749 / 500000000000000000000000000000, -3843874979116286872379533963 / 62500000000000000000000000000]
Desired square lengths:
default : 1
Checking inequality 1:
d = 3
|V| = 24
|E| = 66
Success: d|V| >= |E|
Checking self-intersection:
Square collision distance = 93169426032897887378674912538468563873726429134052043740426639458685560618433386207534502776296385193660773110780301409 / 241379793197737065180568096022547904086205231186588158320274338828537563726763487500000000000000000000000000000000000000
Collision distance in [310639199881395810956792723841 / 500000000000000000000000000000, 621278399762791621913585447683 / 1000000000000000000000000000000] ~ [0.62128, 0.62128]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [16517647731446569999 / 100000000000000000000, 16517647731446570001 / 100000000000000000000] ~ [0.16518, 0.16518]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 377916263225258793218770554069384311032707509420345499330738462792729636224610731209490012296041773037884742378149771123682328336555812230220935925019657171519221156529414072504775848888207830584432987353957853167894425793246394300323296213040365442889862161907150624923719684030596728408341 / 250000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000
rho in [3888013699694273418925626910779 / 100000000000000000000000000000000000000000000000000000000000, 3988013699694273418925626910779 / 100000000000000000000000000000000000000000000000000000000000] ~ [0.0, 0.0]
sigma_min ^ 2 / (16 * E ^ .5) in [272832686580162020222629469302006860001 / 1299846144741753657673581370922720000000000, 272832686580162020288700060227793140001 / 1299846144741753657673581370922560000000000] ~ [0.00021, 0.00021]
Success: rho < sigma_min ^ 2 / (16 * E ^ .5)
Checking inequality 4:
LHS NUM := sigma_min - [sigma_min ^ 2 - 16 * rho * |E| ^ .5 ] ^ .5 in [-8553430001 / 100000000000000000000, 1446570001 / 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 [-5345893750625000000 / 4062019202317980180229941784133, 904106250625000000 / 4062019202317980180229941784133] ~ [-0.0, 0.0]
CD / |V| ^ .5 in [103546399960465270318930907947 / 816496580927726032732428024902, 621278399762791621913585447683 / 4898979485566356196394568149411] ~ [0.12682, 0.12682]
Success: LHS < CD / |V| ^ .5
Success: existence proven