show/hide visualization coordinates
a : (-0.47218564753190334, 0.9274875975074413, 0.030679510488006767)
b : (0.029549189807098364, 1.2113016201404836, 0.8478158232028783)
c : (0.39047906396787135, 1.4250786588853592, -0.059944609754937095)
d : (0.11996694742809111, 0.7620876303332009, -0.7579890860345789)
e : (-0.8317156881198555, 0.4554349158321983, -0.7742455889082273)
f : (-1.1926455622806285, 0.24165787708732273, 0.13351484404958813)
g : (-0.5255842800083219, 0.37973072490839976, 0.8656112409727008)
h : (0.35557389066282546, 0.4028719651088618, 1.3378662158130532)
i : (0.7165037648235985, 0.6166490038537374, 0.43010578285523776)
j : (1.0774336389843715, 0.830426042598613, -0.4776546501025777)
k : (0.8152120055236033, 0.2060143734605182, -1.2134194782843446)
l : (-0.10189215232982313, -0.16365797671523968, -1.0642138578691287)
m : (-0.8108552105733899, -0.48566994513460665, -0.43677487737730936)
n : (-0.7474433797662361, -0.5460148821400408, 0.5593864691381509)
o : (-0.22409978792692747, -0.40956503251991255, 1.4005124546001242)
p : (0.4247076394964979, -0.31528089080358684, 0.6454234381649674)
q : (0.7856375136572709, -0.10150385205871121, -0.2623369947928481)
r : (0.6951561969800737, -0.7646929450622459, -1.0052995498745356)
s : (-0.2251955200556352, -1.1439304200888987, -0.9097398591842057)
t : (-0.5861253942164082, -1.3577074588337743, -0.0019794262263903573)
u : (-0.026703551341472342, -1.1922470225519972, 0.8102213160410953)
v : (0.3342263228193007, -0.9784699838071216, -0.09753911691672013)
show/hide computer existence proof
(see shape-existence, preprint)
Attempting to prove existence
Starting realization:
Abstract data:
mode: maximal_simplices
data: [['n', 't', 'm'], ['j', 'i', 'c'], ['d', 'j', 'k'], ['v', 'q', 'p'], ['q', 'k', 'r'], ['n', 'f', 'm'], ['n', 'o', 'u'], ['v', 's', 'r'], ['t', 's', 'm'], ['n', 't', 'u'], ['p', 'i', 'h'], ['n', 'f', 'g'], ['v', 't', 's'], ['q', 'j', 'k'], ['b', 'i', 'h'], ['f', 'a', 'g'], ['u', 'p', 'v'], ['d', 'j', 'c'], ['b', 'g', 'h'], ['o', 'g', 'h'], ['n', 'o', 'g'], ['b', 'i', 'c'], ['q', 'j', 'i'], ['a', 'g', 'b'], ['l', 's', 'r'], ['q', 'p', 'i'], ['l', 's', 'm'], ['l', 'd', 'k'], ['d', 'e', 'a'], ['d', 'a', 'c'], ['v', 'q', 'r'], ['v', 't', 'u'], ['a', 'b', 'c'], ['o', 'p', 'h'], ['u', 'o', 'p'], ['e', 'a', 'f'], ['e', 'f', 'm'], ['l', 'e', 'm'], ['l', 'd', 'e'], ['l', 'k', 'r']]
Coordinate Data:
e : [8310414482331647371 / 6250000000000000000, 970396812555752447 / 25000000000000000000, 67508892935455280723 / 50000000000000000000]
n : [124539400881944410689 / 100000000000000000000, 104026567047446924119 / 100000000000000000000, 827290033136370311 / 50000000000000000000]
t : [21681520465392325943 / 20000000000000000000, 37039164943364055589 / 20000000000000000000, 57791169602726862839 / 100000000000000000000]
i : [-10927656788519515691 / 50000000000000000000, -191247211748920323 / 1562500000000000000, 14582648694564054237 / 100000000000000000000]
h : [3559418459759567129 / 25000000000000000000, 4568941161278330329 / 50000000000000000000, -38096697300608744279 / 50000000000000000000]
q : [-7192172115101569087 / 25000000000000000000, 29787732019656982441 / 50000000000000000000, 41913463229686319347 / 50000000000000000000]
u : [10493083607893608739 / 20000000000000000000, 33729956217728515101 / 20000000000000000000, -23428904624021697763 / 100000000000000000000]
s : [14462922982176865961 / 20000000000000000000, 2559658138161448697 / 1562500000000000000, 148567212898508405633 / 100000000000000000000]
d : [18899184081255850759 / 50000000000000000000, -26783684199877244623 / 100000000000000000000, 133392135583545721647 / 100000000000000000000]
v : [16372430623390743793 / 100000000000000000000, 147272077214155014159 / 100000000000000000000, 67347138671759845027 / 100000000000000000000]
o : [36102520849006778223 / 50000000000000000000, 2259539552135852489 / 2500000000000000000, -41229009239962291527 / 50000000000000000000]
r : [-9860278396343278061 / 50000000000000000000, 3934199166864607901 / 3125000000000000000, 158123181967541387819 / 100000000000000000000]
p : [7324298955671023561 / 100000000000000000000, 40476583956900763111 / 50000000000000000000, -868639604551113013 / 12500000000000000000]
a : [12126703457313893097 / 12500000000000000000, -2166184045865064311 / 5000000000000000000, 54525275931287158487 / 100000000000000000000]
k : [-31726137647039515427 / 100000000000000000000, 28823641487391024043 / 100000000000000000000, 44733793702130570721 / 25000000000000000000]
c : [2686789127133419071 / 25000000000000000000, -93082787055093087181 / 100000000000000000000, 7948460994447692751 / 12500000000000000000]
m : [65440291981329896299 / 50000000000000000000, 48996036673451756589 / 50000000000000000000, 101270714717818776549 / 100000000000000000000]
b : [23420071962305488097 / 50000000000000000000, -14341016636121105169 / 20000000000000000000, -5437671068040000157 / 20000000000000000000]
j : [-57948300993116331301 / 100000000000000000000, -16808762713209231007 / 50000000000000000000, 3292459124698299907 / 3125000000000000000]
l : [29992139069151560717 / 50000000000000000000, 32895438252483406491 / 50000000000000000000, 164014612767000708383 / 100000000000000000000]
f : [33811923826676731569 / 20000000000000000000, 202074328997684569 / 800000000000000000, 44241742575129018653 / 100000000000000000000]
g : [25588372726538247693 / 25000000000000000000, 11452006342602866513 / 100000000000000000000, -28967897117182246113 / 100000000000000000000]
Desired square lengths:
default : 1
Checking inequality 1:
d = 3
|V| = 22
|E| = 60
Success: d|V| >= |E|
Checking self-intersection:
Square collision distance = 561430008363862026847377639992925203105479685724242839902896025412824458997213993741228250716240293107140791386912518841 / 952785371674852501027019628769392182609765462978050235165481510206579836594756020000000000000000000000000000000000000000
Collision distance in [767627050697363486217085970033 / 1000000000000000000000000000000, 383813525348681743108542985017 / 500000000000000000000000000000] ~ [0.76763, 0.76763]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [339 / 1000, 212 / 625] ~ [0.339, 0.3392]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 2612043088548107452628369740937119165038247 / 50000000000000000000000000000000000000000000000000000000000000000000000000000000
rho in [571406498097907031124592173323 / 2500000000000000000000000000000000000000000000000, 571406498100407031124592173323 / 2500000000000000000000000000000000000000000000000] ~ [0.0, 0.0]
sigma_min ^ 2 / (16 * E ^ .5) in [1436512500000000000000000000 / 1549193338482966754071706159913, 1797760000000000000000000000 / 1936491673103708442589632699891] ~ [0.00093, 0.00093]
Success: rho < sigma_min ^ 2 / (16 * E ^ .5)
Checking inequality 4:
LHS NUM := sigma_min - [sigma_min ^ 2 - 16 * rho * |E| ^ .5 ] ^ .5 in [-49999999999989561095042227 / 250000000000000000000000000000, 200000000000041780254415247 / 1000000000000000000000000000000] ~ [-0.0002, 0.0002]
LHS DEN := 8 * |E| ^ .5 in [1936491673103708442589632699891 / 31250000000000000000000000000, 1549193338482966754071706159913 / 25000000000000000000000000000] ~ [61.96773, 61.96773]
LHS := (LHS NUM) / (LHS DEN) in [-4545454545453596463185657 / 1408357580439060685519732872648, 200000000000041780254415247 / 61967733539318670162868246396512] ~ [-0.0, 0.0]
CD / |V| ^ .5 in [767627050697363486217085970033 / 4690415759823429554565630113545, 4127027154286900463532720269 / 25217289031308761046051774804] ~ [0.16366, 0.16366]
Success: LHS < CD / |V| ^ .5
Success: existence proven