tawasuyu

tawasuyu/hifas

Motor en Rust para decidir, con demostración y no a ojo, cuándo un conjunto de réplicas local-first puede operar sin coordinación y cuándo no — y, cuando la respuesta es "sí, dentro de límites", proveer el mecanismo que lo garantiza.

Rust 11Markdown 1TOML 187 Sutichaykuna

⎇ 9de0cc601fd2eb7b9cf9b8a26ef8ed1ac1c9cd8d DISCREPANCIES.md Markdown · 95 siq'ikuna · 5.3 KB Ñawpa willay ch'uya

T8a: encoding desde el orden nativo — mata la circularidad de T5-T7 b666de794 · Sergio ·

1# Discrepancias haz ↔ oráculo CALM
2
3Registro de los casos donde el veredicto cohomológico **lineal** (`H¹`) **no**
4coincide con el oráculo CRDT/CALM. Como dice el SDD (§8, §11 R1), esto no es un
5bug a esconder: es el resultado científico del proyecto — dónde y por qué la
6Hipótesis H (§2.2) se rompe bajo la codificación lineal del MVP.
7
8> **ESTADO (lineal): RESUELTAS por la pista de retículos (M-research).** El caso
9> monótono-sobre-ciclo (triángulo/cuadrado) que el motor lineal marcaba como
10> obstrucción corre libre bajo el orden nativo — eso es correcto y sigue en pie.
11>
12> **⚠️ SALVEDAD (T8, ver `FLIPS.md`).** El acuerdo *perfecto* de T7 con el oráculo
13> era en parte **circular**: el encoding leía la etiqueta monótono/reset. T8a
14> rederiva el orden del merge (sin etiqueta) y el veredicto de los casos con
15> `reset` **voltea** a corre libre. La resolución del caso monótono-cíclico es
16> genuina; la de los reset era fabricada. La pregunta abierta (¿el haz supera a
17> CALM o lo espeja?) se decide en `STRONG_RESULT.md` (T8c).
18
19Reproducibles con `oracle::tests::discrepancias_del_lineal_persisten` (el lineal
20discrepa) y los casos de `oracle::casos_de_discrepancia()`.
21
22## Resumen
23
24| Caso | Oráculo (CALM) | Haz lineal (`H¹`) | Difusión de Tarski | Estado |
25|---|---|---|---|---|
26| `triangulo-monotono` | corre libre | `H¹ = 1` → coordina ❌ | corre libre ✅ | **RESUELTA** |
27| `cuadrado-monotono` | corre libre | `H¹ = 1` → coordina ❌ | corre libre ✅ | **RESUELTA** |
28| (general) dato **monótono** sobre grafo **cíclico** | corre libre | `H¹ = b₁ ≠ 0` ❌ | corre libre ✅ | **RESUELTA** |
29
30El MVP lineal **coincide** con el oráculo en todo el régimen de
31`oracle::casos_de_acuerdo()` (≥20 casos: sharing monótono acíclico y cualquier
32configuración no monótona). Tarski **coincide en toda la batería, sin excepción**,
33incluidos los cíclicos monótonos de arriba.
34
35## La discrepancia, en detalle
36
37**El caso.** Tres réplicas comparten un dato **monótono** (p.ej. un `GCounter`)
38en un triángulo: 0—1, 1—2, 2—0. Todas las operaciones son monótonas.
39
40**Qué dice CALM (oráculo).** Un `GCounter` se funde por máximo casilla a casilla;
41el join siempre existe y es único. No hay operación que retracte conocimiento,
42luego la configuración es **coordination-free**. El ciclo en el grafo de
43compartición es irrelevante: más caminos para difundir la misma información
44monótona no crean un conflicto.
45
46**Qué dice el haz.** La codificación lineal del MVP modela cada dato compartido
47como una restricción de **acuerdo** (identidad). Sobre el triángulo, el haz
48constante tiene `dim H¹ = b₁ = E − V + C = 3 − 3 + 1 = 1`. El motor reporta una
49obstrucción y pide coordinar.
50
51**Por qué ocurre (§2.3, R1).** La cohomología de haces es **lineal**; los
52retículos de los CRDTs son **de orden** (join-semilattices). Al aplanar el orden
53a álgebra lineal, el haz pierde la información de que la fusión monótona *siempre*
54pega las secciones locales. Lo que le queda es la topología pura del grafo, y la
55topología de un ciclo tiene `H¹ ≠ 0` con independencia de los datos. El haz
56"ve" así una obstrucción **topológica** donde CALM no ve ninguna **semántica**.
57
58Dicho de otro modo: bajo esta codificación, `H¹ = 0 ⟺ el grafo de compartición
59es acíclico`, un enunciado **puramente topológico** que solo coincide con CALM
60cuando el ciclo, de existir, transporta una operación no monótona (y por eso la
61codificación honesta añade un segundo enlace en conflicto solo en ese caso).
62
63## Consecuencia para la Hipótesis H
64
65En el **MVP lineal**, la Hipótesis H (`H¹ = 0 ⟺ coordination-free`) **se sostiene**
66para configuraciones cuyo sharing monótono es acíclico, y **falla** para datos
67monótonos sobre grafos cíclicos. La dirección que falla es conservadora: el haz
68pide coordinación de más (falsos positivos), nunca de menos. No se observó el
69fallo inverso (haz dice "libre" donde CALM dice "coordina").
70
71Bajo el **encoding de retículos con el Laplaciano de Tarski** (Addendum), la
72Hipótesis H pasa de "se sostiene solo en el caso acíclico" a **"se sostiene en
73general"**: la difusión reconcilia el dato monótono alrededor del ciclo sin
74colapsar, y solo colapsa a ⊤ ante una operación semánticamente incompatible (un
75`reset` que hace incomparables las generaciones). Verificado además por el
76invariante `proptest` "monótono sobre grafo arbitrario (cíclico incluido) ⟹
77corre libre", que el motor lineal *no podía* satisfacer.
78
79## Cómo se cerró (Addendum §B–§F, §2.3 / §11 Q2)
80
81Causa raíz: **la resta del coboundary** `(δx)_e = R·x_u − R·x_v`. Un
82join-semilattice no tiene inversos; al linealizarlo, `δ` mide desacuerdo-XOR e
83inventa obstrucciones-fantasma alrededor de los ciclos.
84
85La cura fue **eliminar la resta**: haces valuados en **retículos** con
86restricciones como **conexiones de Galois**, y el **Laplaciano de Tarski**
87(Ghrist–Riess 2022) difundido a punto fijo (Kleene/Tarski). El punto fijo es la
88mejor reconciliación coherente; corre libre si preserva lo local sin colapsar a ⊤.
89Ver `src/lattice.rs`, `src/tarski.rs` y `Verdict::via_tarski`.
90
91## Residuo abierto
92
93No se ha encontrado ningún caso donde **Tarski** y el oráculo discrepen. Si
94apareciera (p.ej. un CRDT que pida ya un *quantale*, R-L/Q-L1 del Addendum), ese
95residuo sería el siguiente resultado científico y se anotaría aquí.

DISCREPANCIES.md

Discrepancias haz ↔ oráculo CALM

Registro de los casos donde el veredicto cohomológico lineal (H¹) no coincide con el oráculo CRDT/CALM. Como dice el SDD (§8, §11 R1), esto no es un bug a esconder: es el resultado científico del proyecto — dónde y por qué la Hipótesis H (§2.2) se rompe bajo la codificación lineal del MVP.

ESTADO (lineal): RESUELTAS por la pista de retículos (M-research). El caso monótono-sobre-ciclo (triángulo/cuadrado) que el motor lineal marcaba como obstrucción corre libre bajo el orden nativo — eso es correcto y sigue en pie.

⚠️ SALVEDAD (T8, ver FLIPS.md). El acuerdo perfecto de T7 con el oráculo era en parte circular: el encoding leía la etiqueta monótono/reset. T8a rederiva el orden del merge (sin etiqueta) y el veredicto de los casos con reset voltea a corre libre. La resolución del caso monótono-cíclico es genuina; la de los reset era fabricada. La pregunta abierta (¿el haz supera a CALM o lo espeja?) se decide en STRONG_RESULT.md (T8c).

Reproducibles con oracle::tests::discrepancias_del_lineal_persisten (el lineal discrepa) y los casos de oracle::casos_de_discrepancia().

Resumen

CasoOráculo (CALM)Haz lineal (H¹)Difusión de TarskiEstado
triangulo-monotonocorre libreH¹ = 1 → coordina ❌corre libre ✅RESUELTA
cuadrado-monotonocorre libreH¹ = 1 → coordina ❌corre libre ✅RESUELTA
(general) dato monótono sobre grafo cíclicocorre libreH¹ = b₁ ≠ 0 ❌corre libre ✅RESUELTA

El MVP lineal coincide con el oráculo en todo el régimen de oracle::casos_de_acuerdo() (≥20 casos: sharing monótono acíclico y cualquier configuración no monótona). Tarski coincide en toda la batería, sin excepción, incluidos los cíclicos monótonos de arriba.

La discrepancia, en detalle

El caso. Tres réplicas comparten un dato monótono (p.ej. un GCounter) en un triángulo: 0—1, 1—2, 2—0. Todas las operaciones son monótonas.

Qué dice CALM (oráculo). Un GCounter se funde por máximo casilla a casilla; el join siempre existe y es único. No hay operación que retracte conocimiento, luego la configuración es coordination-free. El ciclo en el grafo de compartición es irrelevante: más caminos para difundir la misma información monótona no crean un conflicto.

Qué dice el haz. La codificación lineal del MVP modela cada dato compartido como una restricción de acuerdo (identidad). Sobre el triángulo, el haz constante tiene dim H¹ = b₁ = E − V + C = 3 − 3 + 1 = 1. El motor reporta una obstrucción y pide coordinar.

Por qué ocurre (§2.3, R1). La cohomología de haces es lineal; los retículos de los CRDTs son de orden (join-semilattices). Al aplanar el orden a álgebra lineal, el haz pierde la información de que la fusión monótona siempre pega las secciones locales. Lo que le queda es la topología pura del grafo, y la topología de un ciclo tiene H¹ ≠ 0 con independencia de los datos. El haz "ve" así una obstrucción topológica donde CALM no ve ninguna semántica.

Dicho de otro modo: bajo esta codificación, H¹ = 0 ⟺ el grafo de compartición es acíclico, un enunciado puramente topológico que solo coincide con CALM cuando el ciclo, de existir, transporta una operación no monótona (y por eso la codificación honesta añade un segundo enlace en conflicto solo en ese caso).

Consecuencia para la Hipótesis H

En el MVP lineal, la Hipótesis H (H¹ = 0 ⟺ coordination-free) se sostiene para configuraciones cuyo sharing monótono es acíclico, y falla para datos monótonos sobre grafos cíclicos. La dirección que falla es conservadora: el haz pide coordinación de más (falsos positivos), nunca de menos. No se observó el fallo inverso (haz dice "libre" donde CALM dice "coordina").

Bajo el encoding de retículos con el Laplaciano de Tarski (Addendum), la Hipótesis H pasa de "se sostiene solo en el caso acíclico" a "se sostiene en general": la difusión reconcilia el dato monótono alrededor del ciclo sin colapsar, y solo colapsa a ⊤ ante una operación semánticamente incompatible (un reset que hace incomparables las generaciones). Verificado además por el invariante proptest "monótono sobre grafo arbitrario (cíclico incluido) ⟹ corre libre", que el motor lineal no podía satisfacer.

Cómo se cerró (Addendum §B–§F, §2.3 / §11 Q2)

Causa raíz: la resta del coboundary (δx)_e = R·x_u − R·x_v. Un join-semilattice no tiene inversos; al linealizarlo, δ mide desacuerdo-XOR e inventa obstrucciones-fantasma alrededor de los ciclos.

La cura fue eliminar la resta: haces valuados en retículos con restricciones como conexiones de Galois, y el Laplaciano de Tarski (Ghrist–Riess 2022) difundido a punto fijo (Kleene/Tarski). El punto fijo es la mejor reconciliación coherente; corre libre si preserva lo local sin colapsar a ⊤. Ver src/lattice.rs, src/tarski.rs y Verdict::via_tarski.

Residuo abierto

No se ha encontrado ningún caso donde Tarski y el oráculo discrepen. Si apareciera (p.ej. un CRDT que pida ya un quantale, R-L/Q-L1 del Addendum), ese residuo sería el siguiente resultado científico y se anotaría aquí.