gioser

tawasuyu/hifas

Motor en Rust para decidir, con demostración y no a ojo, cuándo un conjunto de réplicas local-first puede operar sin coordinación y cuándo no — y, cuando la respuesta es "sí, dentro de límites", proveer el mecanismo que lo garantiza.

Rust 24Markdown 15TOML 1358 Definiciones

⎇ main ADDENDUM.md Markdown · 220 líneas · 12.4 KB Historia crudo

T5: retículos y restricciones de Galois (pista de Tarski) fc986d7cd · Sergio ·

1# SDD — Addendum: Pista de retículos (Tarski)
2
3**Extiende:** `DESIGN.md` (SDD v1) — este documento añade el hito `M-research` y los tickets `T5`–`T7`.
4**Estado:** Diseño — habilitado por el hallazgo del cierre de M3.
5**Precondición:** MVP cerrado (M0–M3, objetivos G1–G6). Batería del oráculo verde. `DISCREPANCIES.md` existe.
6**Última edición:** 2026-07-01
7
8---
9
10## A. Por qué existe esta pista (el hallazgo de M3, en una línea)
11
12El motor lineal del MVP, en el régimen monótono, **no mide consistencia: mide la topología del grafo.**
13Su codificación colapsa al haz constante, cuya cohomología es `dim H¹ = β₁` (§7.2). Consecuencia probada:
14`H¹ = 0 ⟺ grafo acíclico`. Sobre grafos cíclicos con datos monótonos pide coordinación de más
15(triángulo-monótono, cuadrado-monótono en `DISCREPANCIES.md`).
16
17Causa raíz, con nombre: **la resta del coboundary.** `(δx)_e = R·x_u − R·x_v` exige un menos.
18Un join-semilattice no tiene inversos; al linealizarlo, el δ mide *desacuerdo-XOR* en vez de
19*compatibilidad-por-join*, e inventa obstrucciones-fantasma alrededor de los ciclos. Por eso el fallo
20es conservador y nunca inverso (consistente con §2.2 / R1).
21
22**El objetivo de esta pista es eliminar la resta.** No parchear el motor lineal, sino sustituir su
23núcleo por una teoría que reconcilie datos de retículo sin restar.
24
25---
26
27## B. El giro matemático
28
29De vectores a retículos; de `rank` a punto fijo.
30
31| MVP lineal (§7) | Pista de retículos |
32|---|---|
33| Stalks = espacios vectoriales | Stalks = retículos (u order-lattices) |
34| Restricciones = matrices lineales | Restricciones = mapas join-preserving (conexiones de Galois) |
35| Coboundary `δ` con resta | Laplaciano de Tarski `L` (sin resta) |
36| Veredicto = `dim H¹` (¿cokernel = 0?) | Veredicto = ¿la difusión llega a un punto fijo consistente? |
37| Se calcula con eliminación gaussiana | Se calcula iterando `L` a punto fijo (Kleene/Tarski) |
38
39**Andamiaje (real, verificado):** Ghrist & Riess, *Cellular Sheaves of Lattices and the Tarski
40Laplacian*, Homology, Homotopy and Applications 24(1):325–345 (2022); arXiv:2007.04099.
41Inicia una teoría de Hodge discreta para haces celulares valuados en retículos y conexiones de Galois.
42La pieza central, el **Laplaciano de Tarski** `L`, es un endomorfismo del complejo de cocadenas cuyos
43**puntos fijos** dan una cohomología que **coincide con las secciones globales en grado cero**. La
44convergencia la garantiza el teorema de punto fijo de Tarski; para stalks finitas o de rango finito,
45converge en tiempo finito (cotas por la altura del retículo).
46
47Forma del operador (implementar según Def. 2 / Lemma 7 del paper, no reinventar la fórmula):
48`L` se descompone en dos partes que se combinan tomando **meet** sobre las aristas incidentes:
49- **expansión**: `F_{v⊴e}^* ∘ F_{v⊴e}` aplicado al estado local (≥ id: nunca pierde información propia);
50- **mezcla**: trae el estado del vecino `w` a la arista vía `F_{w⊴e}` y lo devuelve a `v` vía la
51  adjunta de Galois `F_{v⊴e}^*`.
52
53La difusión propaga información por los mapas de restricción; su punto fijo es la mejor reconciliación
54globalmente coherente.
55
56---
57
58## C. Qué significa "obstrucción" ahora (y la honestidad que toca)
59
60**Perdemos el `H¹` limpio.** En el mundo de retículos no hay cokernel: sin resta, no hay álgebra lineal.
61La teoría de cohomología superior para haces de retículos es terreno abierto — la propia línea de Ghrist–
62Riess prioriza las *aplicaciones del Laplaciano* (grado 0, secciones globales) por encima de un `H¹`
63cerrado. No prometemos un número de obstrucción; construimos un **diagnóstico dinámico.**
64
65El veredicto pasa de algebraico a dinámico:
66
671. Siembra cada vértice con su estado local.
682. Itera la difusión de Tarski hasta el punto fijo (harmónico).
693. **Corre libre** si el punto fijo es una sección global genuina que *preserva* la información local
70   de cada réplica (cada estado local ≤ / compatible con el valor harmónico). Para CRDTs monótonos
71   alrededor de un ciclo, el punto fijo es exactamente el **join** de los estados → reconcilia sin
72   colapso → sin obstrucción.
734. **Coordina** si la reconciliación no puede sostener los estados locales sin colapsar (p.ej. la
74   difusión fuerza el tope `⊤`, señal de que no existe refinamiento común no trivial). Un `reset`
75   no monótono produce estados incompatibles → colapso → obstrucción real.
76
77**Localización (abierto, R-L1).** En el MVP la base del cokernel señalaba las aristas del nudo. Aquí la
78localización es menos crisp: se toma como las aristas cuyo desacuerdo de restricción *sobrevive* al punto
79fijo. Es aproximación, no teorema. Empezar por ahí; refinar es investigación.
80
81---
82
83## D. Modelo de tipos (bocetos)
84
85Conviven con los tipos del MVP; no los reemplazan (el motor lineal sigue como oráculo topológico barato).
86
87```rust
88/// Un estado local con estructura de retículo. Reemplaza a `Cell` en la pista de retículos.
89pub trait LatticeCell: Clone + PartialOrd {
90    fn join(&self, other: &Self) -> Self;   // ∨  (asoc., conmut., idempotente)
91    fn meet(&self, other: &Self) -> Self;    // ∧
92    fn bottom() -> Self;                     // ⊥
93    fn top() -> Self;                        // ⊤
94}
95
96/// Un mapa de restricción como conexión de Galois: par (lower, upper) adjunto.
97/// lower = F_{v⊴e} (join-preserving), upper = F_{v⊴e}^* (meet-preserving).
98pub trait GaloisRestriction<A: LatticeCell, B: LatticeCell> {
99    fn lower(&self, a: &A) -> B;   // preserva joins
100    fn upper(&self, b: &B) -> A;   // adjunta; preserva meets
101    // debe cumplir: lower(a) ≤ b  ⟺  a ≤ upper(b)
102}
103
104pub struct LatticeSheaf { /* stalks de retículo por vértice/arista + restricciones de Galois */ }
105
106/// El Laplaciano de Tarski como operador monótono sobre el retículo producto C⁰.
107pub struct TarskiLaplacian<'a> { sheaf: &'a LatticeSheaf }
108
109impl<'a> TarskiLaplacian<'a> {
110    /// Una aplicación de L (expansión ∧ mezcla), según Def. 2 / Lemma 7 del paper.
111    pub fn step(&self, x: &Cochain) -> Cochain { /* ... */ }
112
113    /// Itera a punto fijo (Kleene desde ⊥ hacia arriba, o desde la siembra local).
114    /// Converge en tiempo finito para retículos de altura finita (Lemma 8 + Tarski).
115    pub fn harmonize(&self, seed: &Cochain) -> Cochain { /* ... */ }
116}
117```
118
119### D.1 Encodings concretos de los CRDTs del MVP como retículos
120- `GCounter` → producto de cadenas `ℕ` bajo `max` (join) / `min` (meet). Monótono por construcción.
121- `ResettableRegister` → retículo donde el `reset` introduce elementos **incomparables** (no hay `≤`
122  entre pre-reset y post-reset), de modo que su join no colapsa a un valor consistente. Esto es lo que
123  produce el colapso a `⊤` en §C.4 y hace que su obstrucción sea real, no topológica.
124
125---
126
127## E. Cambios de módulos
128
129Aditivos, no destructivos:
130
131```
132Nuevo  src/lattice.rs   — LatticeCell, GaloisRestriction, encodings de §D.1
133Nuevo  src/tarski.rs    — LatticeSheaf, TarskiLaplacian, harmonize (punto fijo)
134Editar src/verdict.rs   — añadir Verdict::via_tarski(...) junto al via_cohomology(...) lineal
135Editar src/oracle.rs    — reusar el mismo oracle_verdict; el objetivo es que el haz lo iguale
136Editar DISCREPANCIES.md — marcar cada discrepancia como RESUELTA / PERSISTE tras la difusión
137```
138
139El módulo `cohomology` del MVP **no se toca**: queda como detector topológico barato y como control
140histórico. El punto científico es exhibir la diferencia entre ambos veredictos sobre los mismos casos.
141
142---
143
144## F. Criterio de éxito de la pista
145
146Un solo test maestro manda: **los casos de `DISCREPANCIES.md` deben cambiar de color.**
147
148- `triangulo-monotono`, `cuadrado-monotono`: MVP lineal decía "coordina" (falso positivo topológico).
149  Con Tarski deben decir **"corre libre"**, igualando al oráculo. La difusión reconcilia al join.
150- Todo caso no monótono (`reset` en ciclo o en árbol): debe **seguir** diciendo "coordina", ahora por la
151  razón correcta (colapso semántico), no por topología.
152- Invariante nuevo para `proptest`: **monótono sobre grafo arbitrario (cíclico incluido) ⟹ corre libre.**
153  Este es el invariante que el MVP lineal *no podía* satisfacer; que Tarski lo satisfaga ES la validación
154  de la Hipótesis H (§2.2) en su forma correcta.
155
156Si esos tres se cumplen, la brecha de modelado de §2.3 queda cerrada y la Hipótesis H pasa de "se
157sostiene solo en el caso acíclico" a "se sostiene en general bajo el encoding de retículos".
158
159---
160
161## G. Hito M-research y tickets
162
163### M-research — Haces de retículos con Laplaciano de Tarski
164Cierra la brecha §2.3. Prerrequisito de M4: sin esto, cablear a Tawasuyu/Hammer sobre topologías
165cíclicas (gossip/mesh) daría falsos positivos de coordinación crónicos.
166
167**T5 — Retículos y restricciones de Galois.**
168"Crea `src/lattice.rs` según §D: el trait `LatticeCell` (join/meet/bottom/top) y `GaloisRestriction`
169(lower/upper adjuntos con la ley `lower(a) ≤ b ⟺ a ≤ upper(b)`). Implementa los encodings de §D.1:
170`GCounter` como producto de cadenas ℕ, `ResettableRegister` con post-reset incomparable. Tests: leyes de
171retículo (asociatividad, conmutatividad, idempotencia, absorción), monotonía de `lower`, y la ley
172adjunta de Galois verificada por `proptest`. No toques el motor lineal."
173
174**T6 — Laplaciano de Tarski y difusión a punto fijo.**
175"Crea `src/tarski.rs`: `LatticeSheaf` y `TarskiLaplacian` con `step` (expansión ∧ mezcla, según Def. 2 /
176Lemma 7 de Ghrist–Riess 2022) y `harmonize` (itera a punto fijo por Kleene; asume altura finita, corta al
177detectar punto fijo). Prueba de cordura CLAVE — el giro respecto al MVP: para el **haz constante de
178retículos sobre un ciclo** (triángulo), la difusión debe converger al join y reportar **sin obstrucción**
179— exactamente lo contrario del `H¹=β₁` del haz constante lineal (§7.2). Si esa prueba no invierte el
180resultado del MVP, el Laplaciano está mal ensamblado. Test de convergencia en tiempo finito acotado por
181la altura del retículo."
182
183**T7 — Veredicto por difusión y cierre de discrepancias.**
184"Añade `Verdict::via_tarski` en `verdict.rs` (§C: corre libre si el punto fijo preserva lo local; coordina
185si colapsa a ⊤). Reejecuta la batería del oráculo por la ruta Tarski. Test maestro (§F): `triangulo-
186monotono` y `cuadrado-monotono` pasan a 'corre libre' e igualan al oráculo; los casos no monótonos siguen
187en 'coordina'. Añade el invariante `proptest` 'monótono sobre grafo arbitrario ⟹ corre libre'. Actualiza
188`DISCREPANCIES.md`: marca cada entrada RESUELTA o PERSISTE, y documenta cualquier caso nuevo donde Tarski y
189oráculo discrepen — ese residuo, si existe, es el siguiente resultado científico."
190
191---
192
193## H. Riesgos y preguntas abiertas de la pista
194
195- **R-L1 (localización).** Señalar *qué* aristas forman el nudo es limpio en el MVP (base del cokernel) y
196  difuso aquí (aristas cuyo desacuerdo sobrevive al punto fijo). Aproximado; refinar es investigación.
197- **R-L2 (cohomología superior).** No hay `H¹` cerrado para haces de retículos; solo grado 0 vía puntos
198  fijos. Si más adelante necesitas obstrucciones de orden superior, es territorio no resuelto en la
199  literatura — no lo prometas.
200- **R-L3 (fidelidad del encoding).** Que `ResettableRegister` colapse correctamente depende de modelar
201  el post-reset como *incomparable*, no como un valor mayor. Un encoding descuidado volvería a esconder
202  o inventar conflictos. Cada CRDT necesita su encoding de retículo justificado, igual que en el MVP
203  necesitaba su encoding lineal (Q1).
204- **Q-L1.** ¿Basta el retículo, o algún CRDT real (p.ej. con métricas/pesos) pide ya un quantale? Si
205  aparece, el horizonte es el Laplaciano de Lawvere (categorías enriquecidas en quantales) y la difusión
206  de haces no-lineal de Riess et al. — fuera de alcance; anotar y seguir.
207
208---
209
210## I. Referencias añadidas
211
212- R. Ghrist, H. Riess — *Cellular Sheaves of Lattices and the Tarski Laplacian*, Homology, Homotopy and
213  Applications 24(1):325–345 (2022). arXiv:2007.04099. (Andamiaje central de esta pista.)
214- H. Riess — tesis doctoral sobre haces valuados en retículos y optimización en redes multi-agente
215  (Tarski sheaves). (Contexto y aplicaciones a consenso.)
216- Y. Zhao, T. Hanks, H. Riess et al. — *Asynchronous nonlinear sheaf diffusion for multi-agent
217  coordination* (2026); y trabajo relacionado sobre difusión de haces no-lineal / co-diseño enriquecido
218  en quantales. (Horizonte Q-L1; solo si el retículo se queda corto.)
219- (Del SDD v1) Shapiro et al. 2011 (CRDTs); Hellerstein–Alvaro (CALM); Hansen–Ghrist 2019 (haces
220  espectrales, base lineal del MVP).

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 vectorialesStalks = retículos (u order-lattices)
Restricciones = matrices linealesRestricciones = mapas join-preserving (conexiones de Galois)
Coboundary δ con restaLaplaciano 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 gaussianaSe 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:

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


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.

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


I. Referencias añadidas