tawasuyu/hifas

1//! `tarski` — haz de retículos y Laplaciano de Tarski (Addendum §D, T6).
2//!
3//! El giro respecto al MVP: en vez de `δ` con resta y `dim H¹`, se difunde el
4//! **Laplaciano de Tarski** `L` a punto fijo (Kleene/Tarski). El punto fijo es la
5//! mejor reconciliación globalmente coherente; su lectura da el veredicto (T7).
6//!
7//! Fórmula (Ghrist–Riess 2022, Def. 2 / Lemma 7), en grado 0 y **sin resta**:
8//! ```text
9//!   (L x)_v = ⋀_{e ∋ v}  F_{v⊴e}^* ( F_{v⊴e}(x_v)  ∨  F_{w⊴e}(x_w) )
10//! ```
11//! - `∨` sobre la arista: reconcilia los dos extremos (expansión ∨ mezcla);
12//! - `F^*` (adjunta de Galois): baja el valor de arista de vuelta al vértice;
13//! - `⋀` sobre las aristas incidentes: el vértice debe ser coherente con todas.
14//!
15//! `L ≥ id` (cada término domina a `x_v` por la clausura de Galois
16//! `upper∘lower ≥ id`), luego iterar desde la siembra es un **ascenso** que
17//! converge en tiempo finito para retículos de altura finita.
18
19use std::marker::PhantomData;
20
21use crate::lattice::{GaloisRestriction, LatticeCell};
22
23/// Una 0-cocadena: un valor de retículo por vértice.
24pub type Cochain<L> = Vec<L>;
25
26/// Un haz **constante** de retículos: la misma stalk `L` en cada vértice/arista y
27/// la misma conexión de Galois `R` en cada incidencia. Cubre la prueba de cordura
28/// del Addendum (haz constante sobre un ciclo) y los encodings de CRDT (§D.1).
29#[derive(Debug, Clone)]
30pub struct LatticeSheaf<L, R> {
31    /// Número de réplicas (vértices).
32    pub num_vertices: usize,
33    /// Aristas del nervio como pares `(u, v)`.
34    pub edges: Vec<(usize, usize)>,
35    /// Conexión de Galois uniforme en toda incidencia.
36    pub restriction: R,
37    _marker: PhantomData<L>,
38}
39
40impl<L, R> LatticeSheaf<L, R> {
41    /// Construye un haz constante de retículos.
42    pub fn new(num_vertices: usize, edges: Vec<(usize, usize)>, restriction: R) -> Self {
43        Self {
44            num_vertices,
45            edges,
46            restriction,
47            _marker: PhantomData,
48        }
49    }
50}
51
52/// El Laplaciano de Tarski como operador monótono sobre el retículo producto `C⁰`.
53pub struct TarskiLaplacian<'a, L, R> {
54    sheaf: &'a LatticeSheaf<L, R>,
55}
56
57impl<'a, L, R> TarskiLaplacian<'a, L, R>
58where
59    L: LatticeCell,
60    R: GaloisRestriction<L, L>,
61{
62    /// Envuelve un haz para difundirlo.
63    pub fn new(sheaf: &'a LatticeSheaf<L, R>) -> Self {
64        Self { sheaf }
65    }
66
67    /// Una aplicación de `L`: expansión ∨ mezcla por arista, meet sobre las
68    /// aristas incidentes (Def. 2 / Lemma 7). Nunca desciende por debajo de `x`.
69    pub fn step(&self, x: &[L]) -> Cochain<L> {
70        let r = &self.sheaf.restriction;
71        (0..self.sheaf.num_vertices)
72            .map(|v| {
73                // Valor de arista reconciliado, bajado a v, para cada arista incidente.
74                let mut acc: Option<L> = None;
75                for &(a, b) in &self.sheaf.edges {
76                    let w = if a == v {
77                        b
78                    } else if b == v {
79                        a
80                    } else {
81                        continue; // arista no incidente a v
82                    };
83                    // F_{v⊴e}(x_v) ∨ F_{w⊴e}(x_w), y de vuelta a v vía la adjunta.
84                    let edge_val = r.lower(&x[v]).join(&r.lower(&x[w]));
85                    let pulled = r.upper(&edge_val);
86                    acc = Some(match acc {
87                        None => pulled,
88                        Some(prev) => prev.meet(&pulled), // ⋀ sobre aristas incidentes
89                    });
90                }
91                // Vértice aislado: se queda como está. Si no, aseguramos el ascenso.
92                match acc {
93                    None => x[v].clone(),
94                    Some(a) => x[v].join(&a),
95                }
96            })
97            .collect()
98    }
99}
100
101impl<L, R> TarskiLaplacian<'_, L, R>
102where
103    L: LatticeCell + PartialEq,
104    R: GaloisRestriction<L, L>,
105{
106    /// Cota de seguridad de iteraciones (backstop; la convergencia real la
107    /// garantiza la altura finita del retículo, muy por debajo de esto).
108    const MAX_STEPS: usize = 10_000;
109
110    /// Itera `L` desde la siembra hasta el punto fijo (Kleene ascendente).
111    pub fn harmonize(&self, seed: &[L]) -> Cochain<L> {
112        self.harmonize_with_steps(seed).0
113    }
114
115    /// Como `harmonize`, devolviendo también cuántas aplicaciones de `L` costó.
116    pub fn harmonize_with_steps(&self, seed: &[L]) -> (Cochain<L>, usize) {
117        let mut x = seed.to_vec();
118        for i in 0..Self::MAX_STEPS {
119            let next = self.step(&x);
120            if next == x {
121                return (x, i);
122            }
123            x = next;
124        }
125        panic!("el Laplaciano de Tarski no convergió en {} pasos", Self::MAX_STEPS);
126    }
127}
128
129#[cfg(test)]
130mod tests {
131    use super::*;
132    use crate::lattice::{IdentityGalois, Nat, ResetVal};
133
134    fn triangulo() -> LatticeSheaf<Nat, IdentityGalois> {
135        LatticeSheaf::new(3, vec![(0, 1), (1, 2), (2, 0)], IdentityGalois)
136    }
137
138    /// LA prueba de cordura del giro (Addendum T6): sobre el **mismo triángulo**
139    /// donde el haz constante lineal inventa `H¹ = β₁ = 1`, la difusión de Tarski
140    /// con datos monótonos **no** tiene obstrucción: preserva lo local y no
141    /// colapsa a ⊤.
142    #[test]
143    fn triangulo_de_reticulos_no_tiene_obstruccion() {
144        let sheaf = triangulo();
145        let seed = vec![Nat(5), Nat(3), Nat(7)];
146        let harm = TarskiLaplacian::new(&sheaf).harmonize(&seed);
147
148        for (i, h) in harm.iter().enumerate() {
149            assert_ne!(*h, Nat::INF, "no debe colapsar a ⊤");
150            assert!(seed[i] <= *h, "preserva la información local (ascenso)");
151        }
152
153        // Contraste explícito con el MVP lineal: el mismo triángulo SÍ da H¹=1.
154        let lineal = crate::sheaf::Sheaf::constant(3, &[(0, 1), (1, 2), (2, 0)], 1);
155        let coho = crate::cohomology::compute(&lineal).unwrap();
156        assert_eq!(coho.dim_h1, 1, "el lineal inventa la obstrucción; Tarski la disuelve");
157    }
158
159    /// Un reset incompatible (generación distinta, incomparable) colapsa a ⊤:
160    /// obstrucción semántica **real**, no topológica (Addendum §C.4).
161    #[test]
162    fn reset_incompatible_colapsa_a_top() {
163        let sheaf = LatticeSheaf::new(3, vec![(0, 1), (1, 2), (2, 0)], IdentityGalois);
164        let seed = vec![
165            ResetVal::Gen { generation: 0, value: 10 },
166            ResetVal::Gen { generation: 0, value: 10 },
167            ResetVal::Gen { generation: 1, value: 0 }, // réplica 2 reseteó
168        ];
169        let harm = TarskiLaplacian::new(&sheaf).harmonize(&seed);
170        assert!(
171            harm.contains(&ResetVal::Top),
172            "el reset incompatible debe colapsar algún vértice a ⊤"
173        );
174    }
175
176    /// Convergencia en tiempo finito (altura del retículo) y punto fijo genuino.
177    #[test]
178    fn converge_en_tiempo_finito_a_punto_fijo() {
179        let sheaf = LatticeSheaf::new(4, vec![(0, 1), (1, 2), (2, 3), (3, 0)], IdentityGalois);
180        let seed = vec![Nat(1), Nat(2), Nat(3), Nat(4)];
181        let lap = TarskiLaplacian::new(&sheaf);
182        let (harm, steps) = lap.harmonize_with_steps(&seed);
183        assert_eq!(lap.step(&harm), harm, "el resultado es un punto fijo");
184        assert!(steps <= 20, "converge acotado, no dio {steps} pasos");
185    }
186}