tawasuyu/hifas

T8 §C-§F: la coordinación real no vive en el tipo de dato sino en un
INVARIANTE que la fusión no preserva. Modelo canónico de Bailis (saldo ≥ 0).
- invariant::AccountConfig: bound + retiros por réplica + grafo. Estado =
  GCounter grow-only de retiros; V = {s : bound ≥ Σ retiros}.
- haz_verdict (§C): reconcilia por el orden nativo y corre libre ⟺ punto
  fijo ∈ V, con localización de réplicas/aristas culpables.
- i_confluence_oracle: oráculo independiente (suma por componente vía
  union-find), camino distinto de la difusión.
- calm_syntactic: condena el retiro por-programa (a batir).

VERSIÓN FUERTE PROBADA (STRONG_RESULT.md): testigo A (retiros [10,10] sobre
100) → haz=libre / CALM-sintáctico=coordina con I preservado. Barrido halla
>100 testigos. proptest: haz == I-confluence en toda instancia (corrección);
haz nunca miente (soundness). La topología importa: mismos 60/60 corren
libres particionados y coordinan conectados.

Honestidad §F: el booleano ES I-confluence (Bailis 2014), no más allá de
CALM; la novedad es el cómo (topología-consciente, difusión a punto fijo) y
la propina (estado reconciliado + nudo). M4 desbloqueado. main muestra el
testigo. 46 tests, clippy limpio.

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

diff --git a/STRONG_RESULT.md b/STRONG_RESULT.md
new file mode 100644
index 0000000..88520ec
--- /dev/null
+++ b/STRONG_RESULT.md
@@ -0,0 +1,75 @@
+# STRONG_RESULT — ¿el haz supera a CALM, o lo espeja? (T8c)
+
+**Conclusión: VERSIÓN FUERTE PROBADA.** El haz da un veredicto estrictamente más
+fino que el CALM **sintáctico por-programa**, y lo hace por un camino honesto,
+sensible a la instancia y consciente de la topología. Con la salvedad de §F: ese
+veredicto booleano **es** I-confluence (Bailis et al. VLDB 2014) — no algo más
+allá de CALM, sino su refinamiento por-instancia, calculado sobre el grafo real.
+
+## El testigo
+
+Reproducible en `invariant::tests::discrepancia_buena_existe`.
+
+| | Instancia A (el premio) |
+|---|---|
+| Programa | dos réplicas retiran de una cuenta con saldo ≥ 0 |
+| Saldo inicial | `bound = 100` |
+| Retiros | `[10, 10]` (concurrentes) |
+| Grafo | `0 — 1` (comparten) |
+| Merge | `Σ retiros = 20 ≤ 100` ⟹ el invariante sobrevive |
+| **Haz (difusión + `∈ V`)** | **corre libre** |
+| **CALM sintáctico** | **coordina** (el retiro es no monótono en valor) |
+| I-confluence (oráculo indep.) | corre libre |
+
+`haz = libre` mientras `CALM-sintáctico = coordina`, con `I` preservado. Eso es la
+discrepancia buena de §D. Y no es una casualidad: el barrido
+`la_caza_encuentra_muchas_discrepancias` halla >100 testigos solo con dos réplicas
+sobre una cuenta de 100.
+
+## Por qué NO es circular (a diferencia de T5–T7)
+
+1. **El orden sale del merge, no de la etiqueta** (T8a): `a ≤ b := merge(a,b)==b`.
+   El haz nunca lee monótono/reset.
+2. **La coordinación sale del invariante, no del tipo de dato** (T8c): sin `I`
+   todo CRDT corre libre (T8a/b); la obstrucción aparece solo cuando el merge
+   empuja fuera de `V = {s : I(s)}`.
+3. **Dos caminos independientes coinciden** (`haz_iguala_i_confluence`): la
+   difusión de merges y la suma aritmética por componente dan el mismo booleano en
+   toda instancia. Corrección, no definición circular.
+4. **Soundness verificada** (`soundness_el_haz_nunca_miente`): el haz jamás dice
+   "libre" con el invariante violado.
+
+## Qué es novedad y qué no (honestidad §F)
+
+- **NO es novedad el sí/no.** El veredicto booleano de la versión fuerte **es**
+  I-confluence (Bailis 2014). Hay incluso una línea "Complete CALM" que muestra
+  `I-confluente ⟺ monótono` bajo el orden dado por la validez del invariante: CALM,
+  I-confluence y esta difusión son la misma moneda con tres órdenes distintos.
+  Reclamar "más preciso que CALM" a secas sería medio cierto: somos más precisos
+  que **CALM sintáctico por-programa**, que es justo lo que I-confluence ya hace.
+- **SÍ es el pitch defendible el *cómo* y la *propina*:** I-confluence sobre el
+  **grafo de comunicación real** (topología-consciente, no un par de estados
+  abstractos: ver `el_mismo_valor_depende_del_grafo` — los mismos retiros 60/60
+  corren libres particionados y coordinan conectados), vía **difusión a punto
+  fijo** que además entrega (a) el **estado reconciliado** y (b) la **localización**
+  de las réplicas/aristas culpables. Un test de I-confluence estándar da un
+  booleano; aquí te llevas el booleano, el merge y el nudo.
+
+## Riesgo aceptado (R-T8b)
+
+El predicado `p ∈ V` es un chequeo **añadido** sobre el punto fijo, no algo
+intrínseco al Laplaciano. No vendemos "la cohomología detecta la violación del
+invariante": la difusión calcula el *merge*; I-confluence es *merge + predicado de
+validez*. Y (R-T8c) el veredicto es por-configuración, no precomputable por
+programa — es la fuente de la precisión y un costo a reevaluar por estado en M4.
+
+## Veredicto final del proyecto
+
+- El MVP lineal medía **topología** (`H¹ = β₁`); útil como detector barato, pero
+  falso-positivo en ciclos.
+- T5–T7 (retículos + Tarski) parecía cerrar la brecha, pero era **circular**:
+  leía la etiqueta (`FLIPS.md`).
+- T8 rederiva todo del merge y ancla la coordinación en un **invariante**. El
+  resultado honesto es un **test de I-confluence constructivo, localizado y
+  consciente de la topología**. Esa es la contribución real y defendible; el
+  camino a M4 (adaptador a sistemas soberanos) queda desbloqueado sobre esta base.
diff --git a/src/invariant.rs b/src/invariant.rs
new file mode 100644
index 0000000..0cda191
--- /dev/null
+++ b/src/invariant.rs
@@ -0,0 +1,264 @@
+//! `invariant` — coordinación de verdad: I-confluence sobre el grafo (T8c, §C–§F).
+//!
+//! Sin invariante, un CRDT nunca coordina (T8a/b). La coordinación aparece cuando
+//! hay un **invariante global `I`** que la fusión no preserva: los estados válidos
+//! `V = {s : I(s)}` no son cerrados bajo join. Ejemplo canónico (Bailis et al.,
+//! VLDB 2014): **saldo ≥ 0**.
+//!
+//! Modelo: `bound` = saldo inicial; cada réplica `i` retira `withdrawals[i]`. El
+//! 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*.)
+
+use std::collections::{BTreeMap, BTreeSet};
+
+use crate::cell::GCounter;
+use crate::native;
+use crate::nerve::ReplicaId;
+use crate::oracle::OracleVerdict;
+use crate::verdict::{Knot, Verdict};
+
+/// Una instancia del programa "retiros sobre una cuenta con saldo ≥ 0".
+#[derive(Debug, Clone)]
+pub struct AccountConfig {
+    /// Nombre del caso.
+    pub name: String,
+    /// Número de réplicas.
+    pub replicas: usize,
+    /// Saldo inicial `B₀` (la cota del invariante).
+    pub bound: u64,
+    /// Retiro concurrente de cada réplica.
+    pub withdrawals: Vec<u64>,
+    /// Grafo de compartición (quién reconcilia con quién).
+    pub edges: Vec<(usize, usize)>,
+}
+
+impl AccountConfig {
+    /// Construye una instancia (con `withdrawals.len() == replicas`).
+    pub fn new(
+        name: impl Into<String>,
+        bound: u64,
+        withdrawals: Vec<u64>,
+        edges: Vec<(usize, usize)>,
+    ) -> Self {
+        Self {
+            name: name.into(),
+            replicas: withdrawals.len(),
+            bound,
+            withdrawals,
+            edges,
+        }
+    }
+
+    /// Estado local de cada réplica: un `GCounter` con su propia casilla puesta a
+    /// su retiro (grow-only; solo incrementa lo suyo).
+    fn seeds(&self) -> Vec<GCounter> {
+        (0..self.replicas)
+            .map(|i| {
+                let mut slots = vec![0u64; self.replicas];
+                slots[i] = self.withdrawals[i];
+                GCounter { slots }
+            })
+            .collect()
+    }
+
+    /// Estado reconciliado por el orden nativo (merge por componente conexa).
+    pub fn reconcile(&self) -> Vec<GCounter> {
+        native::reconcile(&self.edges, &self.seeds())
+    }
+
+    /// Componentes conexas del grafo (union-find). Camino independiente del merge.
+    fn components(&self) -> Vec<usize> {
+        let mut parent: Vec<usize> = (0..self.replicas).collect();
+        fn find(parent: &mut [usize], x: usize) -> usize {
+            let mut r = x;
+            while parent[r] != r {
+                r = parent[r];
+            }
+            r
+        }
+        for &(a, b) in &self.edges {
+            let ra = find(&mut parent, a);
+            let rb = find(&mut parent, b);
+            if ra != rb {
+                parent[ra] = rb;
+            }
+        }
+        (0..self.replicas).map(|i| find(&mut parent, i)).collect()
+    }
+
+    /// **Veredicto del haz (§C):** difunde al punto fijo y comprueba `∈ V`. Corre
+    /// libre si ninguna componente reconciliada sobregira; si alguna lo hace,
+    /// localiza las réplicas culpables (las que retiraron) y sus aristas.
+    pub fn haz_verdict(&self) -> Verdict {
+        let fixpoint = self.reconcile();
+
+        // Vértices cuyo estado reconciliado viola el invariante (sobregiro).
+        let mut malos = BTreeSet::new();
+        for (v, state) in fixpoint.iter().enumerate() {
+            if self.bound < state.value() {
+                malos.insert(v);
+            }
+        }
+
+        if malos.is_empty() {
+            return Verdict::RunsFree;
+        }
+
+        let replicas: Vec<ReplicaId> = malos
+            .iter()
+            .filter(|&&v| self.withdrawals[v] > 0)
+            .map(|&v| ReplicaId(v))
+            .collect();
+        let edges: Vec<usize> = self
+            .edges
+            .iter()
+            .enumerate()
+            .filter(|(_, &(a, b))| malos.contains(&a) || malos.contains(&b))
+            .map(|(i, _)| i)
+            .collect();
+
+        Verdict::NeedsCoordination {
+            knots: vec![Knot { replicas, edges }],
+        }
+    }
+
+    /// El veredicto del haz como `OracleVerdict` (para comparar).
+    pub fn haz_coordination(&self) -> OracleVerdict {
+        match self.haz_verdict() {
+            Verdict::RunsFree => OracleVerdict::CoordinationFree,
+            Verdict::NeedsCoordination { .. } => OracleVerdict::NeedsCoordination,
+        }
+    }
+
+    /// **CALM sintáctico por-programa:** el retiro es una operación no monótona
+    /// (decrementa el saldo), así que el check crudo condena el programa entero,
+    /// sin mirar valores → siempre `coordina`. Es la respuesta a batir (§D).
+    pub fn calm_syntactic(&self) -> OracleVerdict {
+        OracleVerdict::NeedsCoordination
+    }
+
+    /// **Oráculo de I-confluence independiente** (§D): por un camino que NO usa la
+    /// difusión — suma aritmética de los retiros por componente vía union-find — y
+    /// comprueba `Σ ≤ bound`. El haz debe igualarlo en toda instancia (corrección
+    /// y soundness §E.2).
+    pub fn i_confluence_oracle(&self) -> OracleVerdict {
+        let comp = self.components();
+        let mut sums: BTreeMap<usize, u64> = BTreeMap::new();
+        for (&c, &w) in comp.iter().zip(&self.withdrawals) {
+            *sums.entry(c).or_default() += w;
+        }
+        if sums.values().all(|&s| s <= self.bound) {
+            OracleVerdict::CoordinationFree
+        } else {
+            OracleVerdict::NeedsCoordination
+        }
+    }
+
+    /// ¿Es una **discrepancia buena** (versión fuerte, §D instancia A)? El haz
+    /// corre libre mientras el CALM sintáctico coordina — con `I` preservado.
+    pub fn es_discrepancia_buena(&self) -> bool {
+        self.haz_coordination() == OracleVerdict::CoordinationFree
+            && self.calm_syntactic() == OracleVerdict::NeedsCoordination
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+    use proptest::prelude::*;
+
+    /// **El premio (§D, instancia A):** dos réplicas retiran 10 cada una de una
+    /// cuenta de 100. Los valores caben (20 ≤ 100) → el haz corre libre. Pero el
+    /// retiro es no monótono → CALM sintáctico coordina. Discrepancia buena: el
+    /// haz es más fino que el check por-programa. Testigo para `STRONG_RESULT.md`.
+    #[test]
+    fn discrepancia_buena_existe() {
+        let a = AccountConfig::new("retiros-que-caben", 100, vec![10, 10], vec![(0, 1)]);
+        assert_eq!(a.haz_coordination(), OracleVerdict::CoordinationFree);
+        assert_eq!(a.calm_syntactic(), OracleVerdict::NeedsCoordination);
+        assert_eq!(a.i_confluence_oracle(), OracleVerdict::CoordinationFree);
+        assert!(a.es_discrepancia_buena());
+    }
+
+    /// Instancia B: los retiros sobregiran (60 + 60 > 100) → el haz coordina, y
+    /// coincide con I-confluence. Además localiza a las dos réplicas culpables.
+    #[test]
+    fn sobregiro_coordina_y_localiza() {
+        let a = AccountConfig::new("retiros-que-sobregiran", 100, vec![60, 60], vec![(0, 1)]);
+        assert_eq!(a.haz_coordination(), OracleVerdict::NeedsCoordination);
+        assert_eq!(a.i_confluence_oracle(), OracleVerdict::NeedsCoordination);
+        match a.haz_verdict() {
+            Verdict::NeedsCoordination { knots } => {
+                assert_eq!(knots[0].replicas, vec![ReplicaId(0), ReplicaId(1)]);
+            }
+            Verdict::RunsFree => panic!("debería coordinar"),
+        }
+    }
+
+    /// **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.
+    #[test]
+    fn el_mismo_valor_depende_del_grafo() {
+        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);
+        assert_eq!(conectado.haz_coordination(), OracleVerdict::NeedsCoordination);
+    }
+
+    /// Barrido determinista que **caza** discrepancias buenas: hay muchas, no una
+    /// casualidad. Prueba de que la versión fuerte es robusta.
+    #[test]
+    fn la_caza_encuentra_muchas_discrepancias() {
+        let mut encontradas = 0;
+        for total in 0..=90u64 {
+            for w0 in 0..=total {
+                let a = AccountConfig::new("barrido", 100, vec![w0, total - w0], vec![(0, 1)]);
+                if a.es_discrepancia_buena() {
+                    encontradas += 1;
+                }
+            }
+        }
+        assert!(encontradas > 100, "la discrepancia buena es robusta: {encontradas}");
+    }
+
+    fn instancia() -> impl Strategy<Value = AccountConfig> {
+        (2usize..=5, 1u64..=50).prop_flat_map(|(n, bound)| {
+            let ws = prop::collection::vec(0u64..=40, n);
+            let arista = (0..n, 0..n).prop_filter("sin lazos", |(a, b)| a != b);
+            let es = prop::collection::vec(arista, 0..8);
+            (Just(bound), ws, es)
+                .prop_map(|(bound, ws, es)| AccountConfig::new("prop", bound, ws, es))
+        })
+    }
+
+    proptest! {
+        /// **Corrección (§D):** el haz iguala al oráculo de I-confluence en TODA
+        /// instancia. Dos caminos independientes (difusión de merges vs suma por
+        /// componente) que coinciden siempre.
+        #[test]
+        fn haz_iguala_i_confluence(a in instancia()) {
+            prop_assert_eq!(a.haz_coordination(), a.i_confluence_oracle());
+        }
+
+        /// **Soundness (§E.2, no se negocia):** el haz NUNCA dice "corre libre"
+        /// cuando alguna componente reconciliada viola el invariante.
+        #[test]
+        fn soundness_el_haz_nunca_miente(a in instancia()) {
+            if a.haz_coordination() == OracleVerdict::CoordinationFree {
+                for state in a.reconcile() {
+                    prop_assert!(a.bound >= state.value(), "libre ⟹ invariante preservado");
+                }
+            }
+        }
+    }
+}
diff --git a/src/lib.rs b/src/lib.rs
index a13f057..ffd33f9 100644
--- a/src/lib.rs
+++ b/src/lib.rs
@@ -15,6 +15,7 @@ pub mod cell;
 pub mod cohomology;
 pub mod error;
 pub mod gf2;
+pub mod invariant;
 pub mod lattice;
 pub mod linalg;
 pub mod native;
diff --git a/src/main.rs b/src/main.rs
index 3c7da62..f474816 100644
--- a/src/main.rs
+++ b/src/main.rs
@@ -8,6 +8,7 @@
 
 use sheafsync::cell::{Cell, GCounter, ResettableRegister};
 use sheafsync::cohomology::{self, Cohomology};
+use sheafsync::invariant::AccountConfig;
 use sheafsync::oracle::{Config, Share};
 use sheafsync::sheaf::Sheaf;
 use sheafsync::verdict::Verdict;
@@ -19,6 +20,8 @@ fn main() {
     corrida_b();
     println!();
     contraste_tarski();
+    println!();
+    contraste_invariante();
 }
 
 /// Imprime el veredicto de un haz ya construido.
@@ -117,3 +120,27 @@ fn contraste_tarski() {
         triangulo.tarski_verdict()
     );
 }
+
+/// La discrepancia buena (T8c, §D): donde de verdad se supera al CALM sintáctico.
+///
+/// Dos réplicas retiran 10 de una cuenta de 100 (invariante: saldo ≥ 0). Los
+/// valores caben → el haz (I-confluence sobre el grafo) corre libre; el CALM
+/// sintáctico condena el retiro por-programa. Análisis sensible a la instancia.
+fn contraste_invariante() {
+    println!("Discrepancia buena — retiros que caben (saldo ≥ 0, cuenta de 100)");
+
+    let caben = AccountConfig::new("retiros-que-caben", 100, vec![10, 10], vec![(0, 1)]);
+    let sobregiran = AccountConfig::new("sobregiran", 100, vec![60, 60], vec![(0, 1)]);
+
+    println!("  A) retiros [10,10] → Σ=20 ≤ 100:");
+    println!("     CALM sintáctico: {:?}  (condena el retiro)", caben.calm_syntactic());
+    println!(
+        "     haz (I-confluence): {:?}   ← corre libre: los valores pegan",
+        caben.haz_coordination()
+    );
+    println!("  B) retiros [60,60] → Σ=120 > 100:");
+    println!(
+        "     haz (I-confluence): {:?}   ← coordina: el merge rompe el invariante",
+        sobregiran.haz_coordination()
+    );
+}