show/hide visualization coordinates
a : (0.12787836657518842, -0.2353580142748239, 1.180017753156927)
b : (-0.16165694400996766, 0.7017989581468453, 0.9853228303525352)
c : (-0.3825014675869477, 0.2830334973510628, 1.8661537932793348)
d : (-0.8172615066886827, -0.48313374190512415, 1.3928975520201088)
e : (-0.3878522399049368, -0.8222870442374798, 0.5558893566496552)
f : (0.5866973900671675, -0.6610797182674129, 0.40011639116842934)
g : (0.6514725927833244, 0.3269688605440813, 0.539988400597291)
h : (0.07713288412330754, 0.9882594544876153, 0.05746518932333067)
i : (-0.8390685739256926, 0.6381929664509831, 0.25247375893652624)
j : (-1.106796817273839, 0.4540232305165451, 1.1982026292157175)
k : (-1.2104125343710912, -0.25618032680633235, 0.5018731882638412)
l : (-0.9785125608997393, -0.874133114081433, -0.24936362859414551)
m : (0.00957989727764813, -0.9942786580834837, -0.3454799245559613)
n : (1.0044822415044306, -1.07133755533838, -0.41052799759361946)
o : (1.1706114424717522, -0.10904845910615152, -0.1951195858300112)
p : (1.0386178440224185, 0.882201618686931, -0.19610611692617375)
q : (0.3612980015775977, 1.120426797951838, -0.8921568298736757)
r : (-0.49998460866621175, 0.6550605146715445, -0.6881311264010601)
s : (-1.268047871484895, 0.0630238583402361, -0.444058551398537)
t : (-0.46915995351177886, -0.32002864172205236, -0.9077921782929101)
u : (0.5044822415044304, -0.4936383325997051, -1.0557129385579378)
v : (1.5044822415044306, -0.4936383325997051, -1.0557129385579378)
w : (1.0044822415044306, 0.3723870711847335, -1.0557129385579378)
x : (0.08003769340765304, 0.32876511068966424, -1.4345260878237884)
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'], ['e', 'd', 'a'], ['q', 'x', 'r'], ['x', 't', 'u'], ['f', 'e', 'm'], ['q', 'p', 'h'], ['b', 'g', 'a'], ['x', 't', 'r'], ['b', 'i', 'j'], ['n', 'm', 'u'], ['k', 'l', 's'], ['k', 'e', 'd'], ['k', 'd', 'j'], ['f', 'e', 'a'], ['u', 'v', 'n'], ['w', 'o', 'p'], ['b', 'c', 'j'], ['k', 'l', 'e'], ['f', 'o', 'n'], ['w', 'q', 'x'], ['w', 'v', 'u'], ['f', 'g', 'a'], ['v', 'o', 'n'], ['o', 'p', 'g'], ['d', 'c', 'a'], ['l', 't', 's'], ['l', 't', 'm'], ['q', 'r', 'h'], ['p', 'g', 'h'], ['t', 'm', 'u'], ['w', 'q', 'p'], ['b', 'g', 'h'], ['l', 'e', 'm'], ['s', 't', 'r'], ['k', 'i', 's'], ['w', 'o', 'v'], ['b', 'i', 'h'], ['d', 'c', 'j'], ['w', 'x', 'u'], ['f', 'o', 'g'], ['b', 'c', 'a'], ['f', 'm', 'n'], ['k', 'i', 'j']]
Coordinate Data:
u : [-34451302261059313672968666551 / 62500000000000000000000000000000000000000000000000000000000000, -334346951474191386337611564743 / 100000000000000000000000000000000000000000000000000000000000000, -214312238058278791165330768329 / 1000000000000000000000000000000000000000000000000000000000000000000000000000000]
a : [-376603874929242020187670847693 / 1000000000000000000000000000000, 258280318324881190259387916479 / 1000000000000000000000000000000, 55893267292871616100419077683 / 25000000000000000000000000000]
d : [-16521796852413914448572962633 / 12500000000000000000000000000, 10504590694580933795360751903 / 1000000000000000000000000000000, 979444196231218700148981269 / 400000000000000000000000000]
p : [534135602517988174116828084491 / 1000000000000000000000000000000, 8598999695541476235524686803 / 6250000000000000000000000000, 171921364326352817170331979799 / 200000000000000000000000000000]
i : [-1679438519287653793365985019 / 1250000000000000000000000000, 56591564952534408048925872953 / 50000000000000000000000000000, 65409334874723206218593888411 / 50000000000000000000000000000]
l : [-29659896048083392944902618347 / 20000000000000000000000000000, -190247390740863995723093833401 / 500000000000000000000000000000, 806349309963792236945505884587 / 1000000000000000000000000000000]
x : [-84888909619355484821194406681 / 200000000000000000000000000000, 822403443289369270274450407533 / 1000000000000000000000000000000, -23675821829115660151415167601 / 62500000000000000000000000000]
q : [-143184239926832720824729507811 / 1000000000000000000000000000000, 80703256527577157381997921943 / 50000000000000000000000000000, 163556108684262000593580783393 / 1000000000000000000000000000000]
f : [16443029712547404712489642299 / 200000000000000000000000000000, -167441385667707750989072405709 / 1000000000000000000000000000000, 72791466486318361998525930471 / 50000000000000000000000000000]
r : [-100446685017064220648607385829 / 100000000000000000000000000000, 57434942363562476981302163021 / 50000000000000000000000000000, 4594772651960970382206588121 / 12500000000000000000000000000]
s : [-35450602259786513631689110579 / 20000000000000000000000000000, 556662190939941229963105590679 / 1000000000000000000000000000000, 122330877431880157102687749477 / 200000000000000000000000000000]
m : [-247451172113391155967291714363 / 500000000000000000000000000000, -500640325483778645500800634739 / 1000000000000000000000000000000, 355116507000988214616785554243 / 500000000000000000000000000000]
v : [1, -53966559680327417387348570509 / 20000000000000000000000000000000000000000000000000000000000000, -5404983302970208339312385711 / 31250000000000000000000000000000000000000000000000000000000000000000000000000]
k : [-17148947758755215366546812531 / 10000000000000000000000000000, 1899664046346981776203720641 / 8000000000000000000000000000, 155758612682177904713923425533 / 100000000000000000000000000000]
g : [14699035127889394217076954411 / 100000000000000000000000000000, 32824287725751453768853155489 / 40000000000000000000000000000, 159570133915522873525190852727 / 100000000000000000000000000000]
b : [-166534796378599513631748864823 / 250000000000000000000000000000, 29885932268663760291717029349 / 25000000000000000000000000000, 204103576891047319258469597011 / 100000000000000000000000000000]
h : [-427349357381122870989042218071 / 1000000000000000000000000000000, 29637955741746408682755429789 / 20000000000000000000000000000, 111317812788126844131347455061 / 100000000000000000000000000000]
j : [-10070494117364182438907260139 / 6250000000000000000000000000, 189532312623250031040930801877 / 200000000000000000000000000000, 22539155677736552989403860353 / 10000000000000000000000000000]
e : [-892334481409367273787561866173 / 1000000000000000000000000000000, -328648711637774683186741899763 / 1000000000000000000000000000000, 161160229520759307976179344273 / 100000000000000000000000000000]
w : [1 / 2, 866025403784438646763723170753 / 1000000000000000000000000000000, 6051120367001416682380023553 / 15625000000000000000000000000000000000000000000000000000000000000000000000000]
c : [-886983709091378126451765137947 / 1000000000000000000000000000000, 776671829950767911835914191793 / 1000000000000000000000000000000, 292186673183727258365819403047 / 100000000000000000000000000000]
o : [133225840193464360879379091369 / 200000000000000000000000000000, 24036867093347097685838111331 / 62500000000000000000000000000, 860593352727926591320219698791 / 1000000000000000000000000000000]
t : [-243410548754052317714476283319 / 250000000000000000000000000000, 43402422719413186867854061739 / 250000000000000000000000000000, 3698019006625690269237815977 / 25000000000000000000000000000]
n : [1 / 2, -577699222738674870633783183217 / 1000000000000000000000000000000, 25807397638572732908870291493 / 40000000000000000000000000000]
Desired square lengths:
default : 1
Checking inequality 1:
d = 3
|V| = 24
|E| = 66
Success: d|V| >= |E|
Checking self-intersection:
Square collision distance = 555465689069620154646110591943247105170407500411968996720642449081402313661396628481163073935557869177781775274871999601 / 972401088585959205617419025828282310150757775849600270601186706400113813355949260000000000000000000000000000000000000000
Collision distance in [377899141323231644426731749511 / 500000000000000000000000000000, 755798282646463288853463499023 / 1000000000000000000000000000000] ~ [0.7558, 0.7558]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [50521110984823909999 / 100000000000000000000, 50521110984823910001 / 100000000000000000000] ~ [0.50521, 0.50521]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 893057711292069614584596147102615554618657370788880339143422797266931999817900583392095328384205913811771401206892407701616321615682777189242168227577048252884387320629816873499893771671569526975763910738001973712082994053626432477734346418807704207522979 / 500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000
rho in [845249175707173163563030413143 / 20000000000000000000000000000000000000000000000000000000000, 865249175707173163563030413143 / 20000000000000000000000000000000000000000000000000000000000] ~ [0.0, 0.0]
sigma_min ^ 2 / (16 * E ^ .5) in [2552382655140895145257291485718452180001 / 1299846144741753657673581370922720000000000, 2552382655140895145459375929657747820001 / 1299846144741753657673581370922560000000000] ~ [0.00196, 0.00196]
Success: rho < sigma_min ^ 2 / (16 * E ^ .5)
Checking inequality 4:
LHS NUM := sigma_min - [sigma_min ^ 2 - 16 * rho * |E| ^ .5 ] ^ .5 in [-5176090001 / 100000000000000000000, 4823910001 / 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 [-3235056250625000000 / 4062019202317980180229941784133, 3014943750625000000 / 4062019202317980180229941784133] ~ [-0.0, 0.0]
CD / |V| ^ .5 in [377899141323231644426731749511 / 2449489742783178098197284074706, 755798282646463288853463499023 / 4898979485566356196394568149411] ~ [0.15428, 0.15428]
Success: LHS < CD / |V| ^ .5
Success: existence proven