From fc986d7cd7125c337a3117308bdde4bc03f1a5a7 Mon Sep 17 00:00:00 2001 From: Sergio Date: Wed, 1 Jul 2026 19:04:47 +0000 Subject: [PATCH] =?UTF-8?q?T5:=20ret=C3=ADculos=20y=20restricciones=20de?= =?UTF-8?q?=20Galois=20(pista=20de=20Tarski)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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) --- ADDENDUM.md | 220 +++++++++++++++++++++++++++++++++++++++++ src/lattice.rs | 262 +++++++++++++++++++++++++++++++++++++++++++++++++ src/lib.rs | 1 + 3 files changed, 483 insertions(+) create mode 100644 ADDENDUM.md create mode 100644 src/lattice.rs 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 { + 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 { + 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 { + /// `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 GaloisRestriction 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 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(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 { + (0u64..10_000).prop_map(Nat) + } + + fn reset_st() -> impl Strategy { + 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;