show/hide visualization coordinates
a : (0.4764294138102372, -0.13747823659024316, -1.0259859101449438)
b : (0.9473128656155527, -0.27210577143226966, -0.15412342002493085)
c : (0.6052543537753908, -1.060983540301282, -0.664679822650481)
d : (0.19454817013838727, -0.9298661019063992, -1.5669706006544968)
e : (-0.44342164014562924, -0.5147056878211751, -0.9184057606093697)
f : (-0.2915718921790956, 0.46872278994951494, -0.8193598967274106)
g : (0.6017903793539628, 0.6331924864312981, -0.4012049365266689)
h : (0.9981282840948376, 0.47918355098834736, 0.503890369542997)
i : (0.6313312642375157, -0.4076584360233661, 0.7849085830041592)
j : (0.9753361862476198, -1.1836200395380816, 0.25618918341332364)
k : (0.24141436911794506, -1.7788070876841293, -0.07108920582169842)
l : (-0.2664583625711111, -1.4983761700127443, -0.8855975169031022)
m : (-0.3564241406814511, -0.9779392849468393, -0.03644993995790524)
n : (-0.7214386561603718, -0.04790482692515474, -0.07888000455837596)
o : (-0.8163416401661583, 0.9469215455956392, -0.11512793089790285)
p : (-0.03125864042022275, 1.3940699076086291, -0.5437338406320357)
q : (0.30795772640523583, 1.1912313962118366, 0.3748459298680931)
r : (0.13133126423751573, 0.43117090049198065, 1.00023471750999)
s : (-0.36866873576248427, -0.4076584360233661, 0.7849085830041592)
t : (0.13133126423751573, -1.2736838398078048, 0.7849085830041592)
u : (-0.8398387071303033, 0.47417607464981487, 0.7657577640388995)
v : (-1.2674304814780597, 1.3729650421467146, 0.6690951217410896)
w : (-0.46902685749616757, 1.8090182048840309, 0.25387314197681365)
x : (-0.3702857870806604, 1.290135560055049, 1.1029968090056397)
show/hide computer existence proof
(see shape-existence, preprint)
Attempting to prove existence
Starting realization:
Abstract data:
mode: maximal_simplices
data: [['h', 'q', 'r'], ['e', 'm', 'n'], ['i', 'j', 't'], ['x', 'q', 'w'], ['d', 'a', 'c'], ['s', 'm', 'n'], ['i', 's', 'r'], ['b', 'a', 'c'], ['p', 'q', 'g'], ['v', 'o', 'w'], ['i', 's', 't'], ['w', 'v', 'x'], ['i', 'b', 'j'], ['k', 'm', 'l'], ['s', 'n', 'u'], ['b', 'a', 'g'], ['n', 'o', 'u'], ['l', 'd', 'c'], ['e', 'm', 'l'], ['q', 'w', 'p'], ['e', 'f', 'a'], ['p', 'o', 'w'], ['k', 'j', 't'], ['s', 'u', 'r'], ['h', 'i', 'b'], ['e', 'f', 'n'], ['v', 'x', 'u'], ['v', 'o', 'u'], ['s', 'm', 't'], ['e', 'd', 'a'], ['k', 'j', 'c'], ['f', 'o', 'p'], ['e', 'l', 'd'], ['f', 'p', 'g'], ['u', 'x', 'r'], ['h', 'b', 'g'], ['n', 'f', 'o'], ['h', 'i', 'r'], ['q', 'x', 'r'], ['b', 'j', 'c'], ['k', 'l', 'c'], ['k', 'm', 't'], ['h', 'q', 'g'], ['f', 'a', 'g']]
Coordinate Data:
i : [-163002788180508144411311902221 / 1000000000000000000000000000000000000000000000000000000, -518028153182160583266743241609 / 10000000000000000000000000000000000000000000000000000000, 184705610267580377161070105333 / 50000000000000000000000000000000000000000000000000000000000000000000000]
x : [12520213141477201396538446379 / 12500000000000000000000000000, -4244484990196037936686934251 / 2500000000000000000000000000, -159044113000740205396384369473 / 500000000000000000000000000000]
o : [14476729044036739450308428533 / 10000000000000000000000000000, -135457998161900537968548796043 / 100000000000000000000000000000, 900036513902062084988070688593 / 1000000000000000000000000000000]
g : [7385221220888211131090614381 / 250000000000000000000000000000, -1626329566335412757718068467 / 1562500000000000000000000000, 5930567597654140754903610353 / 5000000000000000000000000000]
w : [11003581217336833814592383219 / 10000000000000000000000000000, -221667664090739708696732272947 / 100000000000000000000000000000, 132758860256836379448004634489 / 250000000000000000000000000000]
h : [-91699254964330458213808972703 / 250000000000000000000000000000, -886841987011713469919523257783 / 1000000000000000000000000000000, 439090958533065843677878257 / 1562500000000000000000000000]
p : [132517980931547699149427455871 / 200000000000000000000000000000, -9008641718159976952788265387 / 5000000000000000000000000000, 66432121181809741766190115549 / 50000000000000000000000000000]
s : [100000000000000000000000031627 / 100000000000000000000000000000, -79317145875340219650010787497 / 250000000000000000000000000000000000000000000000000000, -69311864996412204356431258779 / 5000000000000000000000000000000000000000000000000000000000000000000000]
u : [3677924928419547507610021937 / 2500000000000000000000000000, -220458627668295234744633538977 / 250000000000000000000000000000, 4787704741314943791642253233 / 250000000000000000000000000000]
j : [-172002461005052007118300394533 / 500000000000000000000000000000, 387980801757357767088853081031 / 500000000000000000000000000000, 264359699795417788400513066541 / 500000000000000000000000000000]
t : [499999999999999999999999846733 / 1000000000000000000000000000000, 54126587736527415422732721239 / 62500000000000000000000000000, 101682607939352007879712745047 / 10000000000000000000000000000000000000000000000000000000000000000000000]
k : [38991689511957069125820802009 / 100000000000000000000000000000, 68557432583038162948344883111 / 50000000000000000000000000000, 855997788825857612714386769903 / 1000000000000000000000000000000]
c : [1303845523106242519856114207 / 50000000000000000000000000000, 81665638034739488450029844497 / 125000000000000000000000000000, 18119855070683003435259078263 / 12500000000000000000000000000]
v : [189876174571557550654430004221 / 100000000000000000000000000000, -17806234781700806019134091493 / 10000000000000000000000000000, 57906730631534778203397353987 / 500000000000000000000000000000]
l : [224447406702156710535414833179 / 250000000000000000000000000000, 21814354679787564117796798133 / 20000000000000000000000000000, 10440663124420383730716007433 / 6250000000000000000000000000]
m : [246938851229741701556799645009 / 250000000000000000000000000000, 114056169784694656516630084797 / 200000000000000000000000000000, 821358522962064465280417085919 / 1000000000000000000000000000000]
d : [436783094099128459025461005733 / 1000000000000000000000000000000, 261103832941516524717422700997 / 500000000000000000000000000000, 47037583673173119780407036133 / 20000000000000000000000000000]
a : [30980370085455708386778037433 / 200000000000000000000000000000, -270180199433122919581355891921 / 1000000000000000000000000000000, 45272362328727579447640160963 / 25000000000000000000000000000]
r : [499999999999999999999999843131 / 1000000000000000000000000000000, -167765867303069353158897008427 / 200000000000000000000000000000, -215326134505830789578664316209 / 1000000000000000000000000000000]
q : [80843384458069969024268050237 / 250000000000000000000000000000, -15988898322352028072707673847 / 10000000000000000000000000000, 410062653136066119290031978357 / 1000000000000000000000000000000]
e : [107475290438314499215283159683 / 100000000000000000000000000000, 21409450359561807117667753383 / 200000000000000000000000000000, 21291429295169111285896713973 / 12500000000000000000000000000]
b : [-315981601378037051981241866559 / 1000000000000000000000000000000, -13555266459109644792049418761 / 100000000000000000000000000000, 939032003029090058216589336567 / 1000000000000000000000000000000]
n : [4227406001243398383808624607 / 3125000000000000000000000000, -35975360909821134250710472161 / 100000000000000000000000000000, 53986786722658447743761941819 / 62500000000000000000000000000]
f : [184580631283322274451027405433 / 200000000000000000000000000000, -876381225972881045018247285853 / 1000000000000000000000000000000, 8021342398657849655556799821 / 5000000000000000000000000000]
Desired square lengths:
default : 1
Checking inequality 1:
d = 3
|V| = 24
|E| = 66
Success: d|V| >= |E|
Checking self-intersection:
Square collision distance = 554965296531640444091206171912208546487012407355588120235399546887138784087266039264712905853329695455676097540783150969 / 973366631388890802334571454343797330287657862108130755580333520916746328625399940000000000000000000000000000000000000000
Collision distance in [151016597786142376764019135269 / 200000000000000000000000000000, 377541494465355941910047838173 / 500000000000000000000000000000] ~ [0.75508, 0.75508]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [40598851889747616999 / 100000000000000000000, 40598851889747617001 / 100000000000000000000] ~ [0.40599, 0.40599]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 968237838435425391719810095935418175785904788401584961967489614689634332585092818580734519817212204464360084911143063765794304512237019643376564630468691314157932137376803536865041031019458859714002940496960591288956784669628341953349961241 / 6250000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000
rho in [3935963086077765321744040626109 / 10000000000000000000000000000000000000000000000000000, 3935963096077765321744040626109 / 10000000000000000000000000000000000000000000000000000] ~ [0.0, 0.0]
sigma_min ^ 2 / (16 * E ^ .5) in [1648266774765663651945758253399193766001 / 1299846144741753657673581370922720000000000, 1648266774765663652108153660958184234001 / 1299846144741753657673581370922560000000000] ~ [0.00127, 0.00127]
Success: rho < sigma_min ^ 2 / (16 * E ^ .5)
Checking inequality 4:
LHS NUM := sigma_min - [sigma_min ^ 2 - 16 * rho * |E| ^ .5 ] ^ .5 in [-252383001 / 100000000000000000000, 9747617001 / 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 [-12133798125000000 / 312463015562921552325380137241, 6092260625625000000 / 4062019202317980180229941784133] ~ [-0.0, 0.0]
CD / |V| ^ .5 in [251694329643570627940031892115 / 1632993161855452065464856049804, 755082988930711883820095676346 / 4898979485566356196394568149411] ~ [0.15413, 0.15413]
Success: LHS < CD / |V| ^ .5
Success: existence proven