tawasuyu/hifas

T9 §A/§B: corrige los dos errores de T8c. (1) el veredicto de T8 era
DETECCIÓN reactiva por-estado, no evitación; (2) trataba un invariante
GLOBAL como edge-local, de ahí el falso-verde particionado.

- invariant::GlobalInvariant (restricción global valor≥floor, no edge-local;
  slack = initial - floor).
- escrow::Budget/SpendResult: reparto con Σ b_i ≤ slack (is_valid_split,
  split proporcional por división entera), gasto local try_spend (Local |
  NeedsRebalance{deficit}), certificado value_after.
- verdict::Verdict::via_escrow: Local→RunsFree (cero coord, correcto incluso
  particionado), NeedsRebalance→NeedsCoordination localizado. Nunca 'libre
  global' a ciegas.

Tests: EL CERTIFICADO (proptest) — para todo reparto válido y todo gasto
spent_i ≤ b_i (particiones y máximos incluidos), valor = inicial - Σspent ≥
piso, por construcción. El caso 60/60 con [50,50]: particionado recibe
NeedsRebalance (bloqueado), no Local — muere el falso-verde. El detector de
T8 se conserva pero su 'topología importa' se reetiqueta como PUNTO CIEGO.

Honestidad §B: escrow no vence a CALM, transforma la operación para que sea
I-confluente. 49 tests, clippy limpio.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

diff --git a/T9.md b/T9.md
new file mode 100644
index 0000000..60e0782
--- /dev/null
+++ b/T9.md
@@ -0,0 +1,230 @@
+# SDD — Addendum: T9 · De detección a evitación (escrow topología-consciente)
+
+**Extiende:** `DESIGN.md` + `DESIGN_lattice.md` (T5–T7) + `DESIGN_T8.md` (T8).
+**Estado:** Diseño — habilitado por el desmontaje del "resultado fuerte" de T8c.
+**Precondición:** T8 cerrado. Existe `STRONG_RESULT.md` con el testigo `[10,10]/[60,60]`.
+**Última edición:** 2026-07-01
+
+---
+
+## A. Qué corrige T9 (los dos errores de T8, nombrados)
+
+**Error 1 — detección disfrazada de evitación.** El veredicto de T8 (`corre libre ⟺ punto_fijo ∈ V`)
+funde dos estados ya divergidos y comprueba el merge. Eso es *detección reactiva de conflicto por-estado*,
+no *evitación de coordinación*. I-confluence (Bailis) cuantifica sobre **todos los estados alcanzables**:
+"retirar con saldo ≥ 0" no es I-confluente porque *existe* un [60,60] que rompe `I` → coordina,
+categórico, igual que CALM (`I-confluente ⟺ monótono`, Prop. 3 de Complete CALM). El testigo `[10,10]`
+no es una cuña más fina; responde otra pregunta, y para un invariante duro llega tarde: si hubiera sido
+[60,60], ambos retiros ya se aceptaron y repararlos es compensación = coordinación.
+
+**Error 2 — invariante global tratado como edge-local.** "Saldo total ≥ 0" acopla a **todas** las
+réplicas que tocan el recurso, compartan arista o no. Codificado por aristas pares, quitar la arista
+(partición) borra la restricción del haz — justo cuando el acoplamiento sigue intacto. De ahí el
+falso-verde: `particionado → libre` es el caso *más* peligroso reportado como seguro, porque el haz está
+**ciego** a él, no porque sea seguro.
+
+T9 arregla ambos de raíz: el invariante pasa a ser una **restricción global** (una hiperarista / celda de
+recurso incidente a todas las réplicas), y el veredicto pasa de *fundir-y-comprobar* a
+**repartir-y-chequear-local** — el esquema de **escrow**.
+
+---
+
+## B. La cura canónica: escrow / Bounded Counter
+
+Prior art, no lo inventamos: método de escrow (O'Neil 1986) materializado como **Bounded Counter CRDT**
+(Balegas, Serra, Duarte, Ferreira, Shapiro, Rodrigues, Preguiça — SRDS 2015).
+
+Idea, para invariante `valor ≥ K`:
+
+1. Define el *slack* global `S = valor − K` (lo que se puede gastar sin romper `I`).
+2. **Reparte** `S` en presupuestos por réplica `b_i` con la condición dura `Σ b_i ≤ S`.
+3. Mientras a `r_i` le quede presupuesto, **retira localmente sin coordinar con nadie** — y esto es
+   correcto **incluso particionada**, porque `b_i` es suyo.
+4. **La única coordinación** aparece cuando `r_i` agota `b_i` y necesita **rebalancear**: pedir
+   presupuesto a un vecino que aún tenga. Local, entre dos réplicas, no global.
+
+**El certificado (esto es lo que el detector de T8 no podía dar).** Sea `spent_i ≤ b_i` en cada réplica.
+Entonces `valor = inicial − Σ spent_i ≥ inicial − Σ b_i ≥ inicial − S = K`. Se cumple **para toda
+ejecución, todo orden, toda partición** — no se descubre tarde, se garantiza por construcción. Eso es
+evitación de coordinación real, cuantificada sobre todos los estados alcanzables dentro de los
+presupuestos.
+
+**Honestidad (para no repetir el sobre-reclamo de T8).** Escrow **tampoco** vence a CALM. *Transforma*
+la operación: de "retirar sin límite" (no I-confluente → coordina) a "retirar dentro de presupuesto"
+(I-confluente / monótona → libre), al costo de un rebalanceo ocasional. No rompes el teorema; re-ingenieras
+la operación para que caiga del lado bueno. Dilo así en `STRONG_RESULT.md`.
+
+---
+
+## C. Dónde el haz por fin se gana el sueldo (y no es derivativo)
+
+Bounded Counter usa esquemas simples para repartir y rebalancear (preguntar a un peer). El candidato a
+**contribución real** de T9 es hacer el reparto y el rebalanceo como un **flujo sobre el grafo de
+comunicación**, con localización principiada:
+
+- **Presupuesto** = una 0-cocadena `b` sobre los vértices, con `Σ b_i ≤ S`.
+- **Rebalanceo** = un flujo (1-cocadena) que mueve presupuesto por las aristas, **conservando el total**
+  (`b_i -= δ`, `b_j += δ` ⟹ `Σ b` invariante ⟹ el certificado se preserva).
+- **El Laplaciano rutea.** La "presión" para rebalancear es el gradiente de presupuesto restante a través
+  de las aristas; un flujo Laplaciano lo suaviza proactivamente para que las réplicas rara vez lleguen a
+  cero. Cuando una se seca, el Laplaciano **localiza** el flujo mínimo que la repone desde vecinos con
+  excedente — el rebalanceo mínimo, edge-local, no un consenso global.
+
+Cierre de arco honesto: el Laplaciano lineal que en el MVP era un **detector con falso-positivo** (H¹=β₁)
+reaparece aquí como un **ruteador de presupuesto legítimo**. Misma máquina, ahora en el problema correcto:
+no detectar conflictos post-hoc, sino repartir derechos proactivamente. Es una aplicación genuina del
+Laplaciano de haces (Hansen–Ghrist) a consenso/flujo. Para un presupuesto escalar basta el Laplaciano de
+grafo ordinario; el Laplaciano de haces solo hace falta si los presupuestos son vectoriales (multi-recurso,
+§H reach).
+
+---
+
+## D. Modelo de tipos (bocetos)
+
+```rust
+/// Restricción global: NO edge-local. Incide sobre todas las réplicas que tocan el recurso.
+pub struct GlobalInvariant {
+    pub floor: i64,        // K en  valor ≥ K
+    pub initial: i64,      // valor inicial del recurso
+}
+impl GlobalInvariant {
+    pub fn slack(&self) -> i64 { self.initial - self.floor }   // S
+}
+
+/// Presupuesto repartido: la 0-cocadena b sobre las réplicas. Invariante: sum(b) ≤ slack.
+pub struct Budget { pub per_replica: Vec<i64> }
+impl Budget {
+    pub fn is_valid_split(&self, inv: &GlobalInvariant) -> bool {
+        self.per_replica.iter().sum::<i64>() <= inv.slack()
+            && self.per_replica.iter().all(|&b| b >= 0)
+    }
+    /// Gasto local: permitido sin coordinar sii hay presupuesto.
+    pub fn try_spend(&mut self, r: usize, amount: i64) -> SpendResult { /* ... */ }
+}
+
+pub enum SpendResult {
+    Local,                          // dentro de presupuesto: cero coordinación
+    NeedsRebalance { deficit: i64 } // presupuesto agotado: coordinación edge-local
+}
+
+/// Ruteo de presupuesto sobre el grafo (Laplaciano). Conserva el total.
+pub struct BudgetRouter<'a> { nerve: &'a Nerve, budget: &'a mut Budget }
+impl<'a> BudgetRouter<'a> {
+    /// Flujo mínimo que repone a `r` desde vecinos con excedente. Devuelve las aristas usadas.
+    pub fn rebalance_to(&mut self, r: usize, deficit: i64) -> Vec<(usize, usize, i64)> { /* ... */ }
+    /// Difusión proactiva: suaviza el presupuesto para minimizar futuros déficits.
+    pub fn diffuse(&mut self) { /* paso de Laplaciano, conserva sum(b) */ }
+}
+```
+
+---
+
+## E. Cambios de módulos
+
+```
+Nuevo  src/invariant.rs — GlobalInvariant (restricción global, no edge-local)
+Nuevo  src/escrow.rs    — Budget, try_spend, el certificado sum(b) ≤ slack
+Nuevo  src/router.rs    — BudgetRouter: rebalanceo y difusión por Laplaciano (reusa el grafo del nervio)
+Editar src/verdict.rs   — Verdict::via_escrow: Local | NeedsRebalance{edges}, NUNCA "libre global" ciego
+Editar STRONG_RESULT.md — corregir el reclamo de T8 (§G)
+Nuevo  COMPARISON.md    — detector (T8) vs escrow (T9) sobre los mismos escenarios, con el punto ciego
+```
+
+El detector de T8 **no se borra**: queda como capa de reconciliación/alarma honesta (para conflictos que
+el escrow no cubre, p.ej. invariantes sin estructura de recurso divisible). Pero deja de ser el consejero
+de coordinación.
+
+---
+
+## F. El certificado y la muerte del falso-verde
+
+Test central de T9, que **invierte** el punto ciego de T8:
+
+- **Certificado exhaustivo.** Para cualquier reparto válido (`Σ b_i ≤ S`) y **cualquier** combinación de
+  gastos con `spent_i ≤ b_i` — incluidas todas las réplicas gastando su máximo a la vez, incluidas
+  particiones arbitrarias — el invariante global `valor ≥ K` se preserva. `proptest` sobre repartos y
+  gastos aleatorios; la aserción es el certificado de §B, no un merge concreto.
+- **El falso-verde particionado desaparece.** El caso 60/60 de T8: con presupuestos `[50,50]` (reparto
+  válido de `S=100`), una réplica particionada que intenta retirar 60 recibe `NeedsRebalance{deficit:10}`
+  — correctamente **bloqueada/pendiente de coordinación**, no "libre". Contrasta explícitamente en
+  `COMPARISON.md` contra el detector de T8, que decía "particionado → libre".
+- **Rebalanceo conserva y localiza.** Tras cualquier `rebalance_to`, `Σ b` es invariante (certificado
+  intacto) y las aristas devueltas son edge-locales al nodo seco. `proptest`: nunca un rebalanceo toca una
+  réplica no adyacente al déficit.
+
+---
+
+## G. Corrección obligatoria de `STRONG_RESULT.md`
+
+T9 no está completo hasta reescribir el reclamo de T8 con lo que el testigo realmente probó:
+
+- **Quitar:** "versión fuerte probada / más fino que CALM / I-confluence sobre el grafo real."
+- **Poner:** "detección de conflicto por-estado con localización, topología-consciente. NO es una
+  separación respecto a I-confluence ni a CALM — ambos coinciden (Prop. 3). El caso particionado-60/60
+  queda documentado como **punto ciego**: el detector reporta 'libre' porque, sin arista, no ve el
+  acoplamiento del invariante global. Esto motivó T9."
+- **Añadir puntero** a `COMPARISON.md` y al certificado de escrow como la evitación real.
+
+Un error registrado con honestidad vale más que un resultado fuerte reclamado de más. Ese es el criterio.
+
+---
+
+## H. Riesgos y horizonte
+
+- **R-T9a (reparto inicial).** `Σ b_i ≤ S` deja libertad en *cómo* repartir. Un reparto malo (todo a una
+  réplica) causa rebalanceos constantes = mucha coordinación. La calidad del reparto es un problema de
+  optimización sobre el grafo — donde el Laplaciano/difusión aporta. No es corrección (el certificado
+  aguanta cualquier reparto válido), es *rendimiento*. Sepáralos en los tests.
+- **R-T9b (recurso no divisible).** Escrow sirve para invariantes sobre un *recurso conservado divisible*
+  (saldo, stock, cupo). Invariantes no divisibles (unicidad de ID, integridad referencial) NO se resuelven
+  con presupuestos numéricos — ahí el detector de T8 sigue siendo lo mejor que tienes, o se necesitan
+  reservas de otro tipo. Documenta la frontera; no vendas escrow como universal.
+- **R-T9c (honestidad de novedad).** Bounded Counter/escrow es prior art (Balegas 2015). Tu candidato a
+  novedad es el **ruteo/localización del presupuesto por el grafo real** y, como reach, **múltiples
+  invariantes acoplados** — que el propio paper de Balegas señala como no resuelto ("constraints over
+  multiple counters... only way is to store them in a single object"). Ese multi-invariante vía haces sí
+  sería nuevo. Reclámalo solo si lo construyes.
+- **Q-T9 (M4).** Con escrow, el adaptador a Tawasuyu/Hammer cablea un mecanismo libre de coordinación de
+  verdad: presupuestos por nodo soberano, gasto local sin sync, rebalanceo edge-local al secarse. Eso es
+  lo que justifica el aparato sobre una malla de gossip. El detector de T8, no.
+
+---
+
+## I. Tickets
+
+**T9a — Invariante global + certificado de escrow.**
+"Crea `src/invariant.rs` (`GlobalInvariant`, restricción global no edge-local) y `src/escrow.rs`
+(`Budget`, `try_spend`, `is_valid_split`). Implementa el veredicto `Verdict::via_escrow`:
+`Local` si hay presupuesto, `NeedsRebalance{deficit}` si no. Test del certificado (§F): `proptest` que,
+para todo reparto válido y toda combinación de gastos dentro de presupuesto —incluidas particiones y todos
+gastando el máximo—, verifica `valor ≥ K`. Reproduce el caso 60/60 de T8 con presupuestos [50,50] y
+verifica que la réplica particionada recibe `NeedsRebalance`, no `Local`."
+
+**T9b — Ruteo de presupuesto por Laplaciano.**
+"Crea `src/router.rs` (`BudgetRouter`) reusando el grafo del nervio. `rebalance_to(r, deficit)` calcula el
+flujo mínimo que repone a `r` desde vecinos con excedente y devuelve las aristas usadas; `diffuse` hace un
+paso de Laplaciano que suaviza el presupuesto conservando `Σ b`. Tests: (1) todo rebalanceo conserva
+`Σ b` (certificado intacto); (2) las aristas del rebalanceo son adyacentes al nodo seco (nunca toca una
+réplica no vecina); (3) tras `diffuse`, la varianza del presupuesto no aumenta. Para presupuesto escalar
+usa el Laplaciano de grafo ordinario; deja un `TODO` marcado para el Laplaciano de haces si se pasa a
+multi-recurso."
+
+**T9c — Comparación honesta y corrección del registro.**
+"Crea `COMPARISON.md`: corre el detector de T8 y el certificador de escrow de T9 sobre los mismos
+escenarios (conectado, particionado, 10/10, 60/60, repartos varios) y tabula sus veredictos, resaltando el
+falso-verde particionado del detector frente al bloqueo correcto del escrow. Reescribe `STRONG_RESULT.md`
+según §G (quitar el reclamo fuerte, documentar el punto ciego, apuntar a la evitación real). No declares
+T9 cerrado hasta que ambos archivos reflejen lo que los tests realmente prueban."
+
+---
+
+## J. Referencias añadidas
+
+- V. Balegas, D. Serra, S. Duarte, C. Ferreira, M. Shapiro, R. Rodrigues, N. Preguiça — *Extending
+  Eventually Consistent Cloud Databases for Enforcing Numeric Invariants*, IEEE SRDS 2015. (Bounded Counter
+  CRDT: la evitación por presupuestos.)
+- P. E. O'Neil — *The Escrow Transactional Method*, ACM TODS 11(4), 1986. (Origen del escrow.)
+- (Contexto) Milano & Myers — *Predictive Treaties* (predicados particionables enforced localmente, con
+  dependencia del tiempo): generalización del reparto local; útil si el reach multi-invariante avanza.
+- (De addenda previos) Bailis et al. 2014 (I-confluence); Ghrist–Riess 2022 (Tarski); Hansen–Ghrist 2019
+  (Laplaciano de haces, base del ruteo); Shapiro et al. 2011 (CRDTs); Hellerstein–Alvaro (CALM).
diff --git a/src/escrow.rs b/src/escrow.rs
new file mode 100644
index 0000000..5dbc74f
--- /dev/null
+++ b/src/escrow.rs
@@ -0,0 +1,165 @@
+//! `escrow` — evitación de coordinación por presupuestos (T9, §B).
+//!
+//! Método de escrow (O'Neil 1986) como Bounded Counter CRDT (Balegas et al.,
+//! SRDS 2015). Para un invariante global `valor ≥ K`:
+//!
+//! 1. El *slack* `S = valor − K` es lo gastable sin romper `I`.
+//! 2. Se **reparte** `S` en presupuestos por réplica `b_i` con `Σ b_i ≤ S`.
+//! 3. Mientras `r_i` tenga presupuesto, **gasta localmente sin coordinar** — y es
+//!    correcto **incluso particionada**, porque `b_i` es suyo.
+//! 4. La única coordinación es el **rebalanceo edge-local** al agotar `b_i` (T9b).
+//!
+//! **El certificado.** Si `spent_i ≤ b_i` en cada réplica, entonces
+//! `valor = inicial − Σ spent_i ≥ inicial − Σ b_i ≥ inicial − S = K`, para **toda
+//! ejecución, orden y partición**. No se descubre tarde: se garantiza por
+//! construcción. Eso es evitación real, no la detección reactiva de T8 (§A).
+//!
+//! **Honestidad (§B):** escrow no vence a CALM; *transforma* la operación
+//! ("retirar sin límite" → "retirar dentro de presupuesto") para que sea
+//! I-confluente, al costo de un rebalanceo ocasional.
+
+use crate::invariant::GlobalInvariant;
+
+/// El resultado de intentar gastar localmente.
+#[derive(Debug, Clone, Copy, PartialEq, Eq)]
+pub enum SpendResult {
+    /// Dentro de presupuesto: gasto local, **cero coordinación**.
+    Local,
+    /// Presupuesto agotado: hace falta rebalanceo edge-local (T9b).
+    NeedsRebalance {
+        /// Cuánto falta para cubrir el gasto pedido.
+        deficit: i64,
+    },
+}
+
+/// El presupuesto repartido: la 0-cocadena `b` sobre las réplicas.
+#[derive(Debug, Clone, PartialEq, Eq)]
+pub struct Budget {
+    /// Presupuesto restante por réplica.
+    pub per_replica: Vec<i64>,
+}
+
+impl Budget {
+    /// Presupuesto a partir de un reparto explícito.
+    pub fn new(per_replica: Vec<i64>) -> Self {
+        Self { per_replica }
+    }
+
+    /// Reparte el `slack` en `n` presupuestos proporcionales a `weights`, con
+    /// división entera para garantizar `Σ b_i ≤ slack` (reparto siempre válido).
+    pub fn split(inv: &GlobalInvariant, weights: &[u64]) -> Self {
+        let s = inv.slack().max(0) as u128;
+        let total: u128 = weights.iter().map(|&w| w as u128).sum();
+        let per_replica = if total == 0 {
+            vec![0; weights.len()]
+        } else {
+            // ⌊w_i · S / total⌋ ⟹ la suma nunca excede S.
+            weights.iter().map(|&w| ((w as u128 * s) / total) as i64).collect()
+        };
+        Self { per_replica }
+    }
+
+    /// El certificado del reparto (§B): `Σ b_i ≤ slack` y todo `b_i ≥ 0`.
+    pub fn is_valid_split(&self, inv: &GlobalInvariant) -> bool {
+        self.per_replica.iter().all(|&b| b >= 0)
+            && self.per_replica.iter().sum::<i64>() <= inv.slack()
+    }
+
+    /// Presupuesto restante de la réplica `r`.
+    pub fn remaining(&self, r: usize) -> i64 {
+        self.per_replica[r]
+    }
+
+    /// Gasto local de `amount` (≥ 0) en la réplica `r`. Si cabe, descuenta y
+    /// devuelve `Local`; si no, **no gasta** y devuelve `NeedsRebalance` con el
+    /// déficit. Nunca declara "libre global" a ciegas.
+    pub fn try_spend(&mut self, r: usize, amount: i64) -> SpendResult {
+        debug_assert!(amount >= 0, "los gastos son no negativos");
+        if amount <= self.per_replica[r] {
+            self.per_replica[r] -= amount;
+            SpendResult::Local
+        } else {
+            SpendResult::NeedsRebalance {
+                deficit: amount - self.per_replica[r],
+            }
+        }
+    }
+
+    /// El valor del recurso implicado por unos gastos `spent_i` (para el
+    /// certificado): `inicial − Σ spent_i`.
+    pub fn value_after(inv: &GlobalInvariant, spent: &[i64]) -> i64 {
+        inv.initial - spent.iter().sum::<i64>()
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+    use crate::verdict::Verdict;
+    use proptest::prelude::*;
+
+    /// El caso 60/60 de T8, ahora bien tratado (§F): con presupuestos [50,50]
+    /// (reparto válido de S=100), una réplica **particionada** que intenta retirar
+    /// 60 recibe `NeedsRebalance`, NO `Local`. Muere el falso-verde del detector.
+    #[test]
+    fn t9_particionado_60_es_bloqueado_no_libre() {
+        let inv = GlobalInvariant::new(100, 0); // saldo ≥ 0, slack 100
+        let mut budget = Budget::new(vec![50, 50]);
+        assert!(budget.is_valid_split(&inv));
+
+        // La réplica 0, aislada, intenta retirar 60 (> su presupuesto de 50).
+        let res = budget.try_spend(0, 60);
+        assert_eq!(res, SpendResult::NeedsRebalance { deficit: 10 });
+        // El veredicto de escrow NO es "libre": pide rebalanceo (localizado).
+        assert!(matches!(Verdict::via_escrow(0, &res), Verdict::NeedsCoordination { .. }));
+        // Y no gastó: el presupuesto sigue intacto (el gasto queda pendiente).
+        assert_eq!(budget.remaining(0), 50);
+    }
+
+    /// Gasto dentro de presupuesto: local y descuenta.
+    #[test]
+    fn gasto_dentro_de_presupuesto_es_local() {
+        let mut budget = Budget::new(vec![50, 50]);
+        assert_eq!(budget.try_spend(0, 30), SpendResult::Local);
+        assert_eq!(budget.remaining(0), 20);
+        assert!(matches!(Verdict::via_escrow(0, &SpendResult::Local), Verdict::RunsFree));
+    }
+
+    fn split_valido(inv: &GlobalInvariant, raw: &[u64]) -> Budget {
+        let b = Budget::split(inv, raw);
+        assert!(b.is_valid_split(inv), "split debe ser válido por construcción");
+        b
+    }
+
+    proptest! {
+        /// **EL CERTIFICADO (§F, el corazón de T9a).** Para todo reparto válido y
+        /// TODA combinación de gastos dentro de presupuesto —incluidas particiones
+        /// arbitrarias y todas las réplicas gastando su máximo a la vez— el
+        /// invariante global `valor ≥ K` se preserva. Se cuantifica sobre todos
+        /// los estados alcanzables, no sobre un merge concreto.
+        #[test]
+        fn certificado_valor_nunca_baja_del_piso(
+            initial in 0i64..500,
+            floor in -100i64..100,
+            pesos in prop::collection::vec(0u64..50, 1..6),
+            gasto_raw in prop::collection::vec(0u64..600, 1..6),
+        ) {
+            prop_assume!(initial >= floor);              // slack ≥ 0
+            let inv = GlobalInvariant::new(initial, floor);
+            let budget = split_valido(&inv, &pesos);
+
+            // Gastos arbitrarios pero acotados por el presupuesto de cada réplica.
+            let spent: Vec<i64> = budget
+                .per_replica
+                .iter()
+                .zip(gasto_raw.iter().chain(std::iter::repeat(&0)))
+                .map(|(&b, &g)| (g as i64).min(b))       // spent_i ≤ b_i
+                .collect();
+
+            // El certificado: valor = inicial − Σ spent ≥ floor. Para cualquier
+            // subconjunto que sincronice (partición) el valor es aún mayor.
+            let valor = Budget::value_after(&inv, &spent);
+            prop_assert!(inv.holds(valor), "valor {} < piso {}", valor, inv.floor);
+        }
+    }
+}
diff --git a/src/invariant.rs b/src/invariant.rs
index 0cda191..332e7d3 100644
--- a/src/invariant.rs
+++ b/src/invariant.rs
@@ -9,13 +9,12 @@
 //! estado es un `GCounter` grow-only de retiros (merge = máximo por casilla). El
 //! invariante sobre un estado reconciliado `s` es `bound ≥ Σ retiros(s)`.
 //!
-//! **Veredicto honesto (§C):** reconcilia por el orden NATIVO (el merge del CRDT)
-//! y `corre libre ⟺ punto_fijo ∈ V`. Es un test de I-confluence **constructivo,
-//! sensible a la instancia y consciente de la topología**: el mismo programa da
-//! distinto veredicto según los valores concretos y según quién sincroniza con
-//! quién. (Riesgo R-T8b: `p ∈ V` es un predicado **añadido** sobre el punto fijo,
-//! no algo intrínseco al Laplaciano. La difusión calcula el *merge*; I-confluence
-//! es *merge + predicado de validez*.)
+//! **`AccountConfig` es un DETECTOR reactivo por-estado** (T8c): funde estados ya
+//! divergidos y comprueba el merge. T9 §A lo degrada de "consejero de
+//! coordinación" a alarma: tiene un **punto ciego** (una restricción global
+//! codificada por aristas desaparece al particionar el grafo — ver `COMPARISON.md`
+//! y el test `t9_punto_ciego...`). La **evitación** real vive en `escrow` sobre la
+//! restricción global `GlobalInvariant` de abajo, no aquí.
 
 use std::collections::{BTreeMap, BTreeSet};
 
@@ -25,6 +24,34 @@ use crate::nerve::ReplicaId;
 use crate::oracle::OracleVerdict;
 use crate::verdict::{Knot, Verdict};
 
+/// Una **restricción global** `valor ≥ floor` (T9 §D): incide sobre TODAS las
+/// réplicas que tocan el recurso, compartan arista o no. No es edge-local — ese
+/// fue el Error 2 de T8. El escrow reparte su `slack` en presupuestos por réplica.
+#[derive(Debug, Clone, Copy, PartialEq, Eq)]
+pub struct GlobalInvariant {
+    /// `K` en `valor ≥ K`.
+    pub floor: i64,
+    /// Valor inicial del recurso.
+    pub initial: i64,
+}
+
+impl GlobalInvariant {
+    /// Crea la restricción `valor ≥ floor` con valor inicial `initial`.
+    pub fn new(initial: i64, floor: i64) -> Self {
+        Self { floor, initial }
+    }
+
+    /// El *slack* `S = valor − K`: lo que se puede gastar sin romper `I`.
+    pub fn slack(&self) -> i64 {
+        self.initial - self.floor
+    }
+
+    /// ¿El valor dado satisface el invariante?
+    pub fn holds(&self, value: i64) -> bool {
+        value >= self.floor
+    }
+}
+
 /// Una instancia del programa "retiros sobre una cuenta con saldo ≥ 0".
 #[derive(Debug, Clone)]
 pub struct AccountConfig {
@@ -203,16 +230,20 @@ mod tests {
         }
     }
 
-    /// **La topología importa** (§F, el pitch de novedad): los MISMOS valores
-    /// (60 y 60 sobre 100) corren libres si las réplicas NO comparten (dos
-    /// componentes de 60) y coordinan si comparten (una de 120). I-confluence
-    /// sobre el grafo real, no sobre un par abstracto.
+    /// **El PUNTO CIEGO del detector** (T9 §A, Error 2). Lo que T8c celebraba como
+    /// "la topología importa" es en realidad un falso-verde peligroso: con los
+    /// mismos retiros 60/60 sobre 100, el detector dice `libre` al **particionar**
+    /// —el caso MÁS peligroso— porque, sin arista, no ve el acoplamiento del
+    /// invariante GLOBAL. No es que sea seguro; es que el haz está ciego. La cura
+    /// (escrow) bloquea correctamente ese caso: ver `escrow::tests` y `COMPARISON.md`.
     #[test]
-    fn el_mismo_valor_depende_del_grafo() {
+    fn t9_punto_ciego_del_detector_particionado() {
         let desconectado = AccountConfig::new("particion", 100, vec![60, 60], vec![]);
         let conectado = AccountConfig::new("conjunto", 100, vec![60, 60], vec![(0, 1)]);
-        assert_eq!(desconectado.haz_coordination(), OracleVerdict::CoordinationFree);
+        // Conectado detecta el sobregiro...
         assert_eq!(conectado.haz_coordination(), OracleVerdict::NeedsCoordination);
+        // ...pero particionado lo declara "libre": ESO es el bug que motiva T9.
+        assert_eq!(desconectado.haz_coordination(), OracleVerdict::CoordinationFree);
     }
 
     /// Barrido determinista que **caza** discrepancias buenas: hay muchas, no una
diff --git a/src/lib.rs b/src/lib.rs
index ffd33f9..092401d 100644
--- a/src/lib.rs
+++ b/src/lib.rs
@@ -14,6 +14,7 @@
 pub mod cell;
 pub mod cohomology;
 pub mod error;
+pub mod escrow;
 pub mod gf2;
 pub mod invariant;
 pub mod lattice;
diff --git a/src/verdict.rs b/src/verdict.rs
index df33133..0c64eb9 100644
--- a/src/verdict.rs
+++ b/src/verdict.rs
@@ -6,6 +6,7 @@ use std::collections::BTreeSet;
 use std::fmt;
 
 use crate::cohomology::Cohomology;
+use crate::escrow::SpendResult;
 use crate::lattice::{GaloisRestriction, LatticeCell};
 use crate::nerve::ReplicaId;
 use crate::sheaf::Sheaf;
@@ -121,6 +122,23 @@ impl Verdict {
             }
         }
     }
+
+    /// Veredicto por **escrow** (T9, §D/§E): un gasto dentro de presupuesto es
+    /// `Local` → `RunsFree` (cero coordinación, correcto **incluso particionado**);
+    /// agotarlo pide un **rebalanceo edge-local** → `NeedsCoordination` localizado
+    /// en la réplica seca. NUNCA declara "libre global" a ciegas (mata el punto
+    /// ciego de T8). Las aristas del rebalanceo las rellena el `BudgetRouter` (T9b).
+    pub fn via_escrow(replica: usize, spend: &SpendResult) -> Verdict {
+        match spend {
+            SpendResult::Local => Verdict::RunsFree,
+            SpendResult::NeedsRebalance { .. } => Verdict::NeedsCoordination {
+                knots: vec![Knot {
+                    replicas: vec![ReplicaId(replica)],
+                    edges: Vec::new(),
+                }],
+            },
+        }
+    }
 }
 
 impl fmt::Display for Verdict {