We propose that the sheaf condition on a presheaf of design spaces provides a mathematical model for multi-view consistency in the architecture of cyber-physical systems (CPS). In model-based systems engineering, multiple engineering views -- electrical, thermal, mechanical, and software -- must be kept mutually consistent, yet current practice relies on informal procedures without a precise semantic account of global consistency. We construct an architectural site: a topological space whose points are pairwise interfaces between engineering domains and whose open sets represent engineering views. A design presheaf assigns to each view its local design space and to each inclusion the corresponding restriction map. We show that the sheaf condition on this presheaf is equivalent to compatibility on pairwise overlaps, yielding a local criterion for global multi-view consistency. The equivalence and a concrete three-view worked example are machine-verified in Lean 4 using Mathlib. The formalization establishes that the design presheaf is a sheaf, that the sheaf condition is equivalent to pairwise overlap compatibility, and that compatible local design families glue to unique global designs. Global consistency of an arbitrary number of views can be certified by checking only pairwise interface compatibility; compatible local designs determine a unique global design; derived properties computed by limit-preserving functors inherit the same consistency guarantee; and the entire verification chain admits machine-checkable proofs in Lean.

翻译：我们提出，设计空间预层上的层条件为网络物理系统（CPS）架构中的多视图一致性提供了数学模型。在基于模型的系统工程中，电气、热学、机械和软件等多个工程视图必须保持相互一致，但当前实践依赖非正式流程，缺乏对全局一致性的精确语义解释。我们构建了一个架构场地：其点为工程领域之间的成对接口，其开集表示工程视图。设计预层将每个局部设计空间分配给相应视图，并将限制映射分配给包含关系。我们证明该预层上的层条件等价于成对重叠上的相容性，从而为全局多视图一致性提供了局部判据。该等价性及一个具体的三视图示例已在Lean 4中通过Mathlib库完成机器验证。形式化证明表明：设计预层为层；层条件等价于成对重叠相容性；相容的局部设计族可粘合为唯一的全局设计。任意数量视图的全局一致性可通过仅检查成对接口相容性来认证；相容的局部设计唯一确定全局设计；由保极限函子计算的派生属性继承相同的一致性保证；整个验证链可在Lean中生成机器可检验的证明。