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 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:
- Siembra cada vértice con su estado local.
- Itera la difusión de Tarski hasta el punto fijo (harmónico).
- 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.
- 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).