A Calculus of Apartness over Separoids: Effective Convex Representation, Stratified Conservativity, and the Complexity of Entailment

Resumen Técnico: Un Cálculo de Apartamiento sobre Separoides

Planteamiento del Problema
El artículo investiga la estructura lógica y combinatoria inducida por la disyunción de los envolventes convexos de cuerpos convexos compactos en el espacio euclidiano. Dado un conjunto finito de "sitios" $E$, donde cada sitio está asociado con un cuerpo convexo compacto no vacío, el estudio se centra en la relación binaria de apartamiento ($A \mathbin{\#} B$) entre subconjuntos disjuntos de sitios. Esta relación se cumple si los envolventes convexos de las uniones de los cuerpos correspondientes a $A$ y $B$ son disjuntos. El problema central es determinar hasta qué punto los detalles geométricos de los cuerpos (dimensión, forma, coordenadas) pueden olvidarse manteniendo las consecuencias lógicas de sus patrones de separación. Específicamente, el estudio busca axiomatizar esta relación, proporcionar una representación efectiva y clasificar la complejidad del razonamiento sobre ella.

Metodología
Los autores emplean un enfoque multicapa que combina la geometría convexa, la topología combinatoria y la teoría de la demostración:

1. Fundación Axiomática: El artículo identifica tres leyes fundamentales que satisface la relación de apartamiento de cualquier escena de cuerpos convexos: Simetría, Subsunción Bilateral (monotonicidad) y Vacuidad (el conjunto vacío es ajeno a todo). Estas leyes definen una estructura llamada separoide de apartamiento, que se muestra criptomórfica con los separoides no axiales encontrados en la literatura existente (Strausz et al.), viendo efectivamente la relación de separación desde el lado complementario de la "partición de Radon".
2. Representación Efectiva: Se desarrolla un teorema constructivo para realizar cualquier separoide de apartamiento finito utilizando politopos racionales. A diferencia de las realizaciones geométricas previas que optimizan para una dimensión mínima, esta construcción es "legible por demostración" (proof-readable). Asigna una coordenada a cada separación máxima y utiliza coordenadas racionales explícitas con una altura de bits acotada. La construcción garantiza un margen euclidiano uniforme (al menos 2) para todas las separaciones, proporcionando robustez contra perturbaciones.
3. Análisis de Estabilidad: Utilizando funciones de distancia y cuerpos paralelos exteriores, el artículo analiza la estabilidad de la realización. Demuestra que la relación de apartamiento es invariante bajo el agrandamiento por cuerpo paralelo exterior por cualquier radio $r < 1$ y que los cuerpos pueden engrosarse para convertirse en cuerpos de dimensión completa $C^{1,1}$ sin alterar la relación.
4. Cálculo Lógico y Complejidad: Se define un lenguaje formal $L_E$ con átomos que representan aserciones de separación. El artículo introduce un cálculo de secuentes positivo ($SC_0$) y un cálculo booleano ($ACE$). Analiza los problemas de decisión de satisfacibilidad, validez y implicación, estableciendo su complejidad computacional.
5. Estratificación: El artículo introduce una disciplina de estratificación para probar un teorema de conservatividad, mostrando que el estrato booleano (razonamiento compuesto) es inerte con respecto al estrato atómico (hechos positivos).

Contribuciones Clave y Resultados

• Axiomatización Criptomórfica: El artículo establece que las tres leyes (Simetría, Subsunción Bilateral, Vacuidad) axiomatizan completamente la relación de apartamiento de los cuerpos convexos. Esto confirma que el "olvido" de los detalles geométricos no tiene coste alguno respecto a la relación de consecuencia lógica, siempre que la dimensión ambiente sea suficientemente alta.
• Representación Racional Efectiva (Teorema 4.3): Todo separoide de apartamiento finito es realizado por una escena de politopos racionales. La construcción es sensible a la salida (output-sensitive):
  • Las coordenadas están indexadas por separaciones máximas.
  • Todas las coordenadas son números racionales con tamaños de numerador y denominador explícitamente acotados ($O(\log n)$ bits).
  • La realización garantiza un margen uniforme de al menos 2 para cada separación bilateral.
  • La construcción permite la enumeración de separaciones máximas y particiones de Radon mínimas a partir de varios formatos de entrada (tabla completa, generadores o oráculos de membresía) con un coste de salida exponencial pero sin un crecimiento aritmético oculto.
• Estabilidad y Robustez (Teorema 4.13): La realización es estable. Si cada cuerpo en la escena es reemplazado por su cuerpo paralelo exterior con un radio $r < 1$, la relación de apartamiento permanece inalterada. Además, los cuerpos pueden suavizarse para tener fronteras $C^{1,1}$ preservando la relación.
• Jerarquía de Dimensión y Umbral (Teorema 4.17): El artículo caracteriza precisamente la jerarquía de las relaciones de consecuencia basadas en la dimensión ambiente $d$.
  • Para $d < |E| - 1$, las relaciones de consecuencia forman una cadena estrictamente decreciente: $|=_{0} \supsetneq |=_{1} \supsetneq \dots \supsetneq |=_{|E|-2}$.
  • La jerarquía se estabiliza exactamente en la dimensión $d = |E| - 1$. Para todo $d \ge |E| - 1$, la relación de consecuencia es idéntica a la consecuencia geométrica independiente de la dimensión ($|=_{geo}$).
  • Este umbral se demuestra como exacto; las dimensiones por debajo de $|E|-1$ amplían estrictamente el conjunto de aserciones refutables.
• Cálculo Lógico y Complejidad:
  • Implicación Positiva: La implicación positiva colapsa a una simple subsunción. Una aserción sigue de un conjunto de premisas si y solo si es vacua o está dominada componente a componente (posiblemente tras un intercambio) por una única premisa. Esta verificación es lineal en el tamaño de la entrada para codificaciones ordenadas.
  • Cierre Booleano: El cálculo booleano es sólido, completo y decidible. La satisfacibilidad es NP-completa y la validez es coNP-completa.
  • Conservatividad (Teorema 7.3): Una condición de estratificación formal prueba que el estrato booleano es inerte en el estrato atómico. Ninguna cantidad de razonamiento clásico (negación, disyunción, análisis de casos) puede derivar un nuevo hecho de apartamiento positivo que no sea ya una subsunción de los datos atómicos.

Significancia y Reivindicaciones
El artículo afirma que el "núcleo estable" del discurso de separación es pequeño, exactamente conocido y enteramente subsumente. Argumenta que una vez que la dimensión ambiente supera el umbral de $|E| - 1$, la geometría específica de la escena se vuelve irrelevante para las consecuencias lógicas; la relación está totalmente capturada por las tres leyes axiomáticas.

La significancia reside en proporcionar una "capa lógica y efectiva" a la teoría combinatoria existente de los separoides. Mientras que los trabajos previos se centraron en la universalidad y los homomorfismos, este artículo proporciona:

1. Un teorema de representación cuantitativa con márgenes racionales, haciendo que la estructura lógica sea inspeccionable coordenada por coordenada.
2. Una clasificación de complejidad precisa, distinguiendo entre la trivialidad de la implicación positiva y la dificultad introducida por las combinaciones booleanas.
3. Un resultado de conservatividad que separa formalmente los "datos" (separaciones atómicas) del "razonamiento" (lógica booleana), mostrando que este último no añade nuevas restricciones geométricas.

El artículo se posiciona no como un descubrimiento de nuevos fenómenos geométricos, sino como una formalización rigurosa de los límites lógicos del apartamiento convexo, demostrando que el "olvido" del detalle geométrico no tiene coste en términos de consecuencia lógica, siempre que se permanezca dentro del régimen estable e independiente de la dimensión.