arxiv: 2605.08609 · v1 · submitted 2026-05-09 · 💻 cs.LO · math.CT

Recognition: no theorem link

Sheaves as a Means of Maintaining Consistency in Model-based Systems Engineering

Josh Gibson

Authors on Pith no claims yet

Pith reviewed 2026-05-12 00:56 UTC · model grok-4.3

classification 💻 cs.LO math.CT

keywords sheavespresheavesmulti-view consistencymodel-based systems engineeringcyber-physical systemsformal verificationLean 4topological models

0 comments

The pith

The sheaf condition on a presheaf of design spaces reduces global multi-view consistency to checks on pairwise interfaces.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper models multi-view consistency in model-based systems engineering by treating engineering views as open sets in a topological space whose points are pairwise domain interfaces. It assigns to each view a design space together with restriction maps, forming a presheaf. The central result establishes that this presheaf satisfies the sheaf condition precisely when local designs agree on every pairwise overlap. This equivalence supplies a local test that guarantees a unique global design exists. The construction and its consequences are verified by machine-checked proofs in Lean 4, including a concrete three-view example.

Core claim

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. 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.

What carries the argument

The architectural site, whose points are pairwise interfaces between engineering domains and whose open sets are the engineering views, together with the design presheaf that assigns local design spaces and restriction maps to those views; the sheaf condition on this presheaf then enforces global consistency.

If this is right

Global consistency of an arbitrary number of views can be certified by checking only pairwise interface compatibility.
Compatible local design families glue to unique global designs.
Derived properties computed by limit-preserving functors inherit the same consistency guarantee.
The entire verification chain admits machine-checkable proofs in Lean.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The same local-to-global pattern could be applied to consistency management in software architecture or database schema integration where overlapping models must agree.
If the topology is refined to include higher-order interfaces, the same sheaf machinery might handle consistency across more than two domains at once.
Machine-verifiable certificates of this form could be integrated into existing MBSE tools to automate consistency checks without manual global inspection.

Load-bearing premise

The chosen topological space whose points are pairwise interfaces and whose open sets are engineering views, together with the assignment of design spaces to views, accurately reflects the consistency requirements of actual model-based systems engineering practice.

What would settle it

A concrete CPS example in which two pairwise-compatible local designs fail to glue to any single global design, or in which the sheaf condition holds but global consistency is absent, would refute the claimed equivalence.

read the original abstract

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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

This paper gives a sheaf model for multi-view consistency in CPS where the sheaf condition reduces to pairwise interface checks, all verified in Lean.

read the letter

The main thing to know is that the authors build an architectural site with points as pairwise interfaces and opens as engineering views, then define a design presheaf and prove that its sheaf condition is exactly equivalent to compatibility on pairwise overlaps. Compatible local designs glue to a unique global design, and this plus some functor inheritance properties are all machine-checked in Lean 4 with Mathlib, including a concrete three-view example. Global consistency for any number of views can therefore be certified by checking only the pairwise cases. That equivalence and the gluing result are the actual new pieces here, and the formalization is a clear strength because it removes any doubt about the algebra working out. The construction itself is straightforward once the site is set up, and the Lean scripts give reproducible evidence that the presheaf really is a sheaf. On the practical side the paper stays light. There is no test against real CPS models or engineering data, so it is still an open question whether the chosen topology and restriction maps match the inconsistencies that show up in actual workflows. The claim that this will support automated verification tools follows from the math but is not demonstrated with any implementation or case study beyond the small example. The work is aimed at the small group of people who already care about categorical methods in systems engineering. A reader looking for a precise local-to-global criterion in formal MBSE could pull the equivalence and the Lean code as a starting point. I would send it to peer review. The formal core is grounded enough to justify referee time, and the authors can address the applicability gap in revisions without changing the central result.

Referee Report

0 major / 3 minor

Summary. The manuscript proposes modeling multi-view consistency in model-based systems engineering (MBSE) for cyber-physical systems via sheaves. It defines an architectural site as a topological space whose points are pairwise interfaces between engineering domains (e.g., electrical, mechanical) and whose open sets represent engineering views. A design presheaf assigns local design spaces to views together with restriction maps for inclusions. The central claims are that the sheaf condition on this presheaf is equivalent to pairwise overlap compatibility (providing a local criterion for global consistency), that the presheaf is a sheaf, and that compatible local design families glue to a unique global design. These results, along with a three-view worked example and inheritance properties under limit-preserving functors, are machine-verified in Lean 4 using Mathlib.

Significance. If the modeling assumptions hold, the work supplies a rigorous, machine-checkable semantic account of consistency in multi-domain CPS design, replacing informal procedures with a local-to-global principle. The explicit Lean 4 formalization using Mathlib is a clear strength, delivering parameter-free, reproducible proofs of the equivalence and gluing property. This could support development of automated consistency tools in MBSE. The approach is internally consistent and falsifiable via the formalization.

minor comments (3)

[Abstract] Abstract and §1: the description of the machine verification states that the equivalence and gluing are 'machine-verified' but supplies no metrics on formalization size (lines of code, number of definitions or theorems). Adding these would allow readers to gauge verification effort.
[§3] §3 (architectural site construction): the basis for the topology is defined via engineering views, but the verification that this collection satisfies the topology axioms (closure under arbitrary unions and finite intersections) is only sketched; an explicit lemma or reference to the Lean code for this check would improve clarity.
[§5] §5 (three-view example): the concrete design spaces and restriction maps are given, yet the manuscript does not discuss how these spaces would be populated from real engineering artifacts (e.g., SysML models), leaving the link to practice implicit.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive and accurate summary of our manuscript, which correctly captures the core contributions: the construction of an architectural site, the design presheaf, the equivalence of the sheaf condition to pairwise overlap compatibility, the gluing property for unique global designs, and the complete machine-verified formalization in Lean 4 using Mathlib. We appreciate the recognition of the work's internal consistency, falsifiability, and potential to support automated consistency tools in MBSE. The recommendation for minor revision is noted. As the report provides no specific major comments to address, the point-by-point responses below are empty.

Circularity Check

0 steps flagged

No significant circularity; formal construction with external verification

full rationale

The paper constructs an architectural site (points as pairwise interfaces, opens as views) and a design presheaf, then proves in Lean 4 (using Mathlib) that the sheaf condition is equivalent to pairwise overlap compatibility and that compatible local sections glue to a unique global section. This equivalence is a standard result in sheaf theory, here specialized to the chosen site and formally machine-checked rather than derived from fitted parameters or self-referential definitions. No load-bearing step reduces by construction to its own inputs; the central claims rest on explicit formalization of the presheaf axioms and gluing property, which are independent of the target consistency application. The derivation is self-contained against external benchmarks (Lean/Mathlib) and receives score 0.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 2 invented entities

The model introduces a custom topological space and presheaf tailored to engineering views; it relies on standard axioms of topology and sheaf theory but postulates that these structures correctly represent design consistency.

axioms (1)

standard math Standard axioms of topological spaces and presheaves/sheaves from category theory
Invoked when defining the architectural site and the design presheaf.

invented entities (2)

architectural site no independent evidence
purpose: Topological space whose points are pairwise interfaces and open sets are engineering views
Newly defined structure to host the presheaf model of multi-view design spaces.
design presheaf no independent evidence
purpose: Assignment of local design spaces to views with restriction maps
Custom presheaf whose sheaf condition is claimed to capture consistency.

pith-pipeline@v0.9.0 · 5525 in / 1410 out tokens · 35682 ms · 2026-05-12T00:56:15.698126+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

10 extracted references · 10 canonical work pages

[1]

Bohrer, V

B. Bohrer, V. Rahli, I. Vukotic, M. Völp, and A. Platzer. Formally verified differential dynamic logic. InProc. CPP, 2017

work page 2017
[2]

Breiner, E

S. Breiner, E. Subrahmanian, and R. Sriram. Modeling the roles of category theory in systems engineering. InProc. Applied Category Theory, 2019

work page 2019
[3]

A. Censi. A mathematical theory of co-design. arXiv:1512.08055, 2015

work page arXiv 2015
[4]

J. Goguen. Sheaf semantics for concurrent interacting objects.Mathematical Structures in Computer Science, 2(2):159–191, 1992

work page 1992
[5]

Goguen and G

J. Goguen and G. Malcolm. A hidden agenda.Theoretical Computer Science, 245(1):55–101, 2000

work page 2000
[6]

Kashiwara and P

M. Kashiwara and P. Schapira.Categories and Sheaves. Springer, 2006

work page 2006
[7]

Mac Lane and I

S. Mac Lane and I. Moerdijk.Sheaves in Geometry and Logic. Springer, 1994

work page 1994
[8]

Schultz, D

P. Schultz, D. I. Spivak, and C. Vasilakopoulou. Dynamical systems and sheaves.Applied Categorical Structures, 28:1–57, 2020

work page 2020
[9]

D. I. Spivak. The operad of wiring diagrams: formalizing a graphical language for databases, recursion, and plug-and-play circuits. arXiv:1305.0297, 2013

work page arXiv 2013
[10]

D. I. Spivak.Category Theory for the Sciences. MIT Press, 2014. 12

work page 2014