show/hide visualization coordinates
a : (0.20102659212553425, 0.7421191952509493, -0.3576425726480319)
b : (0.5177104099708514, -0.10854224962995751, -0.7772691515345964)
c : (-0.03819978215364184, 0.5330143092093909, -1.305822876431435)
d : (-0.7375626402486212, 0.8727889469600797, -0.6769788669516514)
e : (-0.520823607509279, 0.9756397506178007, 0.29381766367367745)
f : (0.4328581095150025, 0.9470772265733349, 0.5932761162740803)
g : (0.7423566303876754, 0.09252512115569905, 0.1762013451551434)
h : (1.050388915449385, -0.7627840712193619, -0.24040674021812736)
i : (0.25415324379446513, -1.07302763377214, -0.7597887644342132)
j : (-0.3799729307223111, -0.3878279111967207, -1.1180977581467455)
k : (-1.0012727931293863, 0.31521279940004815, -1.4641038855730375)
l : (-1.1167929062054194, -0.041896638922853224, -0.5372123317569493)
m : (-1.4471754885160761, 0.7256496286887243, 0.012078189170982634)
n : (-0.846891335364169, 0.039060440071591485, 0.42226622111336526)
o : (-0.2705643283240259, 0.467695927770834, 1.1180526823505637)
p : (0.40469692682190617, 1.0353727465373908, 1.5889722792392706)
q : (0.682702194444939, 0.17030968255568668, 1.1713852026810607)
r : (0.9608259519750328, -0.6944392175547285, 0.7532267216536292)
s : (1.236222604444912, -1.5597193412372239, 0.3343627922345517)
t : (0.29886899360536734, -1.228271754797806, 0.22707483536355882)
u : (-0.42920780218335886, -0.660682292395744, -0.1573030797202295)
v : (0.006653041821216177, -0.39927466406499396, 0.7039119785051314)
show/hide computer existence proof
(see shape-existence, preprint)
Attempting to prove existence
Starting realization:
Abstract data:
mode: maximal_simplices
data: [['n', 'u', 'v'], ['j', 'l', 'k'], ['c', 'k', 'd'], ['j', 'i', 'b'], ['c', 'j', 'k'], ['i', 'b', 'h'], ['r', 's', 'h'], ['f', 'a', 'e'], ['b', 'g', 'a'], ['o', 'f', 'e'], ['c', 'a', 'd'], ['n', 'o', 'v'], ['k', 'l', 'd'], ['q', 'o', 'v'], ['r', 's', 't'], ['r', 'g', 'h'], ['f', 'g', 'a'], ['t', 'i', 'h'], ['m', 'n', 'e'], ['c', 'j', 'b'], ['t', 'u', 'v'], ['r', 'q', 'v'], ['l', 'n', 'u'], ['p', 'q', 'o'], ['o', 'n', 'e'], ['f', 'p', 'q'], ['m', 'l', 'd'], ['t', 's', 'h'], ['j', 'l', 'u'], ['g', 'b', 'h'], ['t', 'i', 'u'], ['c', 'b', 'a'], ['a', 'e', 'd'], ['f', 'p', 'o'], ['r', 'q', 'g'], ['j', 'i', 'u'], ['m', 'e', 'd'], ['m', 'l', 'n'], ['r', 't', 'v'], ['f', 'q', 'g']]
Coordinate Data:
m : [39389522890373751959 / 20000000000000000000, -17031631570647818437 / 50000000000000000000, 24964133345564147503 / 50000000000000000000]
k : [152357344913199809139 / 100000000000000000000, 6980419787571977093 / 100000000000000000000, 49386618541382577139 / 25000000000000000000]
i : [837960663150457849 / 3125000000000000000, 36451115776197700279 / 25000000000000000000, 25422992410329576269 / 20000000000000000000]
s : [-71392194844230035897 / 100000000000000000000, 24309204231412397461 / 12500000000000000000, 3539961276954276959 / 20000000000000000000]
r : [-548156619965526461 / 1250000000000000000, 13493202685381204569 / 12500000000000000000, -24186586557136371829 / 100000000000000000000]
l : [1311274849766424667 / 800000000000000000, 21345681809931057733 / 50000000000000000000, 6553582423995092449 / 6250000000000000000]
n : [136919199136678065099 / 100000000000000000000, 17297827860208823313 / 50000000000000000000, 8909463496890031557 / 100000000000000000000]
u : [1903016916371940993 / 2000000000000000000, 4182797158686048277 / 4000000000000000000, 2674655743209980273 / 4000000000000000000]
c : [56050043815625346209 / 100000000000000000000, -1479973119336228693 / 10000000000000000000, 90859186625685024181 / 50000000000000000000]
p : [2352074583614109687 / 20000000000000000000, -32517787463081137741 / 50000000000000000000, -107761142315700513183 / 100000000000000000000]
f : [4472127324380461037 / 50000000000000000000, -56206022929756688809 / 100000000000000000000, -1638305203836293947 / 20000000000000000000]
e : [52156213175594533583 / 50000000000000000000, -59062275334203277159 / 100000000000000000000, 4350863848171761291 / 20000000000000000000]
o : [3171459937306550261 / 4000000000000000000, -8267893049506605757 / 100000000000000000000, -7583647828353725889 / 12500000000000000000]
t : [22343166239724430451 / 100000000000000000000, 161328875207357386279 / 100000000000000000000, 5685720414374135081 / 20000000000000000000]
b : [229512301588015067 / 50000000000000000000, 49355924690572542661 / 100000000000000000000, 128863000761686189347 / 100000000000000000000]
h : [-13202206486169337753 / 25000000000000000000, 114780106849512987059 / 100000000000000000000, 75176759630039292371 / 100000000000000000000]
q : [-4010038461058182089 / 25000000000000000000, 21470731472008124747 / 100000000000000000000, -66002434659879527963 / 100000000000000000000]
g : [-11002798719253186653 / 50000000000000000000, 29249187612006887837 / 100000000000000000000, 33515951092712214323 / 100000000000000000000]
j : [5639209917030767041 / 6250000000000000000, 77284490847248864681 / 100000000000000000000, 81472930711450548921 / 50000000000000000000]
a : [16063703193853869259 / 50000000000000000000, -8927554949379533159 / 25000000000000000000, 43450171436514873747 / 50000000000000000000]
v : [51564761418139544699 / 100000000000000000000, 4901822883379762149 / 6250000000000000000, -4813778060571647729 / 25000000000000000000]
d : [25197265925024655519 / 20000000000000000000, -48777194968431177231 / 100000000000000000000, 118833972303391704867 / 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 = 4629629629629629629121309506463581114012364461481215254286757143793867342390912107919734294800565390907305516936476723 / 9259259259259259258932815833578945288956108274669903051011198100011315222667750000000000000000000000000000000000000000
Collision distance in [176776695296636881093622512021 / 250000000000000000000000000000, 141421356237309504874898009617 / 200000000000000000000000000000] ~ [0.70711, 0.70711]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [3737 / 10000, 3739 / 10000] ~ [0.3737, 0.3739]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 1449041831175463570064453173725296221220181 / 25000000000000000000000000000000000000000000000000000000000000000000000000000000
rho in [601880767090846567546043712173 / 2500000000000000000000000000000000000000000000000, 601880767093346567546043712173 / 2500000000000000000000000000000000000000000000000] ~ [0.0, 0.0]
sigma_min ^ 2 / (16 * E ^ .5) in [1745646125000000000000000000 / 1549193338482966754071706159913, 2184393906250000000000000000 / 1936491673103708442589632699891] ~ [0.00113, 0.00113]
Success: rho < sigma_min ^ 2 / (16 * E ^ .5)
Checking inequality 4:
LHS NUM := sigma_min - [sigma_min ^ 2 - 16 * rho * |E| ^ .5 ] ^ .5 in [-39999999999992019858358379 / 200000000000000000000000000000, 200000000000039922062614591 / 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 [-199999999999960099291791895 / 61967733539318670162868246396512, 200000000000039922062614591 / 61967733539318670162868246396512] ~ [-0.0, 0.0]
CD / |V| ^ .5 in [707106781186547524374490048084 / 4690415759823429554565630113545, 707106781186547524374490048085 / 4690415759823429554565630113544] ~ [0.15076, 0.15076]
Success: LHS < CD / |V| ^ .5
Success: existence proven