show/hide visualization coordinates
a : (0.7003975271647371, 0.18149817851141659, -1.4632993397686076)
b : (0.13340863233990213, -0.4639333841137075, -0.9514969451741676)
c : (0.20018151148297797, 0.4883204611636849, -0.6535808550323889)
d : (1.2000403340548735, 0.5040917833940328, -0.6593774333549408)
e : (1.5639400023271315, 0.6731698293204783, -1.5753412131066489)
f : (1.4042364433907444, -0.17743499951619374, -2.0763064797896673)
g : (0.9582710684090103, -0.7836071645334945, -1.4177700793715586)
h : (1.0115068652206805, -0.46013348806093723, -0.47303163378613966)
i : (0.16271996874776967, -0.585272954711954, 0.040681241526698164)
j : (-0.5837319658051359, -0.06801314810713016, -0.3779496243603805)
k : (-0.21404697941595585, 0.6194874717352282, 0.24709110115660915)
l : (0.7089181972762, 0.24212250576934458, 0.1713879633406299)
m : (1.722832594049974, -0.2074178595953144, -1.1288902455575336)
n : (0.0977268076905406, -0.07338060294640908, 0.8972687205501362)
o : (-0.716390071232548, -0.5067998369004411, 0.5107955971751346)
p : (-1.1771237660533391, 0.3567336624619294, 0.3057727742120284)
q : (-0.6562737571486594, 0.5369260281608387, 1.140186328493013)
r : (-0.6315701788633015, -0.3954057333395366, 1.5009455552877085)
s : (-1.507814666670176, -0.22167092300657373, 1.051488312308315)
t : (-1.6277590980430154, 0.7700646484441508, 1.0970282914689502)
u : (-1.2673871986950542, 0.2732300404352679, 1.8865138622332311)
v : (-1.482082270227356, -0.7025745145646807, 1.927884101549582)
show/hide computer existence proof
(see shape-existence, preprint)
Attempting to prove existence
Starting realization:
Abstract data:
mode: maximal_simplices
data: [['q', 'p', 'k'], ['u', 't', 's'], ['l', 'i', 'h'], ['h', 'g', 'm'], ['o', 'j', 'i'], ['q', 't', 'p'], ['o', 'j', 'p'], ['v', 's', 'r'], ['u', 'r', 'v'], ['n', 'o', 'r'], ['v', 'u', 's'], ['t', 'q', 'u'], ['b', 'i', 'h'], ['n', 'l', 'k'], ['f', 'a', 'g'], ['b', 'g', 'h'], ['l', 'd', 'h'], ['l', 'k', 'c'], ['d', 'm', 'h'], ['o', 'p', 's'], ['d', 'e', 'm'], ['a', 'g', 'b'], ['l', 'i', 'n'], ['j', 'k', 'c'], ['n', 'o', 'i'], ['s', 'o', 'r'], ['l', 'd', 'c'], ['n', 'q', 'k'], ['d', 'e', 'a'], ['n', 'q', 'r'], ['j', 'b', 'c'], ['d', 'a', 'c'], ['t', 'p', 's'], ['a', 'b', 'c'], ['f', 'g', 'm'], ['e', 'f', 'm'], ['u', 'q', 'r'], ['e', 'a', 'f'], ['k', 'j', 'p'], ['j', 'b', 'i']]
Coordinate Data:
e : [97538937536795917199 / 50000000000000000000, 26362363189313553049 / 25000000000000000000, -27765730014892817697 / 25000000000000000000]
n : [9691311121986551887 / 20000000000000000000, 7698602382641368399 / 25000000000000000000, 136198073306107219877 / 100000000000000000000]
t : [-124092034963422843613 / 100000000000000000000, 57569467334810731329 / 50000000000000000000, 19521753799748578401 / 12500000000000000000]
i : [5495587171565566533 / 10000000000000000000, -20394825645989010589 / 100000000000000000000, 50539325403763422849 / 100000000000000000000]
h : [139834561362946747279 / 100000000000000000000, -7880878980887340033 / 100000000000000000000, -103995265940044791 / 12500000000000000000]
q : [-6735875218496809281 / 25000000000000000000, 22956268160322561711 / 25000000000000000000, 160489834100394908351 / 100000000000000000000]
u : [-5503427814289170519 / 6250000000000000000, 32727736934366588123 / 50000000000000000000, 117561293737208367429 / 50000000000000000000]
s : [-28024397956534724057 / 25000000000000000000, 7982688762274505351 / 50000000000000000000, 75810016240962556489 / 50000000000000000000]
d : [158687908246366041587 / 100000000000000000000, 17708329632921932069 / 20000000000000000000, -152082360034378689 / 781250000000000000]
v : [-109524352181856898631 / 100000000000000000000, -8031245407815421203 / 25000000000000000000, 47851922281210359173 / 20000000000000000000]
o : [-3295513228237610619 / 10000000000000000000, -2509502772967543967 / 20000000000000000000, 48775380484303534549 / 50000000000000000000]
r : [-12236571522725722947 / 50000000000000000000, -88006469296704947 / 6250000000000000000, 49141439194966115751 / 25000000000000000000]
p : [-79028501764455206313 / 100000000000000000000, 7380583607139932421 / 10000000000000000000, 77048478672296447519 / 100000000000000000000]
a : [271809068893380997 / 250000000000000000, 28141143838174023551 / 50000000000000000000, -99858732725767148607 / 100000000000000000000]
k : [17279176899283116137 / 100000000000000000000, 20016243399745841903 / 20000000000000000000, 14236062273350904333 / 20000000000000000000]
c : [14675506497294124789 / 25000000000000000000, 43482257970787433013 / 50000000000000000000, -18886884252145287941 / 100000000000000000000]
m : [105483567122938042329 / 50000000000000000000, 17390683865674943887 / 100000000000000000000, -66417823304659739471 / 100000000000000000000]
b : [10404947614973782813 / 20000000000000000000, -8260868586164365207 / 100000000000000000000, -24339246633161575363 / 50000000000000000000]
j : [-9844660869817442669 / 50000000000000000000, 979098594202917673 / 3125000000000000000, 1084529851881945269 / 12500000000000000000]
l : [109575694568498694277 / 100000000000000000000, 62344720402140845541 / 100000000000000000000, 31804998792578300641 / 50000000000000000000]
f : [179107519179953137039 / 100000000000000000000, 1019448493679350419 / 5000000000000000000, -32231889345574623997 / 20000000000000000000]
g : [134510981681779720293 / 100000000000000000000, -40228246628143078843 / 100000000000000000000, -95305806686062265399 / 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 = 104166666666666666665547488721054724287742012789706364996391053178943436878847370969153303716741550785258912376885227 / 208333333333333333340004082838180360254091416859877141408468134809950501762718700000000000000000000000000000000000000
Collision distance in [707106781186547524385725108889 / 1000000000000000000000000000000, 70710678118654752438572510889 / 100000000000000000000000000000] ~ [0.70711, 0.70711]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [2297 / 5000, 1149 / 2500] ~ [0.4594, 0.4596]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 3853540146515744052854990629402112089020609 / 100000000000000000000000000000000000000000000000000000000000000000000000000000000
rho in [1963043592617276559305760001363 / 10000000000000000000000000000000000000000000000000, 1963043592627276559305760001363 / 10000000000000000000000000000000000000000000000000] ~ [0.0, 0.0]
sigma_min ^ 2 / (16 * E ^ .5) in [2638104500000000000000000000 / 1549193338482966754071706159913, 366722500000000000000000000 / 215165741455967604732181411099] ~ [0.0017, 0.0017]
Success: rho < sigma_min ^ 2 / (16 * E ^ .5)
Checking inequality 4:
LHS NUM := sigma_min - [sigma_min ^ 2 - 16 * rho * |E| ^ .5 ] ^ .5 in [-19999999999997353234067159 / 100000000000000000000000000000, 200000000000026479182036133 / 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 [-99999999999986766170335795 / 30983866769659335081434123198256, 66666666666675493060678711 / 20655911179772890054289415465504] ~ [-0.0, 0.0]
CD / |V| ^ .5 in [707106781186547524385725108889 / 4690415759823429554565630113545, 39283710065919306910318061605 / 260578653323523864142535006308] ~ [0.15076, 0.15076]
Success: LHS < CD / |V| ^ .5
Success: existence proven