show/hide visualization coordinates
a : (0.7260197216287211, 0.5665995155644464, -0.6442377369130737)
b : (1.0282977948965777, -0.016213352721990704, 0.11005473088785067)
c : (0.6953844716970693, -0.4285252760436719, -0.737982766586781)
d : (-0.14682439050225643, 0.08412371494332553, -0.5710239558790783)
e : (-0.10898725981115287, 1.0734004956898944, -0.4299572956904668)
f : (0.7780195940344267, 1.5339082695499169, -0.396024546826675)
g : (1.440601467276394, 0.8852859855518663, -0.021492313297546972)
h : (0.6493870729065061, 0.7804333880817645, 0.5809906449225707)
i : (0.14984978872453358, -0.0858571308749038, 0.5827902220633582)
j : (0.5423178539853455, -0.8897989431911909, 0.13597216047672206)
k : (0.6713366584189893, -1.4274076784249645, -0.6972931009513873)
l : (-0.18227209827451785, -0.9065220967375189, -0.7027977613674729)
m : (-0.98178475086325, -0.42005775681308855, -0.350474097199967)
n : (-0.9298856290690511, 0.5628838008715843, -0.17403040835443173)
o : (-0.8199594819399175, 1.5125618139005317, 0.11927474629978524)
p : (0.14216121728338152, 1.616363191532922, 0.3713640838920127)
q : (1.128254551701841, 1.65698127429011, 0.5325165184644218)
r : (-0.3501502112754664, 0.7796956017684439, 0.6113990845649252)
s : (-0.8501502112754664, -0.0858571308749038, 0.5827902220633582)
t : (-0.3501502112754664, -0.9518825346593424, 0.5827902220633582)
u : (-0.061893894799597615, -1.6623527259201671, -0.05919140021376823)
v : (-0.9774917870354445, -1.4196197521875396, -0.37975528338869824)
w : (-1.3373083266803405, -0.9444682691314443, 0.4232161519360998)
x : (-0.8547719397518576, -1.8136744041640798, 0.5311018790348845)
show/hide computer existence proof
(see shape-existence, preprint)
Attempting to prove existence
Starting realization:
Abstract data:
mode: maximal_simplices
data: [['i', 'j', 't'], ['n', 'o', 'r'], ['d', 'a', 'c'], ['m', 'l', 'd'], ['s', 'm', 'w'], ['k', 'l', 'u'], ['s', 'm', 'n'], ['m', 'l', 'v'], ['e', 'n', 'o'], ['i', 's', 'r'], ['b', 'a', 'c'], ['x', 'w', 't'], ['i', 's', 't'], ['w', 'v', 'x'], ['j', 'u', 't'], ['k', 'j', 'u'], ['s', 'n', 'r'], ['m', 'v', 'w'], ['i', 'b', 'j'], ['s', 'w', 't'], ['o', 'p', 'r'], ['b', 'a', 'g'], ['h', 'q', 'p'], ['q', 'f', 'p'], ['l', 'd', 'c'], ['e', 'f', 'a'], ['e', 'f', 'p'], ['h', 'i', 'b'], ['v', 'x', 'u'], ['n', 'm', 'd'], ['k', 'l', 'c'], ['u', 'x', 't'], ['e', 'd', 'a'], ['k', 'j', 'c'], ['e', 'o', 'p'], ['h', 'p', 'r'], ['h', 'b', 'g'], ['h', 'i', 'r'], ['b', 'j', 'c'], ['n', 'e', 'd'], ['l', 'v', 'u'], ['q', 'f', 'g'], ['h', 'q', 'g'], ['f', 'a', 'g']]
Coordinate Data:
i : [94465098193750130670311708771 / 2500000000000000000000000000000000000000000000000000000000000000000, 373359895886205715894617188543 / 50000000000000000000000000000000000000000000000000000000000000000000, 600182238254972342768221868017 / 100000000000000000000000000000000000000000000000000000000000000000000000000000000000]
x : [10046217284763911470627110001 / 10000000000000000000000000000, 86390863664458798340533837439 / 50000000000000000000000000000, 25844171514236870842791752767 / 500000000000000000000000000000]
o : [484904635332225558617669134709 / 500000000000000000000000000000, -159841894477543561813282875251 / 100000000000000000000000000000, 463515475763572949712570620929 / 1000000000000000000000000000000]
g : [-129075167855186051432609865819 / 100000000000000000000000000000, -194228623285354014044731373829 / 200000000000000000000000000000, 604282535360905136903539093549 / 1000000000000000000000000000000]
w : [148715811540487405453195610397 / 100000000000000000000000000000, 858611138256540573874779678511 / 1000000000000000000000000000000, 159574070127258395308473521 / 1000000000000000000000000000]
h : [-49953728418197245332364789457 / 100000000000000000000000000000, -866290518956668282532923875537 / 1000000000000000000000000000000, 224947142598433562202232163 / 125000000000000000000000000000]
p : [1922142860288018008128981421 / 250000000000000000000000000000, -85111016120391294271139372961 / 50000000000000000000000000000, 10571306908567272828977436923 / 50000000000000000000000000000]
s : [1, -47108520207866534990406565663 / 2000000000000000000000000000000000000000000000000000000000000000000, -241882201960889558727559475607 / 100000000000000000000000000000000000000000000000000000000000000000000000000000000000]
u : [21174368352413119242172850013 / 100000000000000000000000000000, 157649559504526331366563761749 / 100000000000000000000000000000, 16049540556928159737539192681 / 25000000000000000000000000000]
j : [-39246806526081185821475734491 / 100000000000000000000000000000, 803941812316287102928336738043 / 1000000000000000000000000000000, 1117045153966590239180490257 / 2500000000000000000000000000]
t : [1 / 2, 866025403784438646763723170753 / 1000000000000000000000000000000, -186831464279062664846142010691 / 100000000000000000000000000000000000000000000000000000000000000000000000000000000000]
k : [-130371717423613921232013868637 / 250000000000000000000000000000, 134155054755006068040256107223 / 100000000000000000000000000000, 128008332301474549892756285623 / 100000000000000000000000000000]
c : [-68191835371566969325638130019 / 125000000000000000000000000000, 342668145168768117749636253453 / 1000000000000000000000000000000, 66038649432506954451814630713 / 50000000000000000000000000000]
v : [901873260607982396053245939 / 800000000000000000000000000, 66688131065631785411049194919 / 50000000000000000000000000000, 481272752726028204931795279877 / 500000000000000000000000000000]
l : [332121886999051447582750954939 / 1000000000000000000000000000000, 820664965862615118254447659121 / 1000000000000000000000000000000, 12855879834308310031369706383 / 10000000000000000000000000000]
m : [28290863489694591300176939381 / 25000000000000000000000000000, 334200625938184705350493711051 / 1000000000000000000000000000000, 23331607981583129663591743883 / 25000000000000000000000000000]
d : [148337089613395016734297459437 / 500000000000000000000000000000, -42495211454557331955005741477 / 250000000000000000000000000000, 14422677224280455770948993179 / 12500000000000000000000000000]
a : [-115233986580837510277248990327 / 200000000000000000000000000000, -326228323219675115787444205207 / 500000000000000000000000000000, 61351397948821590930487253837 / 50000000000000000000000000000]
r : [1 / 2, -865552732643347635393694472169 / 1000000000000000000000000000000, -28608862501567039839439133619 / 1000000000000000000000000000000]
q : [-978404762977307344484244083407 / 1000000000000000000000000000000, -43570960129125348324055559329 / 25000000000000000000000000000, 50273703598936391502258562417 / 1000000000000000000000000000000]
e : [51767409707137287982991997051 / 200000000000000000000000000000, -57962881328239915970317414727 / 50000000000000000000000000000, 10127475177538248867822127573 / 10000000000000000000000000000]
b : [-7027584049376352260585264659 / 8000000000000000000000000000, -34821889076456551671894057919 / 500000000000000000000000000000, 472735491175507482423087575721 / 1000000000000000000000000000000]
n : [21594708355871694718141846659 / 20000000000000000000000000000, -648740931746488048980668771813 / 1000000000000000000000000000000, 189205157604447490616348441443 / 250000000000000000000000000000]
f : [-628169805309893044302185532867 / 1000000000000000000000000000000, -161976540042482083912801681663 / 100000000000000000000000000000, 61175923055627075508640379881 / 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 = 34007490277251040000321532068145980852543761355801497164005163660277776282019137121904793816947571855888360237819997049 / 61681565479609633611395204258836611280080623477140138812722240374129999158868002500000000000000000000000000000000000000
Collision distance in [742522464541719569047420073443 / 1000000000000000000000000000000, 185630616135429892261855018361 / 250000000000000000000000000000] ~ [0.74252, 0.74252]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [21644748681412833999 / 100000000000000000000, 21644748681412834001 / 100000000000000000000] ~ [0.21645, 0.21645]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 617838452041804485321890527107505690768707739744039297543432180045407184595882546636782527391613487559075616527912666027586669326489060487423442153771566417953271707330974666469615217259877839427108602848744770085752755955638849807086209089030548950311573278031334284751000407 / 5000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000
rho in [3515219629103719275377750920903 / 10000000000000000000000000000000000000000000000000000000000, 3525219629103719275377750920903 / 10000000000000000000000000000000000000000000000000000000000] ~ [0.0, 0.0]
sigma_min ^ 2 / (16 * E ^ .5) in [468495145481522616071824842548730332001 / 1299846144741753657673581370922720000000000, 468495145481522616158403837274381668001 / 1299846144741753657673581370922560000000000] ~ [0.00036, 0.00036]
Success: rho < sigma_min ^ 2 / (16 * E ^ .5)
Checking inequality 4:
LHS NUM := sigma_min - [sigma_min ^ 2 - 16 * rho * |E| ^ .5 ] ^ .5 in [-8587166001 / 100000000000000000000, 1412834001 / 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 [-5366978750625000000 / 4062019202317980180229941784133, 883021250625000000 / 4062019202317980180229941784133] ~ [-0.0, 0.0]
CD / |V| ^ .5 in [742522464541719569047420073443 / 4898979485566356196394568149412, 742522464541719569047420073444 / 4898979485566356196394568149411] ~ [0.15157, 0.15157]
Success: LHS < CD / |V| ^ .5
Success: existence proven