show/hide visualization coordinates
a : (1.2549720603076258, 0.6088694695941571, -0.44089355187226953)
b : (0.8215977712844715, -0.0916920399786032, -1.0078153250639603)
c : (1.675328858899733, 0.33519394575034345, -1.3059957825515163)
d : (1.570205514433738, 1.304992573092889, -1.085905562748822)
e : (0.66210047577768, 1.379724789775798, -0.6738857397340325)
f : (0.44052266371697596, 0.7970017794226546, 0.10799479232144804)
g : (0.7566200991704084, -0.1441935319328036, -0.011310686103749412)
h : (-0.02629110292661585, -0.4016381886777299, -0.5776783214294976)
i : (0.0962817261987779, 0.565180247309731, -0.8018167014427321)
j : (0.8023487196780532, 0.7938182892396995, -1.4720361032072342)
k : (0.8401889115157477, 1.7883837204565842, -1.5690295200460027)
l : (-0.423181334064959, 0.3023732196794876, 0.011258076944588025)
m : (0.18810007995083783, 0.09638777478526017, 0.7753948640256546)
n : (0.08129953463210388, -0.7951922746512563, 0.33530548791393777)
o : (-0.8330270145001075, -0.6090853321373888, -0.024376548751951277)
p : (-0.7868464372460858, -0.11522744634317983, 0.8439389140398611)
q : (-0.11603581552403286, -0.691961292164315, 1.3101911857439634)
r : (-0.7151518319388311, -1.248949183785807, 0.7350177445435649)
s : (-1.5599615700242173, -0.7201612868460123, 0.6532872943668421)
t : (-1.0873986180973023, -0.7747841446579784, 1.5328898181641386)
u : (-1.5551506386610918, -1.5788159904288057, 1.165819200646407)
v : (-2.08652205258291, -0.8002250975027237, 1.4996464642413598)
show/hide computer existence proof
(see shape-existence, preprint)
Attempting to prove existence
Starting realization:
Abstract data:
mode: maximal_simplices
data: [['l', 'f', 'm'], ['n', 'g', 'h'], ['d', 'j', 'k'], ['l', 'i', 'h'], ['n', 'g', 'm'], ['e', 'j', 'i'], ['e', 'f', 'i'], ['q', 't', 'p'], ['q', 'p', 'm'], ['l', 'f', 'i'], ['n', 'o', 'r'], ['u', 's', 'v'], ['v', 't', 's'], ['b', 'i', 'h'], ['f', 'a', 'g'], ['n', 'o', 'h'], ['d', 'j', 'c'], ['b', 'g', 'h'], ['l', 'o', 'p'], ['t', 'q', 'r'], ['o', 'p', 's'], ['e', 'j', 'k'], ['a', 'g', 'b'], ['s', 'o', 'r'], ['d', 'e', 'a'], ['n', 'q', 'r'], ['u', 's', 'r'], ['j', 'b', 'c'], ['l', 'o', 'h'], ['d', 'e', 'k'], ['l', 'p', 'm'], ['u', 't', 'r'], ['d', 'a', 'c'], ['t', 'p', 's'], ['v', 't', 'u'], ['a', 'b', 'c'], ['f', 'g', 'm'], ['n', 'q', 'm'], ['e', 'a', 'f'], ['j', 'b', 'i']]
Coordinate Data:
e : [111398139553449708459 / 100000000000000000000, 196250191486647849157 / 100000000000000000000, -1011123672860200401 / 10000000000000000000]
n : [26659022719446045761 / 50000000000000000000, -21241514956057599561 / 100000000000000000000, 2270197150904875839 / 2500000000000000000]
t : [-15887942458512131361 / 25000000000000000000, -960035097836491071 / 5000000000000000000, 105283159530607560239 / 50000000000000000000]
i : [54816264595559499137 / 100000000000000000000, 28698934310010279623 / 25000000000000000000, -11452166449735980669 / 50000000000000000000]
h : [21279490841510059349 / 50000000000000000000, 141514794072617471 / 781250000000000000, -490494898148508133 / 100000000000000000000]
q : [1343380416931136837 / 4000000000000000000, -13648020884204343 / 125000000000000000, 18829645581919758149 / 10000000000000000000]
u : [-11032697189042748171 / 10000000000000000000, -99603886533812539223 / 100000000000000000000, 86929628654720969391 / 50000000000000000000]
s : [-6925504064171252637 / 6250000000000000000, -6869208087766602997 / 50000000000000000000, 61303033340742728507 / 50000000000000000000]
d : [101104321709527740249 / 50000000000000000000, 47194242454589230097 / 25000000000000000000, -51313219030080971579 / 100000000000000000000]
v : [-81732056641304645269 / 50000000000000000000, -5436199310301087239 / 25000000000000000000, 51810495917234313559 / 25000000000000000000]
o : [-4764326184291130403 / 12500000000000000000, -328852588083857087 / 12500000000000000000, 54839682369606128817 / 100000000000000000000]
r : [-6581772804550352257 / 25000000000000000000, -66617205869512695473 / 100000000000000000000, 65389555849578878307 / 50000000000000000000]
p : [-33496551748926878033 / 100000000000000000000, 46754967874750039921 / 100000000000000000000, 141671228648787371541 / 100000000000000000000]
a : [4267132450161106599 / 2500000000000000000, 119164659468483730403 / 100000000000000000000, 13187982057574297941 / 100000000000000000000]
k : [2584139662545129307 / 2000000000000000000, 23711608455472641761 / 10000000000000000000, -99625614759799035763 / 100000000000000000000]
c : [26590122233206875821 / 12500000000000000000, 22949276771025591433 / 25000000000000000000, -73322241010350374957 / 100000000000000000000]
m : [63998099970765488633 / 100000000000000000000, 67916489987594039633 / 100000000000000000000, 134816823647366703131 / 100000000000000000000]
b : [25469573820825769527 / 20000000000000000000, 24554254255603851689 / 50000000000000000000, -43504195261594786973 / 100000000000000000000]
j : [31355740985871755583 / 25000000000000000000, 5506381657321518827 / 4000000000000000000, -89926273075922170037 / 100000000000000000000]
l : [2869958569185806553 / 100000000000000000000, 88515034477016789869 / 100000000000000000000, 29201572469630026423 / 50000000000000000000]
f : [17848071669475860373 / 20000000000000000000, 137977890451333485373 / 100000000000000000000, 4254801029809128237 / 6250000000000000000]
g : [4834004075708901483 / 4000000000000000000, 21929179657893832451 / 50000000000000000000, 28073134317213153083 / 50000000000000000000]
Desired square lengths:
default : 1
Checking inequality 1:
d = 3
|V| = 22
|E| = 60
Success: d|V| >= |E|
Checking self-intersection:
Square collision distance = 1953124999999999999943173071753762322985260817460315339933923247988003983029769972700485432193215998374330656431044561 / 3906250000000000000023255590283694682398992625759190671377805394761197319570828906250000000000000000000000000000000000
Collision distance in [176776695296636881097113183383 / 250000000000000000000000000000, 707106781186547524388452733533 / 1000000000000000000000000000000] ~ [0.70711, 0.70711]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [423 / 1000, 529 / 1250] ~ [0.423, 0.4232]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 3238047237272985372261563965761686822933759 / 100000000000000000000000000000000000000000000000000000000000000000000000000000000
rho in [1799457484152650207388356912117 / 10000000000000000000000000000000000000000000000000, 1799457484162650207388356912117 / 10000000000000000000000000000000000000000000000000] ~ [0.0, 0.0]
sigma_min ^ 2 / (16 * E ^ .5) in [2236612500000000000000000000 / 1549193338482966754071706159913, 2798410000000000000000000000 / 1936491673103708442589632699891] ~ [0.00144, 0.00145]
Success: rho < sigma_min ^ 2 / (16 * E ^ .5)
Checking inequality 4:
LHS NUM := sigma_min - [sigma_min ^ 2 - 16 * rho * |E| ^ .5 ] ^ .5 in [-199999999999973651157397613 / 1000000000000000000000000000000, 200000000000026361300684143 / 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 [-199999999999973651157397613 / 61967733539318670162868246396512, 200000000000026361300684143 / 61967733539318670162868246396512] ~ [-0.0, 0.0]
CD / |V| ^ .5 in [707106781186547524388452733532 / 4690415759823429554565630113545, 707106781186547524388452733533 / 4690415759823429554565630113544] ~ [0.15076, 0.15076]
Success: LHS < CD / |V| ^ .5
Success: existence proven