show/hide visualization coordinates
a : (-0.4742168878575055, -0.3174405198199128, 0.514339351312822)
b : (-1.3056918275870777, 0.2000487001951442, 0.31221480611874586)
c : (-1.3184395688512038, -0.7993409487485253, 0.2796905893424436)
d : (-0.44614154354890423, -1.2883041818055485, 0.2763571568574493)
e : (0.39785676013654103, -0.7521200163471906, 0.28952545544971464)
f : (0.3832865034999845, 0.1741251352424466, 0.6661653720520777)
g : (-0.41920360104822574, 0.6626595095518055, 0.32361056297714175)
h : (-0.9370543109923357, 0.5951879524190907, -0.5291955293958363)
i : (-1.9247930766632286, 0.5826649808000788, -0.3735828500513491)
j : (-1.4372174807154585, -0.2701780907651035, -0.5604751546533375)
k : (-0.9372174807154585, -1.1359522692159558, -0.5813335325325448)
l : (-1.2964728544961495, -1.781449614142014, 0.09266109215158835)
m : (0.06272812148670437, -1.1359836757991801, -0.5709032089431181)
n : (0.5627281214867044, -0.26995827201474165, -0.5709032089431181)
o : (1.1983707176425256, -0.16058247289749356, 0.19329272438795586)
p : (1.247301148744, 0.6711791998213578, 0.746264995580791)
q : (0.49118404973892893, 1.0639454399337702, 0.22279425788849727)
r : (0.06272812148670437, 0.5958159064361106, -0.5500448310639107)
s : (-0.43727187851329563, -0.26995827201474165, -0.5709032089431181)
t : (1.0578605343118828, 0.5906338656805898, -0.45163432655170477)
u : (1.9281775683461648, 0.5040592128722329, 0.03318841400496797)
v : (2.1133212957625376, 1.171115039294695, 0.7548242810696655)
w : (1.4281775683461646, 1.3698333913230853, 0.05404679188417538)
show/hide computer existence proof
(see shape-existence, preprint)
Attempting to prove existence
Starting realization:
Abstract data:
mode: maximal_simplices
data: [['d', 'l', 'k'], ['t', 'q', 'w'], ['o', 'f', 'p'], ['b', 'c', 'j'], ['q', 'g', 'r'], ['o', 'n', 't'], ['b', 'g', 'a'], ['e', 'f', 'o'], ['b', 'h', 'g'], ['t', 'n', 'r'], ['b', 'c', 'a'], ['w', 'v', 'p'], ['u', 'o', 't'], ['b', 'i', 'j'], ['s', 'n', 'r'], ['c', 'l', 'k'], ['d', 'c', 'l'], ['u', 'v', 'p'], ['q', 'r', 't'], ['d', 'e', 'a'], ['u', 'v', 'w'], ['h', 'j', 'i'], ['m', 'e', 'n'], ['m', 's', 'k'], ['m', 's', 'n'], ['c', 'j', 'k'], ['s', 'j', 'k'], ['q', 'f', 'g'], ['w', 'q', 'p'], ['u', 'o', 'p'], ['e', 'f', 'a'], ['m', 'd', 'k'], ['m', 'd', 'e'], ['h', 's', 'r'], ['w', 'u', 't'], ['f', 'g', 'a'], ['q', 'f', 'p'], ['h', 'j', 's'], ['d', 'c', 'a'], ['b', 'h', 'i'], ['e', 'n', 'o'], ['h', 'g', 'r']]
Coordinate Data:
n : [225248088698534783045557148249 / 6250000000000000000000000000000000000000000000000000000000000000000000000000000000000000, 1360366802467733524742307864967 / 50000000000000000000000000000000000000000000000000000000000000000000000000000000000000000, 1639739577838581331292546980599 / 100000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000]
r : [1 / 2, -432887089225426135531718920563 / 500000000000000000000000000000, -5214594469801840676317226953 / 250000000000000000000000000000]
f : [89720808993359939673157731333 / 500000000000000000000000000000, -222041703628594138435677966639 / 500000000000000000000000000000, -4948274323980782980666112739 / 4000000000000000000000000000]
j : [1999945602202162984130058799401 / 1000000000000000000000000000000, 13738671897615734100940637 / 62500000000000000000000000000, -651753393111287509168186267 / 62500000000000000000000000000]
m : [1 / 2, 13531646934131853855683174543 / 15625000000000000000000000000, 169052647517149900607973978543 / 12500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000]
q : [35772035873887717646554852221 / 500000000000000000000000000000, -1333903711948512029691171207181 / 1000000000000000000000000000000, -793697466831615389142510875201 / 1000000000000000000000000000000]
e : [10304460084385209165847777413 / 62500000000000000000000000000, 482161744332448895183084253357 / 1000000000000000000000000000000, -860428664392832771408968101087 / 1000000000000000000000000000000]
d : [1008869665035608694220344567663 / 1000000000000000000000000000000, 509172954895403394113714803769 / 500000000000000000000000000000, -847260365800567454668868037607 / 1000000000000000000000000000000]
k : [1499945602202162984130058799401 / 1000000000000000000000000000000, 432996998600607061404526445659 / 500000000000000000000000000000, 521516179471338127928896377 / 50000000000000000000000000000]
w : [-865449446859460391208828612481 / 1000000000000000000000000000000, -1639791663337826829698908659819 / 1000000000000000000000000000000, -624950000827293431254209499659 / 1000000000000000000000000000000]
h : [374945608119759994672034932177 / 250000000000000000000000000000, -432573112216916196648503479999 / 500000000000000000000000000000, -417076795472818724250090161 / 10000000000000000000000000000]
v : [-1550593174275833240368082392707 / 1000000000000000000000000000000, -1441073311309436742488041796789 / 1000000000000000000000000000000, -662863745006391807969426573021 / 500000000000000000000000000000]
a : [1036945009344209879942211016943 / 1000000000000000000000000000000, 47482247805171116813423476803 / 1000000000000000000000000000000, -1085242560255940229548896692213 / 1000000000000000000000000000000]
g : [9819317225349300928722759169 / 10000000000000000000000000000, -932617781566547215347524590359 / 1000000000000000000000000000000, -44725688596012990248245049309 / 50000000000000000000000000000]
t : [-49513241282517836453443228813 / 100000000000000000000000000000, -860592137695331475802348563473 / 1000000000000000000000000000000, -119268882391413295841404490733 / 1000000000000000000000000000000]
p : [-684573027257295686614480124923 / 1000000000000000000000000000000, -941137471836099382309584187939 / 1000000000000000000000000000000, -658584102261954512638833161871 / 500000000000000000000000000000]
c : [1881167690337908277428915057149 / 1000000000000000000000000000000, 529382676733783673980414668047 / 1000000000000000000000000000000, -170118759657112328526020611453 / 200000000000000000000000000000]
i : [2487521198149932973395367479591 / 1000000000000000000000000000000, -170524650562964076028107525719 / 200000000000000000000000000000, -197320358891768959465962298001 / 1000000000000000000000000000000]
o : [-635642596155821066998980357561 / 1000000000000000000000000000000, -27343949779312027269927263323 / 250000000000000000000000000000, -764195933331073907685435477969 / 1000000000000000000000000000000]
b : [934209974536891058889155644173 / 500000000000000000000000000000, -58750871526235729985115805561 / 125000000000000000000000000000, -883118015061863938672308046151 / 1000000000000000000000000000000]
u : [-1365449446859460391208828612481 / 1000000000000000000000000000000, -193504371221743639658867704673 / 250000000000000000000000000000, -302045811474043034274470295923 / 500000000000000000000000000000]
l : [1859200975982853933035383958491 / 1000000000000000000000000000000, 1511491342127272262500691962597 / 1000000000000000000000000000000, -663564301094706425609417521181 / 1000000000000000000000000000000]
s : [1, -2028534637648317033326827182643 / 100000000000000000000000000000000000000000000000000000000000000000000000000000000000000000, -4707745693852674136332537077729 / 100000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000]
Desired square lengths:
default : 1
Checking inequality 1:
d = 3
|V| = 23
|E| = 63
Success: d|V| >= |E|
Checking self-intersection:
Square collision distance = 78128311014732336161919164872526254009949016230862147019189706054609540878219795939016588477561701207172232362352889 / 156264514044918887420426031062817349657280387118802090781530818729845539974013281250000000000000000000000000000000000
Collision distance in [141417785005452774734232386123 / 200000000000000000000000000000, 88386115628407984208895241327 / 125000000000000000000000000000] ~ [0.70709, 0.70709]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [37 / 1000, 93 / 2500] ~ [0.037, 0.0372]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 5363402852418480530518459835414505071754087785633799991366025453998473515307270984930745701211501094593424534318133106029614449636273633341433956908804527889736110406548071449837920829295592772735865615589752778202382686346517765671904604320775500316626919904970298952390638936206150894362555773218975070717152211520812604222744760241952923158254695348822656919090428386161722422770380165518163319313992911882060991568649899843192437258337090475285655896633028163650110928107798454172541168870773516469 / 50000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000
rho in [1035702935442251272034922725919 / 100000000000000000000000000000000000000000000000000000000000, 1135702935442251272034922725919 / 100000000000000000000000000000000000000000000000000000000000] ~ [0.0, 0.0]
sigma_min ^ 2 / (16 * E ^ .5) in [42781250000000000000000000 / 3968626966596885885752423630459, 28830000000000000000000000 / 2645751311064590590501615753639] ~ [1e-05, 1e-05]
Success: rho < sigma_min ^ 2 / (16 * E ^ .5)
Checking inequality 4:
LHS NUM := sigma_min - [sigma_min ^ 2 - 16 * rho * |E| ^ .5 ] ^ .5 in [-1 / 5000, 2000001 / 10000000000] ~ [-0.0002, 0.0002]
LHS DEN := 8 * |E| ^ .5 in [7937253933193771771504847260917 / 125000000000000000000000000000, 3968626966596885885752423630459 / 62500000000000000000000000000] ~ [63.49803, 63.49803]
LHS := (LHS NUM) / (LHS DEN) in [-25000000000000000000000000 / 7937253933193771771504847260917, 8333337500000000000000000 / 2645751311064590590501615753639] ~ [-0.0, 0.0]
CD / |V| ^ .5 in [707088925027263873671161930615 / 4795831523312719541597438064163, 11404660081084901188244547268 / 77352121343753540993507065551] ~ [0.14744, 0.14744]
Success: LHS < CD / |V| ^ .5
Success: existence proven