tawasuyu/hifas

Addendum §D/T5, aditivo — no toca el motor lineal:
- lattice::LatticeCell (join/meet/bottom/top) y GaloisRestriction
  (lower/upper adjuntos, ley lower(a)≤b ⟺ a≤upper(b)).
- Encodings §D.1: Nat (casilla GCounter, cadena ℕ con ⊤=∞) y ResetVal
  (ResettableRegister; post-reset incomparable → join de generaciones
  distintas colapsa a ⊤, meet a ⊥: la obstrucción semántica de §C).
- IdentityGalois y ScaleGalois (adjunción k·a≤b ⟺ a≤⌊b/k⌋).
- proptest: leyes de retículo (conmut/asoc/idemp/absorción/neutros) para
  Nat y ResetVal, colapso de incomparables, ley adjunta de Galois y
  monotonía de lower.

ADDENDUM.md incorporado (antes addendumsdd.txt). 29 tests, clippy limpio.

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

diff --git a/ADDENDUM.md b/ADDENDUM.md
new file mode 100644
index 0000000..970c10b
--- /dev/null
+++ b/ADDENDUM.md
@@ -0,0 +1,220 @@
+# SDD — Addendum: Pista de retículos (Tarski)
+
+**Extiende:** `DESIGN.md` (SDD v1) — este documento añade el hito `M-research` y los tickets `T5`–`T7`.
+**Estado:** Diseño — habilitado por el hallazgo del cierre de M3.
+**Precondición:** MVP cerrado (M0–M3, objetivos G1–G6). Batería del oráculo verde. `DISCREPANCIES.md` existe.
+**Última edición:** 2026-07-01
+
+---
+
+## A. Por qué existe esta pista (el hallazgo de M3, en una línea)
+
+El motor lineal del MVP, en el régimen monótono, **no mide consistencia: mide la topología del grafo.**
+Su codificación colapsa al haz constante, cuya cohomología es `dim H¹ = β₁` (§7.2). Consecuencia probada:
+`H¹ = 0 ⟺ grafo acíclico`. Sobre grafos cíclicos con datos monótonos pide coordinación de más
+(triángulo-monótono, cuadrado-monótono en `DISCREPANCIES.md`).
+
+Causa raíz, con nombre: **la resta del coboundary.** `(δx)_e = R·x_u − R·x_v` exige un menos.
+Un join-semilattice no tiene inversos; al linealizarlo, el δ mide *desacuerdo-XOR* en vez de
+*compatibilidad-por-join*, e inventa obstrucciones-fantasma alrededor de los ciclos. Por eso el fallo
+es conservador y nunca inverso (consistente con §2.2 / R1).
+
+**El objetivo de esta pista es eliminar la resta.** No parchear el motor lineal, sino sustituir su
+núcleo por una teoría que reconcilie datos de retículo sin restar.
+
+---
+
+## B. El giro matemático
+
+De vectores a retículos; de `rank` a punto fijo.
+
+| MVP lineal (§7) | Pista de retículos |
+|---|---|
+| Stalks = espacios vectoriales | Stalks = retículos (u order-lattices) |
+| Restricciones = matrices lineales | Restricciones = mapas join-preserving (conexiones de Galois) |
+| Coboundary `δ` con resta | Laplaciano de Tarski `L` (sin resta) |
+| Veredicto = `dim H¹` (¿cokernel = 0?) | Veredicto = ¿la difusión llega a un punto fijo consistente? |
+| Se calcula con eliminación gaussiana | Se calcula iterando `L` a punto fijo (Kleene/Tarski) |
+
+**Andamiaje (real, verificado):** Ghrist & Riess, *Cellular Sheaves of Lattices and the Tarski
+Laplacian*, Homology, Homotopy and Applications 24(1):325–345 (2022); arXiv:2007.04099.
+Inicia una teoría de Hodge discreta para haces celulares valuados en retículos y conexiones de Galois.
+La pieza central, el **Laplaciano de Tarski** `L`, es un endomorfismo del complejo de cocadenas cuyos
+**puntos fijos** dan una cohomología que **coincide con las secciones globales en grado cero**. La
+convergencia la garantiza el teorema de punto fijo de Tarski; para stalks finitas o de rango finito,
+converge en tiempo finito (cotas por la altura del retículo).
+
+Forma del operador (implementar según Def. 2 / Lemma 7 del paper, no reinventar la fórmula):
+`L` se descompone en dos partes que se combinan tomando **meet** sobre las aristas incidentes:
+- **expansión**: `F_{v⊴e}^* ∘ F_{v⊴e}` aplicado al estado local (≥ id: nunca pierde información propia);
+- **mezcla**: trae el estado del vecino `w` a la arista vía `F_{w⊴e}` y lo devuelve a `v` vía la
+  adjunta de Galois `F_{v⊴e}^*`.
+
+La difusión propaga información por los mapas de restricción; su punto fijo es la mejor reconciliación
+globalmente coherente.
+
+---
+
+## C. Qué significa "obstrucción" ahora (y la honestidad que toca)
+
+**Perdemos el `H¹` limpio.** En el mundo de retículos no hay cokernel: sin resta, no hay álgebra lineal.
+La teoría de cohomología superior para haces de retículos es terreno abierto — la propia línea de Ghrist–
+Riess prioriza las *aplicaciones del Laplaciano* (grado 0, secciones globales) por encima de un `H¹`
+cerrado. No prometemos un número de obstrucción; construimos un **diagnóstico dinámico.**
+
+El veredicto pasa de algebraico a dinámico:
+
+1. Siembra cada vértice con su estado local.
+2. Itera la difusión de Tarski hasta el punto fijo (harmónico).
+3. **Corre libre** si el punto fijo es una sección global genuina que *preserva* la información local
+   de cada réplica (cada estado local ≤ / compatible con el valor harmónico). Para CRDTs monótonos
+   alrededor de un ciclo, el punto fijo es exactamente el **join** de los estados → reconcilia sin
+   colapso → sin obstrucción.
+4. **Coordina** si la reconciliación no puede sostener los estados locales sin colapsar (p.ej. la
+   difusión fuerza el tope `⊤`, señal de que no existe refinamiento común no trivial). Un `reset`
+   no monótono produce estados incompatibles → colapso → obstrucción real.
+
+**Localización (abierto, R-L1).** En el MVP la base del cokernel señalaba las aristas del nudo. Aquí la
+localización es menos crisp: se toma como las aristas cuyo desacuerdo de restricción *sobrevive* al punto
+fijo. Es aproximación, no teorema. Empezar por ahí; refinar es investigación.
+
+---
+
+## D. Modelo de tipos (bocetos)
+
+Conviven con los tipos del MVP; no los reemplazan (el motor lineal sigue como oráculo topológico barato).
+
+```rust
+/// 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).
diff --git a/src/lattice.rs b/src/lattice.rs
new file mode 100644
index 0000000..ef2401c
--- /dev/null
+++ b/src/lattice.rs
@@ -0,0 +1,262 @@
+//! `lattice` — estados de retículo y restricciones de Galois (Addendum §D, T5).
+//!
+//! La pista de retículos (Ghrist–Riess 2022): reemplaza los espacios vectoriales
+//! del MVP por **retículos** y las matrices por **conexiones de Galois**. No toca
+//! el motor lineal (`cohomology`), que sigue como oráculo topológico barato.
+//!
+//! Aquí viven las piezas de grado 0: los tipos de retículo (`Nat`, `ResetVal`) y
+//! la interfaz de restricción adjunta (`GaloisRestriction`). El Laplaciano de
+//! Tarski que las difunde a punto fijo llega en T6 (`tarski`).
+
+use std::cmp::Ordering;
+
+/// Un estado local con estructura de retículo acotado (Addendum §D).
+///
+/// `join` (∨) y `meet` (∧) deben ser asociativos, conmutativos, idempotentes y
+/// cumplir absorción; `bottom` (⊥) y `top` (⊤) son sus neutros/absorbentes.
+pub trait LatticeCell: Clone + PartialOrd {
+    /// Supremo ∨ (least upper bound).
+    fn join(&self, other: &Self) -> Self;
+    /// Ínfimo ∧ (greatest lower bound).
+    fn meet(&self, other: &Self) -> Self;
+    /// Elemento mínimo ⊥.
+    fn bottom() -> Self;
+    /// Elemento máximo ⊤.
+    fn top() -> Self;
+}
+
+/// Una casilla de `GCounter` como cadena ℕ con ⊤ = ∞ (Addendum §D.1).
+///
+/// Join = máximo, meet = mínimo. Monótono por construcción: nunca resta. El
+/// `GCounter` completo es el **producto** de estas cadenas (se arma en la stalk
+/// del haz de retículos en T6).
+#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord)]
+pub struct Nat(pub u64);
+
+impl Nat {
+    /// Representación de ∞ (el ⊤ de la cadena).
+    pub const INF: Nat = Nat(u64::MAX);
+}
+
+impl LatticeCell for Nat {
+    fn join(&self, other: &Self) -> Self {
+        Nat(self.0.max(other.0))
+    }
+    fn meet(&self, other: &Self) -> Self {
+        Nat(self.0.min(other.0))
+    }
+    fn bottom() -> Self {
+        Nat(0)
+    }
+    fn top() -> Self {
+        Nat::INF
+    }
+}
+
+/// Un `ResettableRegister` como retículo donde el post-reset es **incomparable**
+/// al pre-reset (Addendum §D.1). Dos generaciones distintas no tienen refinamiento
+/// común no trivial: su join colapsa a ⊤ y su meet a ⊥. Ese colapso a ⊤ es la
+/// señal de obstrucción **real** (semántica, no topológica) de la §C.
+#[derive(Debug, Clone, PartialEq, Eq)]
+pub enum ResetVal {
+    /// ⊥.
+    Bottom,
+    /// Un valor concreto en una generación. Comparable solo dentro de su generación.
+    Gen { generation: u64, value: i64 },
+    /// ⊤ (colapso: no hay reconciliación no trivial).
+    Top,
+}
+
+impl PartialOrd for ResetVal {
+    fn partial_cmp(&self, other: &Self) -> Option<Ordering> {
+        use ResetVal::*;
+        match (self, other) {
+            (Bottom, Bottom) | (Top, Top) => Some(Ordering::Equal),
+            (Bottom, _) | (_, Top) => Some(Ordering::Less),
+            (_, Bottom) | (Top, _) => Some(Ordering::Greater),
+            (
+                Gen { generation: g1, value: v1 },
+                Gen { generation: g2, value: v2 },
+            ) => {
+                if g1 == g2 {
+                    Some(v1.cmp(v2))
+                } else {
+                    None // generaciones distintas: incomparables
+                }
+            }
+        }
+    }
+}
+
+impl LatticeCell for ResetVal {
+    fn join(&self, other: &Self) -> Self {
+        use ResetVal::*;
+        match (self, other) {
+            (Bottom, x) | (x, Bottom) => x.clone(),
+            (Top, _) | (_, Top) => Top,
+            (
+                Gen { generation: g1, value: v1 },
+                Gen { generation: g2, value: v2 },
+            ) => {
+                if g1 == g2 {
+                    Gen { generation: *g1, value: *v1.max(v2) }
+                } else {
+                    Top // incomparables → colapso
+                }
+            }
+        }
+    }
+
+    fn meet(&self, other: &Self) -> Self {
+        use ResetVal::*;
+        match (self, other) {
+            (Top, x) | (x, Top) => x.clone(),
+            (Bottom, _) | (_, Bottom) => Bottom,
+            (
+                Gen { generation: g1, value: v1 },
+                Gen { generation: g2, value: v2 },
+            ) => {
+                if g1 == g2 {
+                    Gen { generation: *g1, value: *v1.min(v2) }
+                } else {
+                    Bottom
+                }
+            }
+        }
+    }
+
+    fn bottom() -> Self {
+        ResetVal::Bottom
+    }
+    fn top() -> Self {
+        ResetVal::Top
+    }
+}
+
+/// Un mapa de restricción como **conexión de Galois** (Addendum §D): un par
+/// adjunto `(lower, upper)` que reemplaza a la matriz lineal del MVP.
+///
+/// Ley adjunta (monótona): `lower(a) ≤ b  ⟺  a ≤ upper(b)`. De ella se siguen
+/// que `lower` preserva joins y `upper` preserva meets, sin necesidad de restar.
+pub trait GaloisRestriction<A: LatticeCell, B: LatticeCell> {
+    /// `F_{v⊴e}`: sube el estado local a la arista. Preserva joins.
+    fn lower(&self, a: &A) -> B;
+    /// `F_{v⊴e}^*`: la adjunta; baja de la arista al vértice. Preserva meets.
+    fn upper(&self, b: &B) -> A;
+}
+
+/// La conexión de Galois identidad: comparten el mismo dato tal cual.
+#[derive(Debug, Clone, Copy, Default)]
+pub struct IdentityGalois;
+
+impl<L: LatticeCell> GaloisRestriction<L, L> for IdentityGalois {
+    fn lower(&self, a: &L) -> L {
+        a.clone()
+    }
+    fn upper(&self, b: &L) -> L {
+        b.clone()
+    }
+}
+
+/// Conexión de Galois no trivial sobre ℕ: `lower(a) = k·a`, `upper(b) = ⌊b/k⌋`.
+/// Es la adjunción clásica multiplicación/división: `k·a ≤ b ⟺ a ≤ ⌊b/k⌋`.
+#[derive(Debug, Clone, Copy)]
+pub struct ScaleGalois {
+    /// Factor de escala, `k ≥ 1`.
+    pub k: u64,
+}
+
+impl ScaleGalois {
+    /// Crea una escala con `k ≥ 1` (satura en 1 si se pasa 0).
+    pub fn new(k: u64) -> Self {
+        Self { k: k.max(1) }
+    }
+}
+
+impl GaloisRestriction<Nat, Nat> for ScaleGalois {
+    fn lower(&self, a: &Nat) -> Nat {
+        Nat(a.0.saturating_mul(self.k))
+    }
+    fn upper(&self, b: &Nat) -> Nat {
+        Nat(b.0 / self.k)
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+    use proptest::prelude::*;
+
+    /// Comprueba las cuatro leyes de retículo sobre una terna concreta.
+    fn leyes_de_reticulo<L: LatticeCell + std::fmt::Debug>(a: &L, b: &L, c: &L) {
+        // Conmutatividad.
+        assert_eq!(a.join(b), b.join(a));
+        assert_eq!(a.meet(b), b.meet(a));
+        // Asociatividad.
+        assert_eq!(a.join(b).join(c), a.join(&b.join(c)));
+        assert_eq!(a.meet(b).meet(c), a.meet(&b.meet(c)));
+        // Idempotencia.
+        assert_eq!(a.join(a), a.clone());
+        assert_eq!(a.meet(a), a.clone());
+        // Absorción.
+        assert_eq!(a.join(&a.meet(b)), a.clone());
+        assert_eq!(a.meet(&a.join(b)), a.clone());
+        // Neutros.
+        assert_eq!(a.join(&L::bottom()), a.clone());
+        assert_eq!(a.meet(&L::top()), a.clone());
+    }
+
+    fn nat_st() -> impl Strategy<Value = Nat> {
+        (0u64..10_000).prop_map(Nat)
+    }
+
+    fn reset_st() -> impl Strategy<Value = ResetVal> {
+        prop_oneof![
+            Just(ResetVal::Bottom),
+            Just(ResetVal::Top),
+            (0u64..4, -100i64..100)
+                .prop_map(|(generation, value)| ResetVal::Gen { generation, value }),
+        ]
+    }
+
+    proptest! {
+        #[test]
+        fn nat_es_reticulo(a in nat_st(), b in nat_st(), c in nat_st()) {
+            leyes_de_reticulo(&a, &b, &c);
+        }
+
+        #[test]
+        fn resetval_es_reticulo(a in reset_st(), b in reset_st(), c in reset_st()) {
+            leyes_de_reticulo(&a, &b, &c);
+        }
+
+        /// Generaciones distintas colapsan: su join es ⊤ y su meet es ⊥.
+        #[test]
+        fn reset_incomparable_colapsa(v1 in -100i64..100, v2 in -100i64..100) {
+            let a = ResetVal::Gen { generation: 0, value: v1 };
+            let b = ResetVal::Gen { generation: 1, value: v2 };
+            prop_assert!(a.partial_cmp(&b).is_none(), "gen distintas son incomparables");
+            prop_assert_eq!(a.join(&b), ResetVal::Top);
+            prop_assert_eq!(a.meet(&b), ResetVal::Bottom);
+        }
+
+        /// Ley adjunta de Galois para la identidad: trivial pero debe cumplirse.
+        #[test]
+        fn galois_identidad(a in nat_st(), b in nat_st()) {
+            let g = IdentityGalois;
+            prop_assert_eq!(g.lower(&a) <= b, a <= g.upper(&b));
+        }
+
+        /// Ley adjunta de Galois para la escala k·a ≤ b ⟺ a ≤ ⌊b/k⌋, y
+        /// monotonía de `lower`.
+        #[test]
+        fn galois_escala(a in 0u64..1000, a2 in 0u64..1000, b in 0u64..1000, k in 1u64..8) {
+            let g = ScaleGalois::new(k);
+            let (na, nb) = (Nat(a), Nat(b));
+            prop_assert_eq!(g.lower(&na) <= nb, na <= g.upper(&nb), "ley adjunta");
+            // Monotonía de lower: a ≤ a' ⟹ lower(a) ≤ lower(a').
+            let (lo, hi) = (Nat(a.min(a2)), Nat(a.max(a2)));
+            prop_assert!(g.lower(&lo) <= g.lower(&hi));
+        }
+    }
+}
diff --git a/src/lib.rs b/src/lib.rs
index 73b881e..8b866e1 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 lattice;
 pub mod linalg;
 pub mod nerve;
 pub mod oracle;