T6: Laplaciano de Tarski y difusión a punto fijo
Addendum §D/T6, aditivo — el motor lineal intacto: - tarski::LatticeSheaf (haz constante de retículos) y TarskiLaplacian con step (fórmula Ghrist-Riess Def.2/Lemma7: join sobre arista, F* adjunta, meet sobre aristas incidentes; sin resta) y harmonize (Kleene ascendente a punto fijo, con cota de seguridad). - Prueba de cordura CLAVE (la inversión): sobre el mismo triángulo donde el haz constante LINEAL inventa H¹=β₁=1, la difusión de Tarski con datos monótonos NO tiene obstrucción (preserva lo local, no colapsa a ⊤). - Un reset incompatible (generación incomparable) colapsa a ⊤: obstrucción semántica real, no topológica (§C.4). - Convergencia en tiempo finito verificada + punto fijo genuino. 32 tests, clippy limpio. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
This commit is contained in:
co-authored by
Claude Opus 4.8
parent
fc986d7cd7
commit
3819f9d88b
@@ -20,6 +20,7 @@ pub mod linalg;
|
||||
pub mod nerve;
|
||||
pub mod oracle;
|
||||
pub mod sheaf;
|
||||
pub mod tarski;
|
||||
pub mod verdict;
|
||||
|
||||
pub use error::{Result, SheafError};
|
||||
|
||||
+186
@@ -0,0 +1,186 @@
|
||||
//! `tarski` — haz de retículos y Laplaciano de Tarski (Addendum §D, T6).
|
||||
//!
|
||||
//! El giro respecto al MVP: en vez de `δ` con resta y `dim H¹`, se difunde el
|
||||
//! **Laplaciano de Tarski** `L` a punto fijo (Kleene/Tarski). El punto fijo es la
|
||||
//! mejor reconciliación globalmente coherente; su lectura da el veredicto (T7).
|
||||
//!
|
||||
//! Fórmula (Ghrist–Riess 2022, Def. 2 / Lemma 7), en grado 0 y **sin resta**:
|
||||
//! ```text
|
||||
//! (L x)_v = ⋀_{e ∋ v} F_{v⊴e}^* ( F_{v⊴e}(x_v) ∨ F_{w⊴e}(x_w) )
|
||||
//! ```
|
||||
//! - `∨` sobre la arista: reconcilia los dos extremos (expansión ∨ mezcla);
|
||||
//! - `F^*` (adjunta de Galois): baja el valor de arista de vuelta al vértice;
|
||||
//! - `⋀` sobre las aristas incidentes: el vértice debe ser coherente con todas.
|
||||
//!
|
||||
//! `L ≥ id` (cada término domina a `x_v` por la clausura de Galois
|
||||
//! `upper∘lower ≥ id`), luego iterar desde la siembra es un **ascenso** que
|
||||
//! converge en tiempo finito para retículos de altura finita.
|
||||
|
||||
use std::marker::PhantomData;
|
||||
|
||||
use crate::lattice::{GaloisRestriction, LatticeCell};
|
||||
|
||||
/// Una 0-cocadena: un valor de retículo por vértice.
|
||||
pub type Cochain<L> = Vec<L>;
|
||||
|
||||
/// Un haz **constante** de retículos: la misma stalk `L` en cada vértice/arista y
|
||||
/// la misma conexión de Galois `R` en cada incidencia. Cubre la prueba de cordura
|
||||
/// del Addendum (haz constante sobre un ciclo) y los encodings de CRDT (§D.1).
|
||||
#[derive(Debug, Clone)]
|
||||
pub struct LatticeSheaf<L, R> {
|
||||
/// Número de réplicas (vértices).
|
||||
pub num_vertices: usize,
|
||||
/// Aristas del nervio como pares `(u, v)`.
|
||||
pub edges: Vec<(usize, usize)>,
|
||||
/// Conexión de Galois uniforme en toda incidencia.
|
||||
pub restriction: R,
|
||||
_marker: PhantomData<L>,
|
||||
}
|
||||
|
||||
impl<L, R> LatticeSheaf<L, R> {
|
||||
/// Construye un haz constante de retículos.
|
||||
pub fn new(num_vertices: usize, edges: Vec<(usize, usize)>, restriction: R) -> Self {
|
||||
Self {
|
||||
num_vertices,
|
||||
edges,
|
||||
restriction,
|
||||
_marker: PhantomData,
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
/// El Laplaciano de Tarski como operador monótono sobre el retículo producto `C⁰`.
|
||||
pub struct TarskiLaplacian<'a, L, R> {
|
||||
sheaf: &'a LatticeSheaf<L, R>,
|
||||
}
|
||||
|
||||
impl<'a, L, R> TarskiLaplacian<'a, L, R>
|
||||
where
|
||||
L: LatticeCell,
|
||||
R: GaloisRestriction<L, L>,
|
||||
{
|
||||
/// Envuelve un haz para difundirlo.
|
||||
pub fn new(sheaf: &'a LatticeSheaf<L, R>) -> Self {
|
||||
Self { sheaf }
|
||||
}
|
||||
|
||||
/// Una aplicación de `L`: expansión ∨ mezcla por arista, meet sobre las
|
||||
/// aristas incidentes (Def. 2 / Lemma 7). Nunca desciende por debajo de `x`.
|
||||
pub fn step(&self, x: &[L]) -> Cochain<L> {
|
||||
let r = &self.sheaf.restriction;
|
||||
(0..self.sheaf.num_vertices)
|
||||
.map(|v| {
|
||||
// Valor de arista reconciliado, bajado a v, para cada arista incidente.
|
||||
let mut acc: Option<L> = None;
|
||||
for &(a, b) in &self.sheaf.edges {
|
||||
let w = if a == v {
|
||||
b
|
||||
} else if b == v {
|
||||
a
|
||||
} else {
|
||||
continue; // arista no incidente a v
|
||||
};
|
||||
// F_{v⊴e}(x_v) ∨ F_{w⊴e}(x_w), y de vuelta a v vía la adjunta.
|
||||
let edge_val = r.lower(&x[v]).join(&r.lower(&x[w]));
|
||||
let pulled = r.upper(&edge_val);
|
||||
acc = Some(match acc {
|
||||
None => pulled,
|
||||
Some(prev) => prev.meet(&pulled), // ⋀ sobre aristas incidentes
|
||||
});
|
||||
}
|
||||
// Vértice aislado: se queda como está. Si no, aseguramos el ascenso.
|
||||
match acc {
|
||||
None => x[v].clone(),
|
||||
Some(a) => x[v].join(&a),
|
||||
}
|
||||
})
|
||||
.collect()
|
||||
}
|
||||
}
|
||||
|
||||
impl<L, R> TarskiLaplacian<'_, L, R>
|
||||
where
|
||||
L: LatticeCell + PartialEq,
|
||||
R: GaloisRestriction<L, L>,
|
||||
{
|
||||
/// Cota de seguridad de iteraciones (backstop; la convergencia real la
|
||||
/// garantiza la altura finita del retículo, muy por debajo de esto).
|
||||
const MAX_STEPS: usize = 10_000;
|
||||
|
||||
/// Itera `L` desde la siembra hasta el punto fijo (Kleene ascendente).
|
||||
pub fn harmonize(&self, seed: &[L]) -> Cochain<L> {
|
||||
self.harmonize_with_steps(seed).0
|
||||
}
|
||||
|
||||
/// Como `harmonize`, devolviendo también cuántas aplicaciones de `L` costó.
|
||||
pub fn harmonize_with_steps(&self, seed: &[L]) -> (Cochain<L>, usize) {
|
||||
let mut x = seed.to_vec();
|
||||
for i in 0..Self::MAX_STEPS {
|
||||
let next = self.step(&x);
|
||||
if next == x {
|
||||
return (x, i);
|
||||
}
|
||||
x = next;
|
||||
}
|
||||
panic!("el Laplaciano de Tarski no convergió en {} pasos", Self::MAX_STEPS);
|
||||
}
|
||||
}
|
||||
|
||||
#[cfg(test)]
|
||||
mod tests {
|
||||
use super::*;
|
||||
use crate::lattice::{IdentityGalois, Nat, ResetVal};
|
||||
|
||||
fn triangulo() -> LatticeSheaf<Nat, IdentityGalois> {
|
||||
LatticeSheaf::new(3, vec![(0, 1), (1, 2), (2, 0)], IdentityGalois)
|
||||
}
|
||||
|
||||
/// LA prueba de cordura del giro (Addendum T6): sobre el **mismo triángulo**
|
||||
/// donde el haz constante lineal inventa `H¹ = β₁ = 1`, la difusión de Tarski
|
||||
/// con datos monótonos **no** tiene obstrucción: preserva lo local y no
|
||||
/// colapsa a ⊤.
|
||||
#[test]
|
||||
fn triangulo_de_reticulos_no_tiene_obstruccion() {
|
||||
let sheaf = triangulo();
|
||||
let seed = vec![Nat(5), Nat(3), Nat(7)];
|
||||
let harm = TarskiLaplacian::new(&sheaf).harmonize(&seed);
|
||||
|
||||
for (i, h) in harm.iter().enumerate() {
|
||||
assert_ne!(*h, Nat::INF, "no debe colapsar a ⊤");
|
||||
assert!(seed[i] <= *h, "preserva la información local (ascenso)");
|
||||
}
|
||||
|
||||
// Contraste explícito con el MVP lineal: el mismo triángulo SÍ da H¹=1.
|
||||
let lineal = crate::sheaf::Sheaf::constant(3, &[(0, 1), (1, 2), (2, 0)], 1);
|
||||
let coho = crate::cohomology::compute(&lineal).unwrap();
|
||||
assert_eq!(coho.dim_h1, 1, "el lineal inventa la obstrucción; Tarski la disuelve");
|
||||
}
|
||||
|
||||
/// Un reset incompatible (generación distinta, incomparable) colapsa a ⊤:
|
||||
/// obstrucción semántica **real**, no topológica (Addendum §C.4).
|
||||
#[test]
|
||||
fn reset_incompatible_colapsa_a_top() {
|
||||
let sheaf = LatticeSheaf::new(3, vec![(0, 1), (1, 2), (2, 0)], IdentityGalois);
|
||||
let seed = vec![
|
||||
ResetVal::Gen { generation: 0, value: 10 },
|
||||
ResetVal::Gen { generation: 0, value: 10 },
|
||||
ResetVal::Gen { generation: 1, value: 0 }, // réplica 2 reseteó
|
||||
];
|
||||
let harm = TarskiLaplacian::new(&sheaf).harmonize(&seed);
|
||||
assert!(
|
||||
harm.contains(&ResetVal::Top),
|
||||
"el reset incompatible debe colapsar algún vértice a ⊤"
|
||||
);
|
||||
}
|
||||
|
||||
/// Convergencia en tiempo finito (altura del retículo) y punto fijo genuino.
|
||||
#[test]
|
||||
fn converge_en_tiempo_finito_a_punto_fijo() {
|
||||
let sheaf = LatticeSheaf::new(4, vec![(0, 1), (1, 2), (2, 3), (3, 0)], IdentityGalois);
|
||||
let seed = vec![Nat(1), Nat(2), Nat(3), Nat(4)];
|
||||
let lap = TarskiLaplacian::new(&sheaf);
|
||||
let (harm, steps) = lap.harmonize_with_steps(&seed);
|
||||
assert_eq!(lap.step(&harm), harm, "el resultado es un punto fijo");
|
||||
assert!(steps <= 20, "converge acotado, no dio {steps} pasos");
|
||||
}
|
||||
}
|
||||
Reference in New Issue
Block a user