show/hide visualization coordinates
a : (0.4512187811386919, -0.053676279033345375, 0.8907978706774948)
b : (0.5057063969543052, -0.8240068966564825, 0.2554854742512723)
c : (1.2641195437511177, -0.17556347381133308, 0.32129294481426157)
d : (0.9406911955619859, 0.7449273538601698, 0.5405850873533944)
e : (-0.054487567301248985, 0.7703309308397636, 0.6353116551081552)
f : (-0.4825865543939816, 0.08259314402005347, 1.2216123956161837)
g : (-0.1591588797141647, -0.837896928990458, 1.0023196072294338)
h : (-0.3882107208927244, -1.251657556791355, 0.12122046482086224)
i : (0.05448823221144511, -0.7703309676471758, -0.6353125158716402)
j : (1.035067374473446, -0.5893231244944114, -0.5598057141365098)
k : (0.7131677055518301, 0.3318786232175969, -0.3412448109741041)
l : (0.38821133054340556, 1.2516577922419545, -0.12122081265346674)
m : (-0.5057061758119723, 0.8240073614577874, -0.2554860804142638)
n : (-1.035066749829829, 0.5893245044564852, 0.5598057552296092)
o : (-0.7131724738563294, -0.3318811443489935, 0.34124806085253456)
p : (-0.9406907578795667, -0.7449267101537932, -0.5405855361309249)
q : (-0.45121814524198195, 0.05367643098305408, -0.8907980616499545)
r : (0.4825871599519098, -0.08259343549413145, -1.2216124691903851)
s : (0.15915944588685715, 0.8378971082503179, -1.002319922903923)
t : (-1.2641191411031936, 0.17556326809429557, -0.32129339202802887)
show/hide computer existence proof (failed)
(see shape-existence, preprint)
Attempting to prove existence
Starting realization:
Abstract data:
mode: maximal_simplices
data: [['c', 'k', 'd'], ['a', 'f', 'g'], ['k', 'r', 'j'], ['c', 'k', 'j'], ['p', 'q', 'i'], ['b', 'j', 'i'], ['a', 'c', 'b'], ['s', 'l', 'm'], ['k', 's', 'l'], ['k', 'l', 'd'], ['r', 'j', 'i'], ['f', 'g', 'o'], ['t', 'q', 'm'], ['t', 'n', 'm'], ['t', 'o', 'p'], ['e', 'l', 'd'], ['q', 's', 'm'], ['b', 'c', 'j'], ['p', 'h', 'o'], ['h', 'g', 'o'], ['e', 'l', 'm'], ['q', 'r', 's'], ['a', 'e', 'd'], ['q', 'r', 'i'], ['p', 't', 'q'], ['a', 'g', 'b'], ['p', 'h', 'i'], ['a', 'c', 'd'], ['b', 'h', 'g'], ['b', 'h', 'i'], ['t', 'n', 'o'], ['f', 'e', 'n'], ['f', 'n', 'o'], ['e', 'n', 'm'], ['k', 'r', 's'], ['a', 'f', 'e']]
Coordinate Data:
b : [-1093971801182274917 / 12500000000000000000, 33244522912070789431 / 25000000000000000000, 18628610547961732399 / 100000000000000000000]
k : [-7374476317302670489 / 25000000000000000000, 4347384915218803663 / 25000000000000000000, 78301639070499376843 / 100000000000000000000]
m : [1443585669799524267 / 1562500000000000000, -31823334163143835261 / 100000000000000000000, 69725766014515349923 / 100000000000000000000]
a : [-660602565579373271 / 20000000000000000000, 55945029885969442459 / 100000000000000000000, -11225657273665127707 / 25000000000000000000]
f : [90077520725370484169 / 100000000000000000000, 42318087580629561291 / 100000000000000000000, -9748010198566177011 / 12500000000000000000]
j : [-12337574432274455191 / 20000000000000000000, 109509714432076054167 / 100000000000000000000, 100157729386739936837 / 100000000000000000000]
t : [10514423712268229237 / 6250000000000000000, 16510537586602675323 / 50000000000000000000, 76306497175891848509 / 100000000000000000000]
l : [1498866115815882133 / 50000000000000000000, -745883772415605431 / 1000000000000000000, 28149619619217818151 / 50000000000000000000]
g : [28867376628694396719 / 50000000000000000000, 134367094881680695609 / 100000000000000000000, -56054802749854410431 / 100000000000000000000]
i : [36370042064827812137 / 100000000000000000000, 63805249373676245369 / 50000000000000000000, 10770840956025298647 / 10000000000000000000]
p : [27177588214785796849 / 20000000000000000000, 25014014599602843859 / 20000000000000000000, 98235711586181446913 / 100000000000000000000]
s : [1618932543580413091 / 6250000000000000000, -33212308842396888141 / 100000000000000000000, 72204575131740629119 / 50000000000000000000]
h : [10079992171905595077 / 12500000000000000000, 175743157661770429 / 100000000000000000, 16027555745501371087 / 50000000000000000000]
q : [86940679810170514261 / 100000000000000000000, 5651219860541187071 / 12500000000000000000, 66628482069042200241 / 50000000000000000000]
n : [36331385067238800813 / 25000000000000000000, -8355048463013608949 / 100000000000000000000, -5901708774935979459 / 50000000000000000000]
o : [28284028167901313369 / 25000000000000000000, 41882758208767128999 / 50000000000000000000, 10052351887835506013 / 100000000000000000000]
e : [5908452752012152591 / 12500000000000000000, -26455691101341449333 / 100000000000000000000, -19354007537726557209 / 100000000000000000000]
d : [-52250254270226271247 / 100000000000000000000, -1195766670169103867 / 5000000000000000000, -4940675381125235451 / 50000000000000000000]
r : [-804981338652332043 / 12500000000000000000, 58836745532048049627 / 100000000000000000000, 8316920244606374307 / 5000000000000000000]
c : [-10574136136142430087 / 12500000000000000000, 68133749363768209979 / 100000000000000000000, 12047863491662809961 / 100000000000000000000]
Desired square lengths:
default : 1
Checking inequality 1:
d = 3
|V| = 20
|E| = 54
Success: d|V| >= |E|
Checking self-intersection:
Square collision distance = 548669964425742052032304371281588806513365267604415532560320706483115404796521534703258416315753269331815646796409538121 / 864872250633902253168926210513884721503739975597114331829654273673846466113853580000000000000000000000000000000000000000
Collision distance in [19912217 / 25000000, 79648869 / 100000000] ~ [0.79649, 0.79649]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [31 / 5000, 4 / 625] ~ [0.0062, 0.0064]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 10880270193056601756935206931167880693206029153353786794637744634990031 / 100000000000000000000000000000000000000000000000000000000000000000000000000000000
rho in [104308533 / 10000000000000, 104408533 / 10000000000000] ~ [1e-05, 1e-05]
sigma_min ^ 2 / (16 * E ^ .5) in [961 / 2939387692, 128 / 367423461] ~ [0.0, 0.0]
Failed: unable to verify rho < sigma_min ^ 2 / (16 * E ^ .5)