hifas/ADDENDUM.md

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).

/// 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<A: LatticeCell, B: LatticeCell> {
    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).