show/hide visualization coordinates
a : (-0.9505949890189725, -0.19248454324621223, -0.20714421419524237)
b : (-0.34887092372368256, 0.025893717859952148, -0.9754144038555974)
c : (-0.4330262729250117, -0.9190215534698036, -0.659102837186567)
d : (-0.6333763144080783, -0.981758903308773, 0.3186107639323477)
e : (-0.703652431501301, -0.0852020992663085, 0.7559289141290455)
f : (-1.2431014465892272, 0.6204161012112264, 0.2964752001648294)
g : (-1.0427514051061606, 0.6831534510501959, -0.6812384009540853)
h : (-0.14729471588467635, 1.0052795189375294, -0.9884713974175889)
i : (0.5540766890193193, 0.3467626539016614, -1.2612967826850303)
j : (0.4687288922610812, -0.4914819704534461, -0.7227230149166037)
k : (0.2886317341212356, -1.175990845722086, -0.01631476658677783)
l : (-0.45811004055120064, -1.812230196509331, -0.21016060860792046)
m : (0.16031336492816006, -0.5880588051315219, 0.7823530691087913)
n : (0.006739898982728976, 0.17537032764069382, 1.409721501365444)
o : (-0.5479947988508095, 0.8798048192595905, 0.9669558048202405)
p : (-0.3476447573677429, 0.94254216909856, -0.010757796298674183)
q : (0.574363291161571, 0.748310226685247, -0.34568332681779973)
r : (1.2757346960655664, 0.08979336164937896, -0.6185087120852413)
s : (0.929047033988835, -0.429149626693174, 0.1628400191570069)
t : (0.9287479475120428, -0.018861614772619162, 1.0747959708463186)
u : (0.37401324967850436, 0.6855728768462774, 0.632030274301115)
v : (1.2960212982078183, 0.4913409344329645, 0.29710474378198937)
show/hide computer existence proof
(see shape-existence, preprint)
Attempting to prove existence
Starting realization:
Abstract data:
mode: maximal_simplices
data: [['q', 'i', 'h'], ['n', 't', 'm'], ['n', 'e', 'm'], ['j', 'k', 's'], ['s', 'j', 'r'], ['o', 'f', 'p'], ['j', 'r', 'i'], ['n', 'o', 'e'], ['n', 'o', 'u'], ['u', 'q', 'p'], ['v', 's', 'r'], ['t', 's', 'm'], ['n', 't', 'u'], ['v', 't', 's'], ['b', 'i', 'h'], ['f', 'a', 'g'], ['q', 'p', 'h'], ['b', 'g', 'h'], ['l', 'k', 'c'], ['q', 'r', 'i'], ['d', 'e', 'm'], ['a', 'g', 'b'], ['j', 'k', 'c'], ['l', 'd', 'c'], ['p', 'g', 'h'], ['l', 'd', 'k'], ['d', 'k', 'm'], ['k', 's', 'm'], ['u', 'q', 'v'], ['d', 'e', 'a'], ['f', 'p', 'g'], ['o', 'e', 'f'], ['j', 'b', 'c'], ['d', 'a', 'c'], ['v', 'q', 'r'], ['v', 't', 'u'], ['a', 'b', 'c'], ['u', 'o', 'p'], ['e', 'a', 'f'], ['j', 'b', 'i']]
Coordinate Data:
e : [58553313068540552967 / 50000000000000000000, 29007489798502994703 / 50000000000000000000, -20715060003772740549 / 50000000000000000000]
n : [11516848272169530997 / 25000000000000000000, 31957736906305757241 / 100000000000000000000, -834448271337385487 / 781250000000000000]
t : [-46133411764253270881 / 100000000000000000000, 12845232786909264491 / 25000000000000000000, -73316825679272785247 / 100000000000000000000]
i : [-1083285739372613171 / 12500000000000000000, 14818504280208995611 / 100000000000000000000, 80146224836931049523 / 50000000000000000000]
h : [61470854575418649161 / 100000000000000000000, -12758295555844452431 / 25000000000000000000, 16626238893389743929 / 12500000000000000000]
q : [-10694946129206082323 / 100000000000000000000, -25336252998149560527 / 100000000000000000000, 34365552043569519403 / 50000000000000000000]
u : [9340058019100581061 / 100000000000000000000, -381250360285052241 / 2000000000000000000, -29040256024752430907 / 100000000000000000000]
s : [-23081660205966240359 / 50000000000000000000, 92409732339692544923 / 100000000000000000000, 8939384744829187167 / 50000000000000000000]
d : [13759876803469856677 / 12500000000000000000, 29534132000250489163 / 20000000000000000000, 1150847506062145849 / 50000000000000000000]
v : [-82860746833830813809 / 100000000000000000000, 36067622707868867 / 10000000000000000000, 222614851358006309 / 5000000000000000000]
o : [101540862872031975931 / 100000000000000000000, -19242856127791956387 / 50000000000000000000, -62532809076664987997 / 100000000000000000000]
r : [-20208021654901409213 / 25000000000000000000, 40515433505437244809 / 100000000000000000000, 96013642613883186421 / 100000000000000000000]
p : [40752929361862656273 / 50000000000000000000, -35807557791584689 / 80000000000000000, 35238551035226481717 / 100000000000000000000]
a : [141800881888848262741 / 100000000000000000000, 34371611997498182321 / 50000000000000000000, 10975438564976661509 / 20000000000000000000]
k : [8939104787413729273 / 50000000000000000000, 167093854242583746537 / 100000000000000000000, 35794248064036848787 / 100000000000000000000]
c : [90044010279452190031 / 100000000000000000000, 7069846250867774867 / 5000000000000000000, 25018263781003940353 / 25000000000000000000]
m : [7677511623533752731 / 25000000000000000000, 54150325091763658203 / 50000000000000000000, -55090669381900081 / 125000000000000000]
b : [16325695071863855769 / 20000000000000000000, 9381079576875984401 / 20000000000000000000, 32926052947729698649 / 25000000000000000000]
j : [-131506239157101069 / 100000000000000000000, 12330370839464968749 / 12500000000000000000, 2660876822425485907 / 2500000000000000000]
l : [92552387042071079039 / 100000000000000000000, 230717789321308225809 / 100000000000000000000, 55178832266151111151 / 100000000000000000000]
f : [1368412221166989863 / 800000000000000000, -12546840450747499763 / 100000000000000000000, 4515251388876125631 / 100000000000000000000]
g : [151016523497567069491 / 100000000000000000000, -9410287717322224119 / 50000000000000000000, 20457322300153519069 / 20000000000000000000]
Desired square lengths:
default : 1
Checking inequality 1:
d = 3
|V| = 22
|E| = 60
Success: d|V| >= |E|
Checking self-intersection:
Square collision distance = 166666666666666666664943631660868742612062504841948456382244959052752074242796933914444572804979226328086084848995764147 / 333333333333333333333314123051621928941622621693615873856052497794970028898577630000000000000000000000000000000000000000
Collision distance in [28284271247461900975888385139 / 40000000000000000000000000000, 176776695296636881099302407119 / 250000000000000000000000000000] ~ [0.70711, 0.70711]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [284 / 625, 2273 / 5000] ~ [0.4544, 0.4546]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 2158136185009086917151163753294054600484977 / 50000000000000000000000000000000000000000000000000000000000000000000000000000000
rho in [2077564047151897994719017802147 / 10000000000000000000000000000000000000000000000000, 2077564047161897994719017802147 / 10000000000000000000000000000000000000000000000000] ~ [0.0, 0.0]
sigma_min ^ 2 / (16 * E ^ .5) in [2580992000000000000000000000 / 1549193338482966754071706159913, 3229080625000000000000000000 / 1936491673103708442589632699891] ~ [0.00167, 0.00167]
Success: rho < sigma_min ^ 2 / (16 * E ^ .5)
Checking inequality 4:
LHS NUM := sigma_min - [sigma_min ^ 2 - 16 * rho * |E| ^ .5 ] ^ .5 in [-39999999999994336034523327 / 200000000000000000000000000000, 200000000000028332292096259 / 1000000000000000000000000000000] ~ [-0.0002, 0.0002]
LHS DEN := 8 * |E| ^ .5 in [1936491673103708442589632699891 / 31250000000000000000000000000, 1549193338482966754071706159913 / 25000000000000000000000000000] ~ [61.96773, 61.96773]
LHS := (LHS NUM) / (LHS DEN) in [-2150537634408297636264695 / 666319715476544840460948885984, 200000000000028332292096259 / 61967733539318670162868246396512] ~ [-0.0, 0.0]
CD / |V| ^ .5 in [141421356237309504879441925695 / 938083151964685910913126022709, 176776695296636881099302407119 / 1172603939955857388641407528386] ~ [0.15076, 0.15076]
Success: LHS < CD / |V| ^ .5
Success: existence proven