AI 中文总结
本文提出SAGA比较定理，通过构建两种上同调证明局部与全局软件架构正确性的一致性，结合Lean形式化与ArchSig工具在微服务系统上验证了语义诊断与几何计算的可转换性。
AI 中文摘要
在软件架构中，每个服务可遵循自身约定，相邻服务间的每个交接也可保持正常，却仍可能存在仅在对系统进行完整遍历后才显现的语义不一致性。本文独立构建了两种衡量局部与全局正确性之间差距的上同调，并证明它们是一致的。第一种构建采用修复语言：从每个局部上下文中允许的语义修复选项及其等价关系，生成系数$M_{\mathrm{sem}}$。第二种采用方程语言：将架构的约束组织为联立方程组，并通过其阻碍理想生成商系数$Q_E$。在代数架构理论（AAT，该理论将软件架构构建为代数几何）中选定的有限覆盖$U$上，且在与局部数据匹配的有限个选择条件下，比较映射诱导出同构$H^1_{\mathrm{sem}}(U) \cong \check{H}^1(U, Q_E)$，同时伴随剩余类的对应关系，我们将此称为SAGA比较定理。两种语言中衡量的阻碍是同一上同调类，因此语义诊断与几何计算可相互转换。此外，当修复状态族满足层条件时，存在全局修复当且仅当两侧的阻碍类均消失。本文从三个层面呈现该结果：数学证明、发布时的Lean形式化状态、以及诊断：测量工具ArchSig在真实开源微服务系统上，可复现地完成从测得的非零阻碍到修复后其消失的完整过程。这三个层面指向同一发布标识，且每个主张均与主要证据相关联。
英文摘要
In a software architecture, each service can obey its own conventions and each handoff between adjacent services can hold, and yet a semantic inconsistency may remain that appears only on a full traversal of the system. This paper independently constructs two cohomologies measuring this gap between local and global correctness, and proves that they agree. The first construction speaks the language of repair: from the semantic repair options admitted in each local context and their equivalence relation, it generates the coefficient $M_{\mathrm{sem}}$. The second speaks the language of equations: it organizes the constraints of the architecture as a simultaneous equation system and generates the quotient coefficient $Q_E$ by its obstruction ideal. Over a selected finite cover $U$ in Algebraic Architecture Theory (AAT), which constructs software architecture as algebraic geometry, and under finitely many selection conditions matching the local data, the comparison map induces the isomorphism $H^1_{\mathrm{sem}}(U) \cong \check{H}^1(U, Q_E)$ together with a correspondence of residual classes. We call this the SAGA comparison theorem. The obstructions measured in the two languages are the same cohomology class, so semantic diagnosis and geometric computation translate into each other. Moreover, when the family of repair states satisfies the sheaf condition, a global repair exists if and only if the obstruction class vanishes on both sides. The paper presents this result in three layers: the mathematical proof; the Lean formalization status at release time; and a diagnosis in which the measurement tool ArchSig, on a real open-source microservice system, reproducibly walks the full circle from a measured nonzero obstruction to its disappearance after repair. The three layers refer to the same release identity, and each claim is connected to primary evidence.
Comments42 pages, 2 figures. Version 1.0.1 (textual corrections to the Zenodo v1.0.0 deposit). Also archived on Zenodo with the full evidence bundle and Lean sources: https://doi.org/10.5281/zenodo.21603761
