Nous construisons des opérateurs de frontière sur le nerf d'une couverture finie en utilisant des données d'orientation auxiliaires et prouvons que des données compatibles produisent un complexe de chaînes avec une première homologie bien définie. Nous établissons que des données d'orientation compatibles existent toujours, bien que de façon non canonique. Nous prouvons ensuite le résultat principal : pour chaque paire de triangles partageant un bord, deux données témoins globales différant par une seule transposition de sommet ne peuvent pas toutes deux satisfaire à la cohérence globale. Cela démontre que la condition de cohérence n'est pas déterminée par le support simplicial du nerf. Dans le contexte de la théorie causale spectrale, toute approche intrinsèque pour extraire des données homologiques doit s'appuyer sur des informations structurelles au-delà des données des simplexes non ordonnés du nerf - comme un ordre partiel causal. Tous les résultats sont formalisés et vérifiés par machine dans Lean 4 (63 modules, plus de 260 théorèmes, zéro excuse/admission). Code source : https://github.com/davidichalfyorov-wq/sct-theory
David Alfyorov (Fri,) a étudié cette question.