show/hide visualization coordinates
a : (-0.06916886624649676, -0.8892412329859114, -0.5114575403538498)
b : (0.25122509212602767, -0.45135059483104073, -1.3514572430054077)
c : (0.9091957897298506, -0.7419514497511273, -0.6567445655520207)
d : (0.5415604986885517, -0.7779859285672845, 0.27252708962606953)
e : (-0.37839841542813946, -1.147356787601723, 0.40383118260644646)
f : (-1.0467670215596399, -0.9139640032906347, -0.3024345001003895)
g : (-0.7281222946405546, -0.5003255130584485, -1.1552936545949049)
h : (-0.2071048565166057, 0.31404871993920236, -0.8996856778018377)
i : (0.7884218488783656, 0.2306841047750376, -0.8552231117044501)
j : (1.184745933363155, -0.05620001251738577, 0.01691490678954999)
k : (0.9162109061976553, -0.17093124295736922, 0.9733278322286366)
l : (-0.06062842952954528, -0.38482205393757646, 0.9673584809849336)
m : (-0.9436858966270638, -0.3282669751843413, 0.5015140510831365)
n : (-1.0445271504939533, 0.08071427689098598, -0.40543984905151265)
o : (-0.6751524298240603, 1.0085260239430205, -0.3532126744937226)
p : (0.32254369273386335, 0.944141310827129, -0.33183381227261943)
q : (1.3201869016849832, 0.8789886031624317, -0.31031283837108314)
r : (0.7901660946227937, 0.7120034317815038, 0.5210678786413019)
s : (0.25787664061603166, 0.4878787020706702, 1.3374232195837306)
t : (-0.7218138114892396, 0.3169538954946761, 1.2325836824294294)
u : (-1.1981738764680832, 0.6347281962876106, 0.4127662745580708)
v : (-0.2085903498178966, 0.7537285295105732, 0.49378086877049204)
show/hide computer existence proof
(see shape-existence, preprint)
Attempting to prove existence
Starting realization:
Abstract data:
mode: maximal_simplices
data: [['n', 'g', 'h'], ['j', 'i', 'c'], ['d', 'j', 'k'], ['n', 'f', 'm'], ['n', 'o', 'u'], ['v', 's', 'r'], ['q', 'j', 'r'], ['v', 'p', 'r'], ['p', 'i', 'h'], ['n', 'f', 'g'], ['v', 'o', 'p'], ['q', 'p', 'r'], ['v', 't', 's'], ['u', 'n', 'm'], ['b', 'i', 'h'], ['f', 'a', 'g'], ['n', 'o', 'h'], ['d', 'j', 'c'], ['b', 'g', 'h'], ['l', 't', 's'], ['u', 'o', 'v'], ['s', 'k', 'r'], ['b', 'i', 'c'], ['q', 'j', 'i'], ['a', 'g', 'b'], ['q', 'p', 'i'], ['l', 'd', 'k'], ['l', 'k', 's'], ['d', 'e', 'a'], ['l', 't', 'm'], ['j', 'k', 'r'], ['d', 'a', 'c'], ['v', 't', 'u'], ['u', 't', 'm'], ['a', 'b', 'c'], ['o', 'p', 'h'], ['e', 'a', 'f'], ['e', 'f', 'm'], ['l', 'e', 'm'], ['l', 'd', 'e']]
Coordinate Data:
e : [45561965538404924019 / 50000000000000000000, 163722760207593264569 / 100000000000000000000, 15898530529436184871 / 100000000000000000000]
n : [31547360916678245613 / 20000000000000000000, 40915653758322375609 / 100000000000000000000, 96825633695232097971 / 100000000000000000000]
t : [7841591917682492021 / 6250000000000000000, 17291691897953356363 / 100000000000000000000, -6697671945286211771 / 10000000000000000000]
i : [-6389523838460164499 / 25000000000000000000, 12959335484958606699 / 50000000000000000000, 35450989990131457721 / 25000000000000000000]
h : [14798915037131295907 / 20000000000000000000, 17582209453500731813 / 100000000000000000000, 14625021657026460393 / 10000000000000000000]
q : [-15746920126900484183 / 20000000000000000000, -4863972358602773761 / 12500000000000000000, 43656466313594573037 / 50000000000000000000]
u : [173101477180804222601 / 100000000000000000000, -14485738181340080553 / 100000000000000000000, 7502510667136874841 / 50000000000000000000]
s : [13748212736196369127 / 50000000000000000000, 199211240353952163 / 100000000000000000000, -38730336584146110059 / 50000000000000000000]
d : [-435980167429635003 / 50000000000000000000, 126785674304149425077 / 100000000000000000000, 29028939827473874247 / 100000000000000000000]
v : [37071562257892781733 / 50000000000000000000, -26385771503636351843 / 100000000000000000000, 6903561913031623127 / 100000000000000000000]
o : [6039966625820096739 / 5000000000000000000, -25932760473440543747 / 50000000000000000000, 45801458119726543907 / 50000000000000000000]
r : [-25732519928283478769 / 100000000000000000000, -888530469229176587 / 4000000000000000000, 2087430462975317821 / 50000000000000000000]
p : [657178758144049033 / 3125000000000000000, -2839190602205745313 / 6250000000000000000, 89465030017342775909 / 100000000000000000000]
a : [60200976158645578019 / 100000000000000000000, 137911204746012095487 / 100000000000000000000, 21485480565093162093 / 20000000000000000000]
k : [-3833700108576963239 / 10000000000000000000, 33040102871578945257 / 50000000000000000000, -8210226886556566061 / 20000000000000000000]
c : [-37635489438989150951 / 100000000000000000000, 30795556605633422021 / 25000000000000000000, 15244513168160362119 / 12500000000000000000]
m : [147652679196702285001 / 100000000000000000000, 40906889482927551453 / 50000000000000000000, 383140230110448849 / 6250000000000000000]
b : [28161580321393139421 / 100000000000000000000, 11765267616315630629 / 12500000000000000000, 95713686545310791027 / 50000000000000000000]
j : [-16297625950579896477 / 25000000000000000000, 54607082699159550297 / 100000000000000000000, 54590158111125831189 / 100000000000000000000]
l : [5934693248695042929 / 10000000000000000000, 3498771473647144573 / 4000000000000000000, -20227099654206261687 / 50000000000000000000]
f : [157960791689959885761 / 100000000000000000000, 35095870444121107911 / 25000000000000000000, 21631274700029945759 / 25000000000000000000]
g : [63048159499025680033 / 50000000000000000000, 1547181761769778409 / 1562500000000000000, 171811014249571296739 / 100000000000000000000]
Desired square lengths:
default : 1
Checking inequality 1:
d = 3
|V| = 22
|E| = 60
Success: d|V| >= |E|
Checking self-intersection:
Square collision distance = 35128072593787165997080139664705268609053788565690485501697100121805988518872962850501507554576190226157620726704182969 / 57902042660720441929941689627120626136433084127354707869491629915092118468902802500000000000000000000000000000000000000
Collision distance in [389448667859205310681136061703 / 500000000000000000000000000000, 778897335718410621362272123407 / 1000000000000000000000000000000] ~ [0.7789, 0.7789]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [517 / 2000, 2587 / 10000] ~ [0.2585, 0.2587]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 7845169943548830608509247004009271829851271 / 100000000000000000000000000000000000000000000000000000000000000000000000000000000
rho in [700230763014452195691107526927 / 2500000000000000000000000000000000000000000000000, 700230763016952195691107526927 / 2500000000000000000000000000000000000000000000000] ~ [0.0, 0.0]
sigma_min ^ 2 / (16 * E ^ .5) in [835278125000000000000000000 / 1549193338482966754071706159913, 1045713906250000000000000000 / 1936491673103708442589632699891] ~ [0.00054, 0.00054]
Success: rho < sigma_min ^ 2 / (16 * E ^ .5)
Checking inequality 4:
LHS NUM := sigma_min - [sigma_min ^ 2 - 16 * rho * |E| ^ .5 ] ^ .5 in [-199999999999932908058231909 / 1000000000000000000000000000000, 10000000000003357192521367 / 50000000000000000000000000000] ~ [-0.0002, 0.0002]
LHS DEN := 8 * |E| ^ .5 in [1936491673103708442589632699891 / 31250000000000000000000000000, 1549193338482966754071706159913 / 25000000000000000000000000000] ~ [61.96773, 61.96773]
LHS := (LHS NUM) / (LHS DEN) in [-66666666666644302686077303 / 20655911179772890054289415465504, 50000000000016785962606835 / 15491933384829667540717061599128] ~ [-0.0, 0.0]
CD / |V| ^ .5 in [778897335718410621362272123406 / 4690415759823429554565630113545, 86544148413156735706919124823 / 521157306647047728285070012616] ~ [0.16606, 0.16606]
Success: LHS < CD / |V| ^ .5
Success: existence proven