show/hide visualization coordinates
a : (-0.8204843417366992, 0.28488224259739636, -1.015279022698917)
b : (-0.9391224386499892, -0.6580503601748775, -0.7041470433237685)
c : (-1.2676202839332085, 0.09961931546928432, -0.14020925575003906)
d : (-1.4712573988344133, 0.9432365931178075, -0.6370410323984413)
e : (-0.5383987976676057, 1.2306553140039198, -0.854216788672704)
f : (0.13195493558325033, 0.49130169333877904, -0.7911129383465373)
g : (-0.10704792957039855, -0.39330435205297765, -1.1915499182880809)
h : (-0.04991013386235277, -0.9955530171435167, -0.3952887691050446)
i : (-0.6969971677192164, -0.6145894423970577, 0.26512407550862993)
j : (-0.8758158093833888, 0.22950326735424975, 0.7706252038338547)
k : (-0.7684041755420266, 0.939129156141618, 0.07428201338946844)
l : (0.1588766836285867, 1.2477532181264122, -0.13761748302289978)
m : (0.878883953333061, 0.5538382775739793, -0.12915658172210187)
n : (0.6689386982075862, -0.32139864964556786, -0.5649126041493134)
o : (0.8618742995629398, -1.128338285187358, -0.00667942856644721)
p : (0.05411282595542766, -1.1953750175572238, 0.5790060486895554)
q : (-0.0017275321186888126, -0.24361906999408778, 0.8807384975384517)
r : (-0.018867845971758723, 0.740818574890998, 0.7058421483080461)
s : (0.8392903629396445, 1.242137257223833, 0.5951892350068475)
t : (0.8547063975359781, 0.2700820862295682, 0.8294350256213971)
u : (1.3573453358144287, -0.27565473953199093, 0.15896846065785664)
v : (0.8734629565010966, -0.7265719574681306, 0.908989464069628)
w : (0.8762074059277476, -1.7205021049150548, 0.7990106934205602)
show/hide computer existence proof
(see shape-existence, preprint)
Attempting to prove existence
Starting realization:
Abstract data:
mode: maximal_simplices
data: [['l', 's', 'm'], ['t', 'u', 'v'], ['t', 'r', 's'], ['t', 's', 'm'], ['l', 'f', 'm'], ['o', 'v', 'w'], ['p', 'v', 'q'], ['t', 'u', 'm'], ['j', 'i', 'c'], ['o', 'u', 'n'], ['a', 'f', 'e'], ['e', 'd', 'k'], ['h', 'i', 'b'], ['g', 'a', 'f'], ['g', 'h', 'n'], ['h', 'o', 'p'], ['j', 'k', 'c'], ['l', 'r', 'k'], ['q', 'v', 't'], ['o', 'u', 'v'], ['n', 'f', 'm'], ['p', 'v', 'w'], ['i', 'b', 'c'], ['d', 'k', 'c'], ['l', 'f', 'e'], ['a', 'b', 'c'], ['g', 'a', 'b'], ['a', 'd', 'c'], ['p', 'i', 'q'], ['l', 'r', 's'], ['u', 'n', 'm'], ['a', 'd', 'e'], ['g', 'b', 'h'], ['q', 'i', 'j'], ['h', 'p', 'i'], ['l', 'k', 'e'], ['q', 'r', 't'], ['j', 'r', 'k'], ['h', 'o', 'n'], ['j', 'r', 'q'], ['g', 'n', 'f'], ['o', 'p', 'w']]
Coordinate Data:
s : [-5593958109936087601 / 20000000000000000000, -14958430655371589917 / 20000000000000000000, -5552890204467781229 / 50000000000000000000]
b : [74935744804641472561 / 50000000000000000000, 115226608463013093849 / 100000000000000000000, 118827847424126040417 / 100000000000000000000]
j : [71770413341311448447 / 50000000000000000000, 26471245710100366647 / 100000000000000000000, -7162344322909070169 / 25000000000000000000]
m : [-31929149589022085693 / 100000000000000000000, -5962255311872584299 / 100000000000000000000, 61328801263959374299 / 100000000000000000000]
k : [33199915824621667331 / 25000000000000000000, -44491343168636459443 / 100000000000000000000, 40984941752802343823 / 100000000000000000000]
q : [2245279958246115959 / 4000000000000000000, 9222934930616765447 / 12500000000000000000, -4957588332761997207 / 12500000000000000000]
u : [-3988764391857943419 / 5000000000000000000, 19246761599681108757 / 25000000000000000000, 1625814851298176189 / 5000000000000000000]
c : [182721274137604856979 / 100000000000000000000, 7891928179719382063 / 20000000000000000000, 62434068666753092727 / 100000000000000000000]
g : [1666600967533096833 / 2500000000000000000, 11094000956352887781 / 12500000000000000000, 167568134920557266069 / 100000000000000000000]
w : [-31661494848490751493 / 100000000000000000000, 27683972867128852733 / 12500000000000000000, -7871981562576707681 / 25000000000000000000]
i : [125658962516205653397 / 100000000000000000000, 110880516685231107857 / 100000000000000000000, 21900735540886199761 / 100000000000000000000]
f : [42763752185958978941 / 100000000000000000000, 145701555823719113 / 50000000000000000000, 25504887385280583747 / 20000000000000000000]
t : [-590227880186275853 / 2000000000000000000, 11206681911284261403 / 50000000000000000000, -17265179735195261473 / 50000000000000000000]
p : [50547963148741246363 / 100000000000000000000, 84479537100623856173 / 50000000000000000000, -9487461777206354669 / 100000000000000000000]
a : [6900383995897696399 / 5000000000000000000, 4186669637157140633 / 20000000000000000000, 149941045361640897499 / 100000000000000000000]
l : [40071577381425346551 / 100000000000000000000, -37676874683557938663 / 50000000000000000000, 62174891394039172121 / 100000000000000000000]
r : [14461507585364970747 / 25000000000000000000, -12330142521787227873 / 50000000000000000000, -4434214347811084573 / 20000000000000000000]
o : [-30228184212009960879 / 100000000000000000000, 10140962560266321023 / 6250000000000000000, 24540542974196953989 / 50000000000000000000]
e : [54899562755522291661 / 50000000000000000000, -36821979477433320323 / 50000000000000000000, 133834821959019581273 / 100000000000000000000]
n : [-5467312038237305097 / 50000000000000000000, 81561437410082128681 / 100000000000000000000, 20980880701336105431 / 20000000000000000000]
v : [-31387049905825647711 / 100000000000000000000, 122078768192338411121 / 100000000000000000000, -5310725414401701397 / 12500000000000000000]
h : [60950259130519288713 / 100000000000000000000, 148976874159877004527 / 100000000000000000000, 21985505000563412293 / 25000000000000000000]
d : [40616997125545070549 / 20000000000000000000, -1403190214570481613 / 3125000000000000000, 11211724633159332541 / 10000000000000000000]
Desired square lengths:
default : 1
Checking inequality 1:
d = 3
|V| = 23
|E| = 63
Success: d|V| >= |E|
Checking self-intersection:
Square collision distance = 124999999999999999993009859740009694947168292006938876035436496758761723569672845423066313186269275062710906221512961361 / 249999999999999999992284647767989014174205132280571658274138253742107796563384750000000000000000000000000000000000000000
Collision distance in [11048543456039805068624756493 / 15625000000000000000000000000, 707106781186547524391984415553 / 1000000000000000000000000000000] ~ [0.70711, 0.70711]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [4927 / 10000, 4929 / 10000] ~ [0.4927, 0.4929]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 2313600536235819411371303951047632978261543 / 50000000000000000000000000000000000000000000000000000000000000000000000000000000
rho in [43021859896901894972321325723 / 200000000000000000000000000000000000000000000000, 43021859897101894972321325723 / 200000000000000000000000000000000000000000000000] ~ [0.0, 0.0]
sigma_min ^ 2 / (16 * E ^ .5) in [583541562500000000000000000 / 305278997430529683519417202343, 5061466875000000000000000000 / 2645751311064590590501615753639] ~ [0.00191, 0.00191]
Success: rho < sigma_min ^ 2 / (16 * E ^ .5)
Checking inequality 4:
LHS NUM := sigma_min - [sigma_min ^ 2 - 16 * rho * |E| ^ .5 ] ^ .5 in [-1599999999999778307696211 / 8000000000000000000000000000, 20000000000002772278682213 / 100000000000000000000000000000] ~ [-0.0002, 0.0002]
LHS DEN := 8 * |E| ^ .5 in [7937253933193771771504847260917 / 125000000000000000000000000000, 3968626966596885885752423630459 / 62500000000000000000000000000] ~ [63.49803, 63.49803]
LHS := (LHS NUM) / (LHS DEN) in [-66666666666657429487342125 / 21166010488516724724012926029112, 100000000000013861393411065 / 31749015732775087086019389043668] ~ [-0.0, 0.0]
CD / |V| ^ .5 in [707106781186547524391984415552 / 4795831523312719541597438064163, 707106781186547524391984415553 / 4795831523312719541597438064162] ~ [0.14744, 0.14744]
Success: LHS < CD / |V| ^ .5
Success: existence proven