Upper bounds for Jung constants of $\ell_1^d$

Resumo Técnico: Limites Superiores para as Constantes de Jung de $\ell^d_1$

Enunciado do Problema
O artigo aborda a determinação da constante de Jung $J(\ell^d_1)$ para o espaço real de dimensão $d$ equipado com a norma $\ell_1$ (distância de Manhattan). Para um conjunto limitado não vazio $A \subset \mathbb{R}^d$, a constante de Jung é definida como o supremo da razão entre o raio de Chebyshev ($rad\, A$) e o diâmetro ($diam\, A$) sobre todos os tais conjuntos. Especificamente, o autor busca estabelecer limites superiores apertados para $J(\ell^d_1)$ quando a dimensão $d$ assume a forma $4k+1$ para inteiros $k \ge 1$.

Previamente a este trabalho, embora existissem limites clássicos (por exemplo, $J(\ell^d_1) \le d/(d+1)$ e $J(\ell^{2m}_1) \le (2m-1)/(2m)$), o valor exato para a dimensão $d=5$ (onde $k=1$) constava como desconhecido em um levantamento de 2019 por Alimov e Tsar'kov. Além disso, a conjectura de Ivanov postulava que, se uma matriz de Hadamard de ordem $h=4k$ existe, então $J(\ell^h_1) = J(\ell^{h+1}_1) = J(\ell^{h+2}_1) = (h-1)/h$.

Metodologia
A estratégia de prova combina técnicas de redução geométrica com estimativas combinatórias sobre métricas de corte (cut metrics):

1. Redução de Contato e Limites de Dimensão:
   O autor utiliza o Lema 2.1 para reduzir o problema a um conjunto finito de "pontos de contato" $y_i$ e sinais associados $\sigma_i$ que definem a bola envolvente mínima. Se o raio $R$ exceder um limiar específico, o Lema 2.2 estabelece que o número de pontos de contato deve ser exatamente $2p$ (onde $d=2p-1$) e que os sinais devem somar zero. Isso leva a uma desigualdade envolvendo a soma das distâncias de um ponto arbitrário $z$ a esses pontos de contato.

2. Estimativas de Forma Quadrática para Cortes:
   A principal inovação técnica reside na tradução das restrições de distância geométrica em um problema de somas ponderadas de semimétricas de corte.

   • Caso Geral ($k \ge 2$): Para dimensões $d = 4k+1$ (onde $p = 2k+1 \ge 5$), o autor emprega o Lema 3.1. Este lema fornece um limite superior $B_p$ para a soma ponderada de tamanhos de corte ($\Phi$) dadas as restrições de distâncias pareadas e o número de cortes "equilibrados". A prova do Lema 3.1 baseia-se em uma análise de forma quadrática envolvendo uma matriz de distâncias e construções vetoriais específicas para derivar o limite.
   • Caso de Cinco Dimensões ($k=1$): O limite geral de forma quadrática é insuficiente para $p=3$ (dimensão 5). A Seção 5 introduz uma "estimativa de capacidade de seis rótulos" especializada (Proposição 5.1). Isso envolve uma análise combinatória de cortes em um conjunto de seis rótulos, classificando cortes equilibrados por suas representações de grafos (arestas de $K_5$) e construindo certificados de peso explícitos para provar o limite $\Phi \le 9/2$.

3. Lacunas de Coordenadas e Conjuntos Arbitrários:
   O Lema 4.1 faz a ponte entre conjuntos de contato finitos e conjuntos limitados arbitrários utilizando medianas por coordenada para construir métricas de corte que preservam as distâncias pareadas. O Lema 4.2 estende os resultados finitos para conjuntos limitados não vazios arbitrários via um argumento de compacidade.

4. Nitidez e Matrizes de Hadamard:
   Para provar que os limites são nítidos, o artigo constrói conjuntos de pontos específicos. Para o limite inferior, utiliza propriedades de matrizes de Hadamard (Proposição 7.1). Para o caso específico de $d=5$, um conjunto de quatro pontos é construído explicitamente para demonstrar que o raio não pode ser menor que $3/4$ do seu diâmetro.

Principais Contribuições e Resultados

• Teorema Principal (Teorema 1.1): Para todo inteiro $k \ge 1$, a constante de Jung para a dimensão $4k+1$ satisfaz o limite superior incondicional:
  $$J(\ell^{4k+1}_1) \le \frac{4k-1}{4k}$$
  Isso estabelece que todo conjunto limitado não vazio em $\mathbb{R}^{4k+1}$ possui uma bola envolvente ambiente de raio no máximo $\frac{4k-1}{4k}$ vezes o seu diâmetro.

• Resolução do Caso de Cinco Dimensões: O artigo prova que $J(\ell^5_1) = 3/4$. Isso resolve a questão aberta mencionada no levantamento de Alimov e Tsar'kov, estabelecendo tanto o limite superior quanto um limite inferior correspondente para esta dimensão específica.

• Confirmação da Conjectura de Ivanov (Condicional): O Corolário 1.2 afirma que se uma matriz de Hadamard de ordem $4k$ existir, então o valor exato é determinado para três dimensões consecutivas:
  $$J(\ell^{4k-1}_1) = J(\ell^{4k}_1) = J(\ell^{4k+1}_1) = \frac{4k-1}{4k}$$
  Isso confirma o valor conjecturado para a dimensão $h+1$ (onde $h=4k$) e unifica os valores para as dimensões $h-1, h,$ e $h+1$ sob a existência de matrizes de Hadamard. Sem essa suposição, o artigo fornece o limite superior para $4k+1$ e o limite inferior via exemplos de Hadamard, mas não reivindica o valor exato para todas as dimensões $4k+1$ de forma incondicional.

• Formalização: O limite superior para cada $k \ge 1$ e o resultado de nitidez para a dimensão 5 foram formalmente verificados usando o provador de teoremas Lean. O código está disponível em um repositório público, com dependências restritas a axiomas clássicos padrão.

Significância e Alegações
O artigo afirma fornecer um limite superior nítido para a constante de Jung em dimensões da forma $4k+1$ incondicionalmente, e o valor exato para estas dimensões (assim como para $4k-1$ e $4k$) sob a suposição da existência de matrizes de Hadamard. Ele especificamente resolve o caso de longa data para a dimensão 5. O trabalho refina a compreensão de como a geometria dos espaços $\ell_1$ se comporta em altas dimensões, particularmente em relação à relação entre diâmetro e raio envolvente.

O autor observa que o limite derivado no Lema 3.1 é específico para a "configuração de contato" forçada por um raio que excede o limiar e não é um limite superior incondicional para a constante de Jung em si. A significância do resultado é enquadrada no contexto de problemas clássicos de geometria métrica, especificamente o interplay entre estruturas combinatórias (matrizes de Hadamard, métricas de corte) e constantes geométricas. A formalização em Lean é destacada como uma verificação da correção rigorosa das complexas estimativas combinatórias envolvidas.