show/hide visualization coordinates
a : (-0.041592082054775076, -0.315193111658783, 1.1468728592897346)
b : (-0.7870432300349548, -0.8765775285094219, 0.7874982323441193)
c : (0.14185059916678186, -1.2447905707734055, 0.8271896618678436)
d : (0.8202794633233103, -0.524063597702555, 0.6847575497322287)
e : (0.7494859850540226, 0.28412236604677166, 1.2694144845522204)
f : (-0.17095794032492762, 0.672954571427983, 1.229508391140648)
g : (-0.8417254215067526, 0.12052625205077039, 0.7346407945665152)
h : (-1.0496069419926797, -0.43500510929029956, -0.07044937430092069)
i : (-0.2998876094928423, -1.096637001297192, -0.05763680409124117)
j : (0.6897185466344832, -1.2320663920001838, -0.00927839335726488)
k : (1.038333317727185, -0.3324270738511852, -0.2721792085260051)
l : (1.3095150788428491, 0.31346579058691854, 0.44146135934142516)
m : (0.49391687535380246, 0.8875153857382145, 0.5140329293401016)
n : (-0.4853035972949412, 0.960101789016228, 0.32466957490019754)
o : (-1.3074563073840644, 0.5309496912157641, -0.04935368406449725)
p : (-1.1800322852953133, 0.0664806715857584, -0.925727832701178)
q : (-0.6992961956319134, -0.8103800456962607, -0.9285729307322679)
r : (0.2886957010745089, -0.7482009672158132, -0.7871311609407079)
s : (0.7886957010745089, 0.028162129356436874, -1.1708763137188858)
t : (0.8555776761317196, 0.6441267248492771, -0.38594675094793984)
u : (0.17682434682401918, 1.3734917836187643, -0.3003866609532766)
v : (-0.5673830823430438, 0.8110945800049012, -0.6607540953030775)
w : (-0.2113042989254911, 0.028162129356436874, -1.1708763137188858)
x : (0.2886957010745089, 0.8941875331408755, -1.1708763137188858)
show/hide computer existence proof
(see shape-existence, preprint)
Attempting to prove existence
Starting realization:
Abstract data:
mode: maximal_simplices
data: [['h', 'q', 'i'], ['f', 'n', 'm'], ['c', 'i', 'b'], ['n', 'o', 'v'], ['b', 'g', 'a'], ['q', 'p', 'w'], ['d', 'c', 'a'], ['o', 'h', 'g'], ['o', 'v', 'p'], ['j', 'd', 'c'], ['k', 'l', 'd'], ['e', 'l', 'd'], ['q', 'r', 'w'], ['h', 'q', 'p'], ['n', 'u', 'v'], ['v', 'p', 'w'], ['u', 'x', 't'], ['h', 'g', 'b'], ['o', 'h', 'p'], ['k', 't', 's'], ['f', 'e', 'a'], ['u', 'x', 'v'], ['h', 'i', 'b'], ['k', 'r', 's'], ['n', 'u', 'm'], ['b', 'c', 'a'], ['u', 'm', 't'], ['x', 't', 's'], ['j', 'r', 'i'], ['f', 'g', 'a'], ['q', 'r', 'i'], ['r', 's', 'w'], ['e', 'm', 'l'], ['x', 'v', 'w'], ['n', 'o', 'g'], ['j', 'r', 'k'], ['l', 'm', 't'], ['x', 'w', 's'], ['f', 'n', 'g'], ['k', 'l', 't'], ['j', 'd', 'k'], ['e', 'd', 'a'], ['j', 'c', 'i'], ['f', 'e', 'm']]
Coordinate Data:
w : [-233878018701971952268317858127 / 1000000000000000000000000000000000000000000000000000000000, -72001334578843900086662381999 / 500000000000000000000000000000000000000000000000000000000, 35250025095414715752334119417 / 20000000000000000000000000000000000000000000000000000000000000000000000000000000000]
d : [805924814256875975055488207 / 781250000000000000000000000, -138056431764747977063685240827 / 250000000000000000000000000000, 37112677269022287994095072899 / 20000000000000000000000000000]
m : [705221174279293554441638424237 / 1000000000000000000000000000000, 429676628190888822226640069013 / 500000000000000000000000000000, 168490924305898746302669460049 / 100000000000000000000000000000]
q : [-30499493544151389320455817923 / 62500000000000000000000000000, -33541687002107902986013482307 / 40000000000000000000000000000, 242303382986617904200343310237 / 1000000000000000000000000000000]
r : [25000000000000000000000000053 / 50000000000000000000000000000, -776363096572250070649770058659 / 1000000000000000000000000000000, 383745152778177916883781978859 / 1000000000000000000000000000000]
v : [-356078783417552709074780571781 / 1000000000000000000000000000000, 782932450648464271946193129351 / 1000000000000000000000000000000, 510122218415808318033549108943 / 1000000000000000000000000000000]
n : [-68499824592362516960217680703 / 250000000000000000000000000000, 931939659659791136756752310397 / 1000000000000000000000000000000, 37388647215477084877094156227 / 25000000000000000000000000000]
h : [-419151321533594297411169703979 / 500000000000000000000000000000, -463167238646736440582168745663 / 1000000000000000000000000000000, 27510673485449126533111123507 / 25000000000000000000000000000]
t : [106688197505721079734542936941 / 100000000000000000000000000000, 123192919098568050879668466107 / 200000000000000000000000000000, 784929562770945907833931153101 / 1000000000000000000000000000000]
f : [40346358600563500045906627603 / 1000000000000000000000000000000, 322396221035773009257840148223 / 500000000000000000000000000000, 240038470485953379910863421651 / 100000000000000000000000000000]
e : [960790283979513697433006329597 / 1000000000000000000000000000000, 255960236690334784957770639663 / 1000000000000000000000000000000, 122014539913555300210816435329 / 50000000000000000000000000000]
k : [62481880832633805103863706157 / 50000000000000000000000000000, -360589203207622068255670334207 / 1000000000000000000000000000000, 5616856907455504693420766583 / 6250000000000000000000000000]
j : [901022845559974287668127813319 / 1000000000000000000000000000000, -15752856516957758149409730739 / 12500000000000000000000000000, 116159792036162080962156062879 / 100000000000000000000000000000]
u : [97032161437377563977370204333 / 250000000000000000000000000000, 67266482713116367154970577153 / 50000000000000000000000000000, 870489652765609135059752816291 / 1000000000000000000000000000000]
x : [7812500000000000000000000001 / 15625000000000000000000000000, 86602540378443864676372317093 / 100000000000000000000000000000, -187164195736550262818011758633 / 100000000000000000000000000000000000000000000000000000000000000000000000000000000000]
a : [42428054217679006859170958403 / 250000000000000000000000000000, -343355241015219858222025622897 / 1000000000000000000000000000000, 231774917300862041853008178763 / 100000000000000000000000000000]
b : [-287869465554731836840253631051 / 500000000000000000000000000000, -90473965786585891226194799479 / 100000000000000000000000000000, 195837454606300513970453998509 / 100000000000000000000000000000]
i : [-88583310567351190531800194247 / 1000000000000000000000000000000, -28119978266340723820000678749 / 25000000000000000000000000000, 27830987740691117602082846661 / 25000000000000000000000000000]
p : [-968727986369822110300411325141 / 1000000000000000000000000000000, 38318542229321530295590338109 / 1000000000000000000000000000000, 245148481017707817758991866153 / 1000000000000000000000000000000]
c : [176577449046136489650166588951 / 500000000000000000000000000000, -25459054002596849130953152351 / 20000000000000000000000000000, 24975824694834116428663299703 / 12500000000000000000000000000]
s : [100000000000000000000000000017 / 100000000000000000000000000000, -40764660407757193021079451403 / 1250000000000000000000000000000000000000000000000000000000, 315159570839378944834294924947 / 1000000000000000000000000000000000000000000000000000000000000000000000000000000000000]
o : [-109615200845857322128110626067 / 100000000000000000000000000000, 50278756185932713890652470027 / 100000000000000000000000000000, 112152262965438852753818970921 / 100000000000000000000000000000]
l : [30416387555366804266624954239 / 20000000000000000000000000000, 285303661230481649282300044671 / 1000000000000000000000000000000, 161233767306031095730374844211 / 100000000000000000000000000000]
g : [-630421122581261467803475253571 / 1000000000000000000000000000000, 92364122694333507618114656361 / 1000000000000000000000000000000, 190551710828540107335351370941 / 100000000000000000000000000000]
Desired square lengths:
default : 1
Checking inequality 1:
d = 3
|V| = 24
|E| = 66
Success: d|V| >= |E|
Checking self-intersection:
Square collision distance = 742138535718220655861077208799311823025075248347849388980791893078583797881532987868448566063238682075916661621256601 / 1090852671187996392742386195247514299221239337558469402872940333069485233099324384000000000000000000000000000000000000
Collision distance in [164964098281007533763854272739 / 200000000000000000000000000000, 51551280712814854301204460231 / 62500000000000000000000000000] ~ [0.82482, 0.82482]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [45465777392090094999 / 100000000000000000000, 45465777392090095001 / 100000000000000000000] ~ [0.45466, 0.45466]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 7575801255209077638933069073698123325712529243770118948418261880278864754214999271408818175191169636761101121799868690181564108366621669844106132356318537176428993054098662495166351532457066864497783695930857456782793333999252605835082889325149519338548983708717310576160254956197690033 / 200000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000
rho in [486563242780713631885024962019 / 2500000000000000000000000000000000000000000000000000000, 486565742780713631885024962019 / 2500000000000000000000000000000000000000000000000000000] ~ [0.0, 0.0]
sigma_min ^ 2 / (16 * E ^ .5) in [2067136913867090800001341042324844810001 / 1299846144741753657673581370922720000000000, 159010531835930061552554165530246553077 / 99988164980134896744121643917120000000000] ~ [0.00159, 0.00159]
Success: rho < sigma_min ^ 2 / (16 * E ^ .5)
Checking inequality 4:
LHS NUM := sigma_min - [sigma_min ^ 2 - 16 * rho * |E| ^ .5 ] ^ .5 in [-7909905001 / 100000000000000000000, 2090095001 / 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 [-4943690625625000000 / 4062019202317980180229941784133, 1306309375625000000 / 4062019202317980180229941784133] ~ [-0.0, 0.0]
CD / |V| ^ .5 in [824820491405037668819271363695 / 4898979485566356196394568149412, 824820491405037668819271363696 / 4898979485566356196394568149411] ~ [0.16837, 0.16837]
Success: LHS < CD / |V| ^ .5
Success: existence proven