Manuscript and evidence
The attached two-column monograph develops an operational and higher-categorical theory of computer networks whose processes follow their specified local rules. The attachments include the complete manuscript and its source, exact case generators, and certificate data. The assumptions governing crashes, scheduling, communication, and time are explicit in each model.
Operational and categorical setup
An honest process transition belongs to its specified relation on local state and actual input. Channel operations and environmental events, including crashes and recovery where admitted, obey their own relations. An observation site records which restrictions and overlapping patches are available. In its infinity-topos, a sheaf of raw records $X$ carries a conformance subobject $H\hookrightarrow X$. A map $H\to B$ exposes a joint boundary. Its fiber at $b$ is the space of records realizing $b$, together with comparison to the fixed boundary. A separate witness map can carry authorization, provenance, or a comparison between private representations.
Descent and replacement
For a finite face poset $I$ and a diagram $D:I^{\mathrm{op}}\to\mathcal S$, associate to a downward patch $U$ the limit of $D$ over $I_U^{\mathrm{op}}$. This is a sheaf for covers by unions. Indeed it is the mapping space out of the subterminal presheaf of visible cells, and the augmented Cech nerve of a cover realizes to that presheaf objectwise. Restriction to principal patches and the limit extension are inverse equivalences. The fixed-boundary completion spaces satisfy the same descent because limits commute.
Two open records compose by homotopy pullback over their common interface. A comparison over a joint boundary is an equivalence exactly when it gives equivalences on all generalized completion fibers. Such a comparison survives wiring and hiding. Conformance is observable on an effective quotient $p:X\to B$ exactly when its pullbacks along the two projections $X\times_B X\rightrightarrows X$ agree. Existential and universal images give the closest observable overapproximation and underapproximation.
Higher witnesses and obstructions
For constant $BG$ labels on a finite graph, a spanning forest normalizes tree labels. Each independent cycle retains a holonomy, and the residual action is simultaneous conjugation. A frame at one vertex in each component removes this residual action. Attaching a face adds the corresponding word relation. For abelian coherence of degree $n$, a prescribed obstruction class in $H^{n+1}(X;A)$ vanishes precisely when its space of nullhomotopies is inhabited. After choosing a lift, this space is equivalent to $\operatorname{Map}(X,K(A,n))$, with homotopy groups $H^{n-i}(X;A)$ in degrees $i\le n$. Pinned boundaries use relative cohomology. These results retain comparisons that disappear if connected components are taken before gluing.
Causality and progress
The cubical space of a finite causal event poset is contractible under the hypothesis that simultaneously enabled incomparable events can genuinely execute together. A capacity guard can remove higher cubes without removing any total order. For a downward family of permitted active sets, the manuscript derives the additive cohomology decomposition by induced permission complexes. For infinite histories, finite branching yields compatible runs from nonempty levels. Fairness is a separate condition. Finite recurrence certificates test fair noncompletion, while compactness of a fair family gives a uniform horizon when every run eventually has a finite success witness.
Distributed applications and checks
The manuscript applies the theory to consistent cuts, vector clocks, read and write quorum families, crash-recovery ballots, transaction commit, replicated joins, resource conservation, distributed knowledge, and temporal difference constraints. It includes 340 exact examples in nine families. Computations retain input diagrams and intermediate certificates such as dual obstruction vectors, negative cycles, reachable closed walks, stabilizer profiles, and independent cubical rank calculations. The general theorems are proved mathematically in the manuscript. The cases check finite instances.
References and disclosure
The higher-categorical foundations use Jacob Lurie's Higher Topos Theory and the theory of iterated spans. The distributed background includes Lamport's causal order, Chandy and Lamport's distributed snapshots, and Fischer, Lynch, and Paterson's asynchronous consensus result. The complete bibliography is in the PDF.
Generative AI assisted in drafting the exposition, proofs, typesetting, and case generators. The manuscript uses an anonymous byline.