# SDD — Addendum: Pista de retículos (Tarski) **Extiende:** `DESIGN.md` (SDD v1) — este documento añade el hito `M-research` y los tickets `T5`–`T7`. **Estado:** Diseño — habilitado por el hallazgo del cierre de M3. **Precondición:** MVP cerrado (M0–M3, objetivos G1–G6). Batería del oráculo verde. `DISCREPANCIES.md` existe. **Última edición:** 2026-07-01 --- ## A. Por qué existe esta pista (el hallazgo de M3, en una línea) El motor lineal del MVP, en el régimen monótono, **no mide consistencia: mide la topología del grafo.** Su codificación colapsa al haz constante, cuya cohomología es `dim H¹ = β₁` (§7.2). Consecuencia probada: `H¹ = 0 ⟺ grafo acíclico`. Sobre grafos cíclicos con datos monótonos pide coordinación de más (triángulo-monótono, cuadrado-monótono en `DISCREPANCIES.md`). Causa raíz, con nombre: **la resta del coboundary.** `(δx)_e = R·x_u − R·x_v` exige un menos. Un join-semilattice no tiene inversos; al linealizarlo, el δ mide *desacuerdo-XOR* en vez de *compatibilidad-por-join*, e inventa obstrucciones-fantasma alrededor de los ciclos. Por eso el fallo es conservador y nunca inverso (consistente con §2.2 / R1). **El objetivo de esta pista es eliminar la resta.** No parchear el motor lineal, sino sustituir su núcleo por una teoría que reconcilie datos de retículo sin restar. --- ## B. El giro matemático De vectores a retículos; de `rank` a punto fijo. | MVP lineal (§7) | Pista de retículos | |---|---| | Stalks = espacios vectoriales | Stalks = retículos (u order-lattices) | | Restricciones = matrices lineales | Restricciones = mapas join-preserving (conexiones de Galois) | | Coboundary `δ` con resta | Laplaciano de Tarski `L` (sin resta) | | Veredicto = `dim H¹` (¿cokernel = 0?) | Veredicto = ¿la difusión llega a un punto fijo consistente? | | Se calcula con eliminación gaussiana | Se calcula iterando `L` a punto fijo (Kleene/Tarski) | **Andamiaje (real, verificado):** Ghrist & Riess, *Cellular Sheaves of Lattices and the Tarski Laplacian*, Homology, Homotopy and Applications 24(1):325–345 (2022); arXiv:2007.04099. Inicia una teoría de Hodge discreta para haces celulares valuados en retículos y conexiones de Galois. La pieza central, el **Laplaciano de Tarski** `L`, es un endomorfismo del complejo de cocadenas cuyos **puntos fijos** dan una cohomología que **coincide con las secciones globales en grado cero**. La convergencia la garantiza el teorema de punto fijo de Tarski; para stalks finitas o de rango finito, converge en tiempo finito (cotas por la altura del retículo). Forma del operador (implementar según Def. 2 / Lemma 7 del paper, no reinventar la fórmula): `L` se descompone en dos partes que se combinan tomando **meet** sobre las aristas incidentes: - **expansión**: `F_{v⊴e}^* ∘ F_{v⊴e}` aplicado al estado local (≥ id: nunca pierde información propia); - **mezcla**: trae el estado del vecino `w` a la arista vía `F_{w⊴e}` y lo devuelve a `v` vía la adjunta de Galois `F_{v⊴e}^*`. La difusión propaga información por los mapas de restricción; su punto fijo es la mejor reconciliación globalmente coherente. --- ## C. Qué significa "obstrucción" ahora (y la honestidad que toca) **Perdemos el `H¹` limpio.** En el mundo de retículos no hay cokernel: sin resta, no hay álgebra lineal. La teoría de cohomología superior para haces de retículos es terreno abierto — la propia línea de Ghrist– Riess prioriza las *aplicaciones del Laplaciano* (grado 0, secciones globales) por encima de un `H¹` cerrado. No prometemos un número de obstrucción; construimos un **diagnóstico dinámico.** El veredicto pasa de algebraico a dinámico: 1. Siembra cada vértice con su estado local. 2. Itera la difusión de Tarski hasta el punto fijo (harmónico). 3. **Corre libre** si el punto fijo es una sección global genuina que *preserva* la información local de cada réplica (cada estado local ≤ / compatible con el valor harmónico). Para CRDTs monótonos alrededor de un ciclo, el punto fijo es exactamente el **join** de los estados → reconcilia sin colapso → sin obstrucción. 4. **Coordina** si la reconciliación no puede sostener los estados locales sin colapsar (p.ej. la difusión fuerza el tope `⊤`, señal de que no existe refinamiento común no trivial). Un `reset` no monótono produce estados incompatibles → colapso → obstrucción real. **Localización (abierto, R-L1).** En el MVP la base del cokernel señalaba las aristas del nudo. Aquí la localización es menos crisp: se toma como las aristas cuyo desacuerdo de restricción *sobrevive* al punto fijo. Es aproximación, no teorema. Empezar por ahí; refinar es investigación. --- ## D. Modelo de tipos (bocetos) Conviven con los tipos del MVP; no los reemplazan (el motor lineal sigue como oráculo topológico barato). ```rust /// Un estado local con estructura de retículo. Reemplaza a `Cell` en la pista de retículos. pub trait LatticeCell: Clone + PartialOrd { fn join(&self, other: &Self) -> Self; // ∨ (asoc., conmut., idempotente) fn meet(&self, other: &Self) -> Self; // ∧ fn bottom() -> Self; // ⊥ fn top() -> Self; // ⊤ } /// Un mapa de restricción como conexión de Galois: par (lower, upper) adjunto. /// lower = F_{v⊴e} (join-preserving), upper = F_{v⊴e}^* (meet-preserving). pub trait GaloisRestriction { fn lower(&self, a: &A) -> B; // preserva joins fn upper(&self, b: &B) -> A; // adjunta; preserva meets // debe cumplir: lower(a) ≤ b ⟺ a ≤ upper(b) } pub struct LatticeSheaf { /* stalks de retículo por vértice/arista + restricciones de Galois */ } /// El Laplaciano de Tarski como operador monótono sobre el retículo producto C⁰. pub struct TarskiLaplacian<'a> { sheaf: &'a LatticeSheaf } impl<'a> TarskiLaplacian<'a> { /// Una aplicación de L (expansión ∧ mezcla), según Def. 2 / Lemma 7 del paper. pub fn step(&self, x: &Cochain) -> Cochain { /* ... */ } /// Itera a punto fijo (Kleene desde ⊥ hacia arriba, o desde la siembra local). /// Converge en tiempo finito para retículos de altura finita (Lemma 8 + Tarski). pub fn harmonize(&self, seed: &Cochain) -> Cochain { /* ... */ } } ``` ### D.1 Encodings concretos de los CRDTs del MVP como retículos - `GCounter` → producto de cadenas `ℕ` bajo `max` (join) / `min` (meet). Monótono por construcción. - `ResettableRegister` → retículo donde el `reset` introduce elementos **incomparables** (no hay `≤` entre pre-reset y post-reset), de modo que su join no colapsa a un valor consistente. Esto es lo que produce el colapso a `⊤` en §C.4 y hace que su obstrucción sea real, no topológica. --- ## E. Cambios de módulos Aditivos, no destructivos: ``` Nuevo src/lattice.rs — LatticeCell, GaloisRestriction, encodings de §D.1 Nuevo src/tarski.rs — LatticeSheaf, TarskiLaplacian, harmonize (punto fijo) Editar src/verdict.rs — añadir Verdict::via_tarski(...) junto al via_cohomology(...) lineal Editar src/oracle.rs — reusar el mismo oracle_verdict; el objetivo es que el haz lo iguale Editar DISCREPANCIES.md — marcar cada discrepancia como RESUELTA / PERSISTE tras la difusión ``` El módulo `cohomology` del MVP **no se toca**: queda como detector topológico barato y como control histórico. El punto científico es exhibir la diferencia entre ambos veredictos sobre los mismos casos. --- ## F. Criterio de éxito de la pista Un solo test maestro manda: **los casos de `DISCREPANCIES.md` deben cambiar de color.** - `triangulo-monotono`, `cuadrado-monotono`: MVP lineal decía "coordina" (falso positivo topológico). Con Tarski deben decir **"corre libre"**, igualando al oráculo. La difusión reconcilia al join. - Todo caso no monótono (`reset` en ciclo o en árbol): debe **seguir** diciendo "coordina", ahora por la razón correcta (colapso semántico), no por topología. - Invariante nuevo para `proptest`: **monótono sobre grafo arbitrario (cíclico incluido) ⟹ corre libre.** Este es el invariante que el MVP lineal *no podía* satisfacer; que Tarski lo satisfaga ES la validación de la Hipótesis H (§2.2) en su forma correcta. Si esos tres se cumplen, la brecha de modelado de §2.3 queda cerrada y la Hipótesis H pasa de "se sostiene solo en el caso acíclico" a "se sostiene en general bajo el encoding de retículos". --- ## G. Hito M-research y tickets ### M-research — Haces de retículos con Laplaciano de Tarski Cierra la brecha §2.3. Prerrequisito de M4: sin esto, cablear a Tawasuyu/Hammer sobre topologías cíclicas (gossip/mesh) daría falsos positivos de coordinación crónicos. **T5 — Retículos y restricciones de Galois.** "Crea `src/lattice.rs` según §D: el trait `LatticeCell` (join/meet/bottom/top) y `GaloisRestriction` (lower/upper adjuntos con la ley `lower(a) ≤ b ⟺ a ≤ upper(b)`). Implementa los encodings de §D.1: `GCounter` como producto de cadenas ℕ, `ResettableRegister` con post-reset incomparable. Tests: leyes de retículo (asociatividad, conmutatividad, idempotencia, absorción), monotonía de `lower`, y la ley adjunta de Galois verificada por `proptest`. No toques el motor lineal." **T6 — Laplaciano de Tarski y difusión a punto fijo.** "Crea `src/tarski.rs`: `LatticeSheaf` y `TarskiLaplacian` con `step` (expansión ∧ mezcla, según Def. 2 / Lemma 7 de Ghrist–Riess 2022) y `harmonize` (itera a punto fijo por Kleene; asume altura finita, corta al detectar punto fijo). Prueba de cordura CLAVE — el giro respecto al MVP: para el **haz constante de retículos sobre un ciclo** (triángulo), la difusión debe converger al join y reportar **sin obstrucción** — exactamente lo contrario del `H¹=β₁` del haz constante lineal (§7.2). Si esa prueba no invierte el resultado del MVP, el Laplaciano está mal ensamblado. Test de convergencia en tiempo finito acotado por la altura del retículo." **T7 — Veredicto por difusión y cierre de discrepancias.** "Añade `Verdict::via_tarski` en `verdict.rs` (§C: corre libre si el punto fijo preserva lo local; coordina si colapsa a ⊤). Reejecuta la batería del oráculo por la ruta Tarski. Test maestro (§F): `triangulo- monotono` y `cuadrado-monotono` pasan a 'corre libre' e igualan al oráculo; los casos no monótonos siguen en 'coordina'. Añade el invariante `proptest` 'monótono sobre grafo arbitrario ⟹ corre libre'. Actualiza `DISCREPANCIES.md`: marca cada entrada RESUELTA o PERSISTE, y documenta cualquier caso nuevo donde Tarski y oráculo discrepen — ese residuo, si existe, es el siguiente resultado científico." --- ## H. Riesgos y preguntas abiertas de la pista - **R-L1 (localización).** Señalar *qué* aristas forman el nudo es limpio en el MVP (base del cokernel) y difuso aquí (aristas cuyo desacuerdo sobrevive al punto fijo). Aproximado; refinar es investigación. - **R-L2 (cohomología superior).** No hay `H¹` cerrado para haces de retículos; solo grado 0 vía puntos fijos. Si más adelante necesitas obstrucciones de orden superior, es territorio no resuelto en la literatura — no lo prometas. - **R-L3 (fidelidad del encoding).** Que `ResettableRegister` colapse correctamente depende de modelar el post-reset como *incomparable*, no como un valor mayor. Un encoding descuidado volvería a esconder o inventar conflictos. Cada CRDT necesita su encoding de retículo justificado, igual que en el MVP necesitaba su encoding lineal (Q1). - **Q-L1.** ¿Basta el retículo, o algún CRDT real (p.ej. con métricas/pesos) pide ya un quantale? Si aparece, el horizonte es el Laplaciano de Lawvere (categorías enriquecidas en quantales) y la difusión de haces no-lineal de Riess et al. — fuera de alcance; anotar y seguir. --- ## I. Referencias añadidas - R. Ghrist, H. Riess — *Cellular Sheaves of Lattices and the Tarski Laplacian*, Homology, Homotopy and Applications 24(1):325–345 (2022). arXiv:2007.04099. (Andamiaje central de esta pista.) - H. Riess — tesis doctoral sobre haces valuados en retículos y optimización en redes multi-agente (Tarski sheaves). (Contexto y aplicaciones a consenso.) - Y. Zhao, T. Hanks, H. Riess et al. — *Asynchronous nonlinear sheaf diffusion for multi-agent coordination* (2026); y trabajo relacionado sobre difusión de haces no-lineal / co-diseño enriquecido en quantales. (Horizonte Q-L1; solo si el retículo se queda corto.) - (Del SDD v1) Shapiro et al. 2011 (CRDTs); Hellerstein–Alvaro (CALM); Hansen–Ghrist 2019 (haces espectrales, base lineal del MVP).