show/hide visualization coordinates
a : (0.6974556845493424, -0.31938722200541936, 0.1670783212494768)
b : (0.14300697566180331, -0.41367080122731564, -0.659781543480968)
c : (0.8721568692737708, 0.2696355539449309, -0.6219284375730474)
d : (1.0603780750551097, 0.6026078654665596, 0.30203163594428944)
e : (0.32100525859878226, 0.26599245941924476, 0.8851421800926862)
f : (0.239292429159356, -0.7281127836099146, 0.9564007184367986)
g : (0.11292224497572301, -1.1216441815856069, 0.0458165019270394)
h : (-0.6868087401299033, -0.5438228650237462, -0.11713403531878414)
i : (-0.48334781900982116, 0.3518444891324729, -0.5125877548306453)
j : (0.13851767753254574, 0.3580831313764883, -1.2956869717585304)
k : (0.958543739661862, 0.9252951386095654, -1.3720269762077724)
l : (0.8591519634220269, 1.2513296461193946, -0.43190848647963515)
m : (0.11380412984707744, 0.8601405286084689, 0.1079319356139245)
n : (-0.5917563907356497, 0.25505898131125593, 0.47679596600377144)
o : (-0.4453397348120685, -0.13818660875317512, 1.3844963949796716)
p : (-0.5853169909101352, -1.1279479825066345, 1.3565895714248317)
q : (0.05816329595205583, -1.7063523613785367, 0.8552099797763868)
r : (-0.7791800570869019, -1.3881364665751894, 0.4106936657720743)
s : (-1.136298733940662, -0.5284835140863227, 0.7760196187502248)
t : (-0.06487150871496983, 1.2093244747639682, -0.8119297865659464)
u : (0.10372731122754009, 1.2223427220393839, -1.7975285706316884)
v : (0.605413341161901, 1.8441967005535287, -1.1961894343908903)
w : (-1.5106190207387886, -1.4001069045934016, 1.0924955072667315)
show/hide computer existence proof
(see shape-existence, preprint)
Attempting to prove existence
Starting realization:
Abstract data:
mode: maximal_simplices
data: [['t', 'v', 'u'], ['l', 'd', 'm'], ['b', 'j', 'i'], ['l', 'd', 'c'], ['b', 'j', 'c'], ['p', 'w', 's'], ['t', 'm', 'i'], ['d', 'e', 'a'], ['r', 'p', 'w'], ['b', 'h', 'i'], ['r', 's', 'h'], ['k', 'j', 'c'], ['r', 'g', 'q'], ['e', 'o', 'n'], ['b', 'g', 'a'], ['l', 'k', 'c'], ['t', 'j', 'i'], ['g', 'f', 'a'], ['p', 's', 'o'], ['e', 'a', 'f'], ['m', 'e', 'n'], ['r', 'p', 'q'], ['p', 'f', 'q'], ['k', 'j', 'u'], ['l', 'v', 'k'], ['t', 'l', 'v'], ['v', 'k', 'u'], ['g', 'f', 'q'], ['s', 'n', 'h'], ['m', 'n', 'i'], ['r', 'g', 'h'], ['t', 'l', 'm'], ['s', 'n', 'o'], ['n', 'h', 'i'], ['e', 'o', 'f'], ['b', 'a', 'c'], ['m', 'e', 'd'], ['t', 'j', 'u'], ['d', 'a', 'c'], ['p', 'f', 'o'], ['b', 'g', 'h'], ['r', 's', 'w']]
Coordinate Data:
v : [110543569509608784321 / 100000000000000000000, 59740307567297053029 / 25000000000000000000, -17986564824067786719 / 25000000000000000000]
h : [-2334829827446458041 / 12500000000000000000, 6370948458429777 / 4000000000000000000, 8989820152734870813 / 25000000000000000000]
j : [3192700157333661977 / 5000000000000000000, 45174936675742092951 / 50000000000000000000, -81896013033035138129 / 100000000000000000000]
n : [-4586701840073146129 / 50000000000000000000, 16009491668992190593 / 20000000000000000000, 95352280743195037583 / 100000000000000000000]
f : [73931478309354275921 / 100000000000000000000, -913485907357804801 / 5000000000000000000, 71656377993248875597 / 50000000000000000000]
o : [683532739026477563 / 12500000000000000000, 79536912770542671 / 195312500000000000, 186122323640785049667 / 100000000000000000000]
w : [-50529833340230104491 / 50000000000000000000, -667727580043006167 / 781250000000000000, 156922234869491042529 / 100000000000000000000]
m : [30691324189063207177 / 50000000000000000000, 28111122614936448423 / 20000000000000000000, 58465877704210347957 / 100000000000000000000]
c : [68608961160397872979 / 50000000000000000000, 40752557804164222603 / 50000000000000000000, -14520159614486838271 / 100000000000000000000]
d : [156040042898929622417 / 100000000000000000000, 114802346760491329481 / 100000000000000000000, 38937923868623417043 / 50000000000000000000]
g : [30647229945495485223 / 50000000000000000000, -11524571588945063507 / 20000000000000000000, 13063583583880457963 / 25000000000000000000]
t : [10878771130480421851 / 25000000000000000000, 87737003845116087789 / 50000000000000000000, -33520294513776741637 / 100000000000000000000]
u : [60374966516172676919 / 100000000000000000000, 88387916208886871497 / 50000000000000000000, -33020043230087737103 / 25000000000000000000]
q : [6977320623578031083 / 12500000000000000000, -116093675924018319911 / 100000000000000000000, 16649210265057071579 / 12500000000000000000]
e : [82102761253296891493 / 100000000000000000000, 5071300384734989759 / 6250000000000000000, 68093451076043257381 / 50000000000000000000]
a : [119747803848352902049 / 100000000000000000000, 4520567602658685093 / 20000000000000000000, 32190258133882785003 / 50000000000000000000]
b : [64302932959598999453 / 100000000000000000000, 823405005693987261 / 6250000000000000000, -71505742989370727 / 390625000000000000]
r : [-27915770315271509479 / 100000000000000000000, -1685441728873671511 / 2000000000000000000, 88742050720025321337 / 100000000000000000000]
i : [1667453492436556629 / 100000000000000000000, 89726009127082648539 / 100000000000000000000, -1793045670123317557 / 50000000000000000000]
k : [72928304679802436427 / 50000000000000000000, 14707107407479189849 / 10000000000000000000, -44765006738979670047 / 50000000000000000000]
p : [-8529463697594856473 / 100000000000000000000, -58253238036828098057 / 100000000000000000000, 183331641285301057659 / 100000000000000000000]
s : [-6362763800064753597 / 10000000000000000000, 211651100650387297 / 12500000000000000000, 12527464601784036407 / 10000000000000000000]
l : [135917431735621353459 / 100000000000000000000, 35934904965154963847 / 20000000000000000000, 4481835494854382261 / 100000000000000000000]
Desired square lengths:
default : 1
Checking inequality 1:
d = 3
|V| = 23
|E| = 63
Success: d|V| >= |E|
Checking self-intersection:
Square collision distance = 499999999999999999990500488340926879506316593177841767602851808965290165624010537486881162015456239457937807779722057049 / 999999999999999999997536176879569986909740262246478320833124771190437961609849010000000000000000000000000000000000000000
Collision distance in [70710678118654752439499828601 / 100000000000000000000000000000, 707106781186547524394998286011 / 1000000000000000000000000000000] ~ [0.70711, 0.70711]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [1233 / 2500, 2467 / 5000] ~ [0.4932, 0.4934]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 993678706753015821525073709626503711504011 / 25000000000000000000000000000000000000000000000000000000000000000000000000000000
rho in [498417171341692395529963326889 / 2500000000000000000000000000000000000000000000000, 498417171344192395529963326889 / 2500000000000000000000000000000000000000000000000] ~ [0.0, 0.0]
sigma_min ^ 2 / (16 * E ^ .5) in [7601445000000000000000000000 / 3968626966596885885752423630459, 15215222500000000000000000000 / 7937253933193771771504847260917] ~ [0.00192, 0.00192]
Success: rho < sigma_min ^ 2 / (16 * E ^ .5)
Checking inequality 4:
LHS NUM := sigma_min - [sigma_min ^ 2 - 16 * rho * |E| ^ .5 ] ^ .5 in [-12499999999998396407112443 / 62500000000000000000000000000, 100000000000012833945348331 / 500000000000000000000000000000] ~ [-0.0002, 0.0002]
LHS DEN := 8 * |E| ^ .5 in [7937253933193771771504847260917 / 125000000000000000000000000000, 3968626966596885885752423630459 / 62500000000000000000000000000] ~ [63.49803, 63.49803]
LHS := (LHS NUM) / (LHS DEN) in [-24999999999996792814224886 / 7937253933193771771504847260917, 100000000000012833945348331 / 31749015732775087086019389043668] ~ [-0.0, 0.0]
CD / |V| ^ .5 in [707106781186547524394998286010 / 4795831523312719541597438064163, 707106781186547524394998286011 / 4795831523312719541597438064162] ~ [0.14744, 0.14744]
Success: LHS < CD / |V| ^ .5
Success: existence proven