show/hide visualization coordinates
a : (0.7379849917069011, 0.04221513159793289, 0.9388020452568673)
b : (-0.2380585398770857, 0.244748672948495, 0.8593087179830707)
c : (0.0858778153520251, -0.6972640971337076, 0.7716892066688981)
d : (1.0561745453278713, -0.9048420731659084, 0.8959294564455109)
e : (1.3844399147230377, -0.23638885521453423, 0.22853741074350542)
f : (1.4135681126430466, 0.6939485645491428, 0.5940833496805926)
g : (0.43748246111921885, 0.8955374378952925, 0.5127277903601952)
h : (-0.46062280378536263, 0.828068175176117, 0.07815347940888928)
i : (-1.191864648876605, 0.4663583072506913, 0.6564711563243772)
j : (-0.870076135835218, -0.4771552672707532, 0.5775136514981742)
k : (-0.3286720043159742, -0.9870937896181904, -0.09095046107631954)
l : (0.6634905385784741, -0.8819351109155882, -0.023458678089464446)
m : (1.1634922778724377, -0.38809158994311765, -0.734877568404112)
n : (1.214723290357929, 0.5432249902560862, -0.37428803610211697)
o : (1.1060737661038011, 1.4546880963090305, 0.022486820943626973)
p : (0.3479176178163971, 1.0318234185283683, -0.4738847325316551)
q : (-0.3286720043159742, 0.3727870308175143, -0.8023623160831113)
r : (-1.207242278471886, 0.3026795459138074, -0.3299226755679626)
s : (-1.7925469834757524, -0.23656578201127598, 0.27557949504029033)
t : (-1.3273886266216504, -1.0282715904302218, -0.12043769646090607)
u : (-0.8286720043159742, -0.4932383729669243, -0.8023623160831113)
v : (0.1713279956840258, -0.4932383729669243, -0.8023623160831113)
w : (0.6104660134529086, 0.3376483489929646, -1.1441006028183944)
x : (-1.8192033108465937, -0.3896428185982984, -0.7122751810537361)
show/hide computer existence proof
(see shape-existence, preprint)
Attempting to prove existence
Starting realization:
Abstract data:
mode: maximal_simplices
data: [['i', 'r', 'h'], ['i', 's', 'r'], ['w', 'p', 'n'], ['e', 'd', 'a'], ['x', 's', 'r'], ['l', 'm', 'v'], ['x', 't', 'u'], ['k', 'v', 'u'], ['o', 'p', 'n'], ['w', 'q', 'v'], ['l', 'd', 'c'], ['f', 'e', 'n'], ['q', 'p', 'h'], ['b', 'g', 'a'], ['k', 'l', 'v'], ['b', 'i', 'j'], ['k', 't', 'j'], ['t', 's', 'j'], ['f', 'e', 'a'], ['e', 'm', 'n'], ['b', 'c', 'j'], ['f', 'o', 'n'], ['f', 'g', 'a'], ['t', 'x', 's'], ['o', 'p', 'g'], ['d', 'c', 'a'], ['u', 'x', 'r'], ['q', 'r', 'h'], ['w', 'm', 'n'], ['k', 'c', 'j'], ['k', 't', 'u'], ['p', 'g', 'h'], ['u', 'q', 'v'], ['w', 'q', 'p'], ['b', 'g', 'h'], ['w', 'm', 'v'], ['l', 'e', 'm'], ['i', 's', 'j'], ['q', 'r', 'u'], ['k', 'l', 'c'], ['b', 'i', 'h'], ['f', 'o', 'g'], ['b', 'c', 'a'], ['l', 'e', 'd']]
Coordinate Data:
u : [-164814078814336292802764107069 / 100000000000000000000000000000000000000000000000000000, -20788041149012717246292254527 / 200000000000000000000000000000000000000000000000000000, 62788011235430140215765150739 / 500000000000000000000000000000000000000000000000000000000000000000000]
a : [78332849801143768592219589311 / 50000000000000000000000000000, 4283628036518857305660718413 / 8000000000000000000000000000, 87058218066998929037727663327 / 50000000000000000000000000000]
d : [188484654964384545961769152431 / 100000000000000000000000000000, -51450462524872999184995506783 / 125000000000000000000000000000, 84914588626431107614394224637 / 50000000000000000000000000000]
p : [58829481106618568709038596341 / 50000000000000000000000000000, 152506179149529263851963909717 / 100000000000000000000000000000, 41059697943932019081889043121 / 125000000000000000000000000000]
i : [-72638528912126129775191329559 / 200000000000000000000000000000, 479798340108807809216394441949 / 500000000000000000000000000000, 911770920254680347073165403 / 625000000000000000000000000]
l : [29843250857888967661061503703 / 20000000000000000000000000000, -388696737948663805027910525683 / 1000000000000000000000000000000, 778903637993646833158941721857 / 1000000000000000000000000000000]
x : [-990531306530619558386722998503 / 1000000000000000000000000000000, 20719110873725172107358907979 / 200000000000000000000000000000, 45043567514687596025080471239 / 500000000000000000000000000000]
q : [250000000000000000000000024267 / 500000000000000000000000000000, 86602540378443864676372329457 / 100000000000000000000000000000, 246191783868499099309226535513 / 25000000000000000000000000000000000000000000000000000000000000000000000]
f : [112112005847951042601995675983 / 50000000000000000000000000000, 118718693751606701723061486279 / 100000000000000000000000000000, 17455570822046299782251442223 / 12500000000000000000000000000]
r : [-378570274155911581151924420559 / 1000000000000000000000000000000, 159183583776146348296935818883 / 200000000000000000000000000000, 236219820257574317294646586447 / 500000000000000000000000000000]
s : [-240968744789944541310321315197 / 250000000000000000000000000000, 25667259095564830037433696067 / 100000000000000000000000000000, 13474272639042520606075605357 / 12500000000000000000000000000]
m : [24902053527355146808767493673 / 12500000000000000000000000000, 105146783023806669273628880193 / 1000000000000000000000000000000, 33742373839499610640773268843 / 500000000000000000000000000000]
v : [100000000000000000000000159961 / 100000000000000000000000000000, -198770374601281868967877769497 / 10000000000000000000000000000000000000000000000000000000, -135423693825617538960446071237 / 1000000000000000000000000000000000000000000000000000000000000000000000]
k : [249999999999999999999999443069 / 500000000000000000000000000000, -493855416651266026597604842679 / 1000000000000000000000000000000, 711411855006791712511013160117 / 1000000000000000000000000000000]
g : [126615446543519311104599929251 / 100000000000000000000000000000, 13887758108622167438149704543 / 10000000000000000000000000000, 131509010644330646186145203221 / 100000000000000000000000000000]
b : [295306732219444248965647283591 / 500000000000000000000000000000, 737987045915419313842971084963 / 1000000000000000000000000000000, 10385443962913636798321080791 / 6250000000000000000000000000]
h : [368049200530611599168735230261 / 1000000000000000000000000000000, 132130654814304127564230754337 / 100000000000000000000000000000, 440257897746000260027307027281 / 500000000000000000000000000000]
j : [-41404131519243850684582547379 / 1000000000000000000000000000000, 8041552848085566672788436469 / 500000000000000000000000000000, 4312112398691517505628233241 / 3125000000000000000000000000]
e : [1728993686749228156447148949 / 781250000000000000000000000, 3210618971904875573668704681 / 12500000000000000000000000000, 103089972682661674986358091273 / 100000000000000000000000000000]
w : [71956900888444141945861203263 / 50000000000000000000000000000, 830886721959888933731947990927 / 1000000000000000000000000000000, -68347657347056617538739453219 / 200000000000000000000000000000]
c : [457274909833999677541732261193 / 500000000000000000000000000000, -40805144833356677633535937931 / 200000000000000000000000000000, 157405152275200932927110002183 / 100000000000000000000000000000]
o : [193474577041977526120180113999 / 100000000000000000000000000000, 194792646927595484527156392681 / 100000000000000000000000000000, 41242456851336909474092705273 / 50000000000000000000000000000]
t : [-249358311152838089091856593059 / 500000000000000000000000000000, -535033217463297569233728926183 / 1000000000000000000000000000000, 34096230981110260645054336307 / 50000000000000000000000000000]
n : [40867905893478070567113574191 / 20000000000000000000000000000, 51823168161150518880870097169 / 50000000000000000000000000000, 107018569995248574960483622777 / 250000000000000000000000000000]
Desired square lengths:
default : 1
Checking inequality 1:
d = 3
|V| = 24
|E| = 66
Success: d|V| >= |E|
Checking self-intersection:
Square collision distance = 562443566521745218088944893342492575452953325184093013583444434504309599656702834497035722094021546413260907589168025049 / 933687455575535055651403405818400176398807106887503344604043760444370343835731100000000000000000000000000000000000000000
Collision distance in [31045503386853675919520821911 / 40000000000000000000000000000, 12127149760489717156062821059 / 15625000000000000000000000000] ~ [0.77614, 0.77614]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [41732378364958449999 / 100000000000000000000, 41732378364958450001 / 100000000000000000000] ~ [0.41732, 0.41732]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 398686605626336713373751748494078540215092112422493141603184407052252422377938517550065155015873927346648509833551835932359102215551708348259412668061959169487095241920329197773561692625584486585198177396016672905001132219438813719709606333 / 195312500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000
rho in [1428732102532467061550664233851 / 1000000000000000000000000000000000000000000000000000, 1428732103532467061550664233851 / 1000000000000000000000000000000000000000000000000000] ~ [0.0, 0.0]
sigma_min ^ 2 / (16 * E ^ .5) in [1741591403996052112499405469672583100001 / 1299846144741753657673581370922720000000000, 1741591403996052112666334983132416900001 / 1299846144741753657673581370922560000000000] ~ [0.00134, 0.00134]
Success: rho < sigma_min ^ 2 / (16 * E ^ .5)
Checking inequality 4:
LHS NUM := sigma_min - [sigma_min ^ 2 - 16 * rho * |E| ^ .5 ] ^ .5 in [-5041550001 / 100000000000000000000, 4958450001 / 100000000000000000000] ~ [-0.0, 0.0]
LHS DEN := 8 * |E| ^ .5 in [4062019202317980180229941784133 / 62500000000000000000000000000, 8124038404635960360459883568267 / 125000000000000000000000000000] ~ [64.99231, 64.99231]
LHS := (LHS NUM) / (LHS DEN) in [-3150968750625000000 / 4062019202317980180229941784133, 3099031250625000000 / 4062019202317980180229941784133] ~ [-0.0, 0.0]
CD / |V| ^ .5 in [258712528223780632662673515925 / 1632993161855452065464856049804, 776137584671341897988020547776 / 4898979485566356196394568149411] ~ [0.15843, 0.15843]
Success: LHS < CD / |V| ^ .5
Success: existence proven