show/hide visualization coordinates
a : (0.3772853805945053, 0.26034099821012346, -0.6536695591787448)
b : (-0.5928592616535951, 0.01859519786203051, -0.6342185661098728)
c : (-0.31070036682110025, 0.9664702371858052, -0.48616699437266464)
d : (0.5582597369412625, 0.9877336102562675, 0.008258133462652917)
e : (1.203016631527055, 0.22974418991501394, -0.09043627131702858)
f : (0.9580841635975408, -0.553667128585545, -0.6616409563461109)
g : (0.061071985526722494, -0.5751218658796797, -1.1031257767423353)
h : (-0.6948820359603723, -0.9749584806522322, -0.5847975034591636)
i : (-1.2577453497453073, -0.38511525774762206, -0.005772579653163468)
j : (-1.114586044786849, 0.6045487700622346, -0.014170523626673925)
k : (-0.29762833362619856, 0.8512650348144459, 0.507088704475686)
l : (0.5634125549562856, 0.9431671559003442, 1.0072512663783129)
m : (1.4261009640560474, 1.0016260185095718, 0.5049054988164097)
n : (1.137028739536385, 0.13077314051441902, 0.9024636881407069)
o : (0.695067406222448, -0.5365434803469105, 0.3029983368671041)
p : (0.25001654819440244, -1.174593101254266, -0.3253506227313663)
q : (-0.12768594813717526, -1.5548949079118832, -1.1695729631831258)
r : (-0.3023738133132434, -0.5569831316755172, 0.23449115312176638)
s : (-0.8524869227398156, 0.06822089142634125, 0.7881115070957502)
t : (-1.8192736146289237, 0.20624553200292284, 0.5730006264322658)
u : (0.14087758025992553, 0.043146577394135965, 0.9003534019295938)
show/hide computer existence proof
(see shape-existence, preprint)
Attempting to prove existence
Starting realization:
Abstract data:
mode: maximal_simplices
data: [['b', 'c', 'j'], ['s', 'k', 'u'], ['i', 't', 's'], ['c', 'k', 'd'], ['o', 'n', 'e'], ['f', 'o', 'e'], ['q', 'h', 'p'], ['o', 'n', 'u'], ['f', 'a', 'g'], ['m', 'l', 'd'], ['c', 'd', 'a'], ['i', 'b', 'j'], ['i', 'r', 's'], ['s', 'k', 'j'], ['l', 'n', 'u'], ['b', 'a', 'g'], ['t', 'j', 's'], ['o', 'r', 'u'], ['f', 'o', 'p'], ['f', 'g', 'p'], ['f', 'a', 'e'], ['o', 'r', 'p'], ['q', 'g', 'p'], ['q', 'g', 'h'], ['m', 'l', 'n'], ['m', 'n', 'e'], ['i', 'r', 'h'], ['m', 'd', 'e'], ['l', 'k', 'u'], ['s', 'r', 'u'], ['l', 'k', 'd'], ['b', 'c', 'a'], ['i', 't', 'j'], ['d', 'a', 'e'], ['b', 'g', 'h'], ['r', 'h', 'p'], ['i', 'b', 'h'], ['c', 'k', 'j']]
Coordinate Data:
n : [-12398370732251504587 / 20000000000000000000, 458375888117730861 / 1250000000000000000, -18796697576490076293 / 50000000000000000000]
f : [-1763895842694923531 / 4000000000000000000, 26278524489853718663 / 25000000000000000000, 59408534647850813359 / 50000000000000000000]
h : [3029980597210455579 / 2500000000000000000, 147243233166083596521 / 100000000000000000000, 2778318100175172269 / 2500000000000000000]
q : [2014987972065578373 / 3125000000000000000, 12827304743253044239 / 6250000000000000000, 33922053995880623511 / 20000000000000000000]
d : [-4114953401745263947 / 100000000000000000000, -1225649398119159451 / 2500000000000000000, 51827160314825240009 / 100000000000000000000]
g : [712559714682948947 / 1562500000000000000, 107259571688828338613 / 100000000000000000000, 162965551335324052761 / 100000000000000000000]
e : [-13718128572064903973 / 20000000000000000000, 13386483054679488481 / 50000000000000000000, 616966007927933911 / 1000000000000000000]
l : [-4630235203247574073 / 100000000000000000000, -22284665244587024211 / 50000000000000000000, -24036076488370378281 / 50000000000000000000]
m : [-45449538056611872761 / 50000000000000000000, -25207608375048400947 / 50000000000000000000, 2162423779449558567 / 100000000000000000000]
t : [116819190877636686863 / 50000000000000000000, 29122831900568086347 / 100000000000000000000, -580886122767005461 / 12500000000000000000]
j : [5099050774095808607 / 3125000000000000000, -267687297634077377 / 2500000000000000000, 54070026023757925517 / 100000000000000000000]
o : [-3559144065972764517 / 20000000000000000000, 103401733135551404407 / 100000000000000000000, 22353139974380118303 / 100000000000000000000]
i : [177485555266911710489 / 100000000000000000000, 44129455437811289607 / 50000000000000000000, 53230231626406873901 / 100000000000000000000]
u : [37623262266388429923 / 100000000000000000000, 567909092018084647 / 1250000000000000000, -37382366531868857389 / 100000000000000000000]
a : [436952569779076673 / 3125000000000000000, 11856642639924013609 / 50000000000000000000, 7376245598685313401 / 6250000000000000000]
b : [110996946457740492877 / 100000000000000000000, 47887865314657318031 / 100000000000000000000, 116074830272077821011 / 100000000000000000000]
k : [8147385365500084137 / 10000000000000000000, -884477959514605779 / 2500000000000000000, 1944103213521926769 / 100000000000000000000]
p : [26709365472940737327 / 100000000000000000000, 5225209225821467783 / 3125000000000000000, 42594017967113577617 / 50000000000000000000]
s : [136959712566362544263 / 100000000000000000000, 42925295958226244689 / 100000000000000000000, -26158177048484490187 / 100000000000000000000]
c : [82781056974491009423 / 100000000000000000000, -11724909654430037611 / 25000000000000000000, 25317418274589249503 / 25000000000000000000]
r : [81948401623705326907 / 100000000000000000000, 5272284913420604267 / 5000000000000000000, 14601929174456945321 / 50000000000000000000]
Desired square lengths:
default : 1
Checking inequality 1:
d = 3
|V| = 21
|E| = 57
Success: d|V| >= |E|
Checking self-intersection:
Square collision distance = 499999999999999999985436657840129621203159832117973408786462539632178433372752100844549455053127071971337648984258473689 / 999999999999999999992656653528090116767457650167542373484092905694564359059693660000000000000000000000000000000000000000
Collision distance in [14142135623730950487862855783 / 20000000000000000000000000000, 707106781186547524393142789151 / 1000000000000000000000000000000] ~ [0.70711, 0.70711]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [2963 / 10000, 593 / 2000] ~ [0.2963, 0.2965]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 2193411775304902905411901436163680711752011 / 50000000000000000000000000000000000000000000000000000000000000000000000000000000
rho in [2094474528517786919239081712669 / 10000000000000000000000000000000000000000000000000, 2094474528527786919239081712669 / 10000000000000000000000000000000000000000000000000] ~ [0.0, 0.0]
sigma_min ^ 2 / (16 * E ^ .5) in [5487105625000000000000000000 / 7549834435270749697236684806947, 2747257812500000000000000000 / 3774917217635374848618342403473] ~ [0.00073, 0.00073]
Success: rho < sigma_min ^ 2 / (16 * E ^ .5)
Checking inequality 4:
LHS NUM := sigma_min - [sigma_min ^ 2 - 16 * rho * |E| ^ .5 ] ^ .5 in [-99999999999978667202807149 / 500000000000000000000000000000, 200000000000042694393302131 / 1000000000000000000000000000000] ~ [-0.0002, 0.0002]
LHS DEN := 8 * |E| ^ .5 in [3774917217635374848618342403473 / 62500000000000000000000000000, 7549834435270749697236684806947 / 125000000000000000000000000000] ~ [60.39868, 60.39868]
LHS := (LHS NUM) / (LHS DEN) in [-99999999999978667202807149 / 30199337741082998788946739227784, 200000000000042694393302131 / 60398675482165997577893478455568] ~ [-0.0, 0.0]
CD / |V| ^ .5 in [707106781186547524393142789150 / 4582575694955840006588047193729, 707106781186547524393142789151 / 4582575694955840006588047193728] ~ [0.1543, 0.1543]
Success: LHS < CD / |V| ^ .5
Success: existence proven