Author: Anonymous
Version: 1.0.0, 16 October 2026
Article type: Research manuscript
We formalize distributed capability through executable protocols with preservation and progress contracts. We prove transport and composition results, metric descent, and incentive separation. A presheaf infinity-topos distinguishes contextual correctness from global witnesses. Finite artifacts exhibit coordination failures and behavioral shifts under view-based rewards.
Keywords: distributed computation; safety; liveness; infinity-topos; contracts; incentives; observability.
A data center operates through distributed storage, communication, scheduling, and control. Service guarantees depend on coordination. Programmable ranking, allocation, and payments also influence participants. A feasible service need not induce desirable behavior; changing a reward need not change computational solvability.
Our thesis is relative: given hardware, local operations, observations, resources, failures, and timing assumptions, guaranteed capabilities are the tasks realized by executable protocols satisfying their contracts. This is a semantic definition, not a decision procedure from the labels preservation and progress.
We synthesize distributed semantics [1-6], topos semantics [7], and incentive analysis [8-10]. We contribute the combined framework and worked application. The transport, metric descent, and incentive separation lemmas are elementary. Impossibility results are imported; universal human control is not claimed.
Definition 2.1 (environment). Fix nonempty inputs and an environment : processes, local observations, executable primitives, network/storage semantics, failures, scheduling assumptions, and resources. Let be its executable local protocols. A process acts only on its local history; an omniscient global prescription is not thereby executable.
For and , let be the nonempty set of admissible maximal executions. Record scheduling and failures in executions. Pad finite terminal or deadlocked executions by stuttering, so every execution has a state sequence . An observation map yields an external history . External assumptions must not silently exclude an internal deadlock. Require an admissible extension for every legal finite execution prefix; explicitly identified terminal cases may stutter.
Fairness assumes scheduling behavior; it does not prove completion. Weak fairness concerns continuously enabled actions; strong fairness concerns actions enabled infinitely often. Resources belong to : exceeding a budget invalidates an implementation despite abstract correctness.
Definition 2.2 (contract). A task specifies a safety property and a progress obligation on external histories. Safety has a finite bad prefix whenever it fails [1]. A usual preservation certificate is an invariant with
Induction then gives . Not every safety property is already a predicate on the original state: a monitor or history variable can be necessary. A representative progress obligation is
with request identities and the obligated, for example nonfaulty, clients specified. This need not give a uniform latency bound. We use “progress obligation” broadly; it need not be a dense liveness property in the precise topology of [1]. Safety closure and response progress are separate proof obligations.
Definition 2.3 (realization and capability). Put
Existence requires executable witnesses; nonempty execution sets prevent vacuity. This is universal adversarial correctness. Almost-sure correctness instead quantifies probability-one events for each adversary, with its access to random choices specified.
Theorem 3.1 (environment restriction). Suppose two environments share inputs, protocols, observation maps, and costs, with and
for every and . Then .
Proof. Reuse the realizing program. Every execution quantified over in was already covered by its correctness proof in . The program remains executable and within budget.
Changing hardware, local information, or budgets is not merely restricting an adversary. Adding an oracle changes the program model. Strengthened assumptions must be declared.
Definition 3.2 (contract-preserving refinement). refines through input map and complete-history map if every admissible execution of maps to an admissible execution history of at input . Preserve task safety, progress, obligated clients, and request identities. Infinite internal stuttering cannot complete an outstanding abstract request. Also supply executable code and resource bounds [2].
Proposition 3.3 (refinement transport). If and satisfies Definition 3.2, then realizes the pullback contract .
Proof. Map each admissible complete implementation history to the promised admissible abstract history. Abstract correctness implies membership in ; taking the inverse image proves the assertion.
Theorem 3.4 (compatible composition). Let an executable assembly have component projections . Suppose every admissible execution of projects to an admissible complete execution of component , each realizes , and the global contract contains every history satisfying all pulled-back component contracts. Then realizes the global contract.
Proof. For any assembly execution, admissibility of each projection allows component correctness to be invoked. Its history belongs to every , hence to the global contract.
Projection admissibility is a scheduling and interface obligation. Components awaiting each other’s first message can deadlock: a projection may violate the assumed eventual arrival of an initiating message. Circular assumptions cannot supply that event. Finite step simulation alone does not establish progress.
The Fischer-Lynch-Paterson theorem rules out deterministic binary consensus with agreement, validity, and guaranteed termination in its asynchronous message-passing model with at least two processes and one possible crash [3]. Reliable eventual delivery does not give a known delivery bound. Replication or faster processors alone do not remove that obstruction. Partial synchrony changes assumptions and supports different solvability results [4]; randomization changes the termination guarantee and adversary model.
In the standard wait-free read/write setting, the asynchronous computability theorem characterizes finite task solvability by a chromatic decision map on a suitable protocol subdivision, carried by the task relation [5]. The colors, input/output carriers, and local-view structure are essential; bare equivalence of underlying homotopy types is insufficient.
For illustration, a mixed-input edge for two-process binary consensus has solo-input endpoints forced by validity to different decision components. Its wait-free protocol subdivision remains connected. A continuous decision map into the disconnected consensus output cannot carry both endpoints as required. This is the usual connectivity obstruction under these task hypotheses, not an assertion about all distributed models.
Proposition 4.1 (local invariants need not survive merge). Let replica states be subsets of , merge be union, and the invariant be . Starting from , independent reservations can each preserve the invariant while their merge violates it.
Proof. The reachable branch states and each satisfy the invariant; their union has cardinality two.
This violates invariant confluence in the merge model [6]. Union of event identifier sets instead preserves nonnegative counting and deduplication, though not honest event production. Coordination requirements depend on invariants and operations.
Choose a small category of finite observation contexts, with an initial empty context and arrows toward more informative extensions. The presheaf infinity-topos
supports restrictions and space-valued coherence [7]. The finite models use set-valued presheaves among its -truncated objects. The context category presents the semantic topos; it is not that topos. No additional sheaf gluing is presumed: imposing a topology requires specifying covers and their observational meaning.
Represent executable protocols by a -truncated object and admissible executions by . A baseline uses constant presheaves on and , with forgetting inputs and executions. Nonconstant contextual models require a specified operational witness interpretation. Let classify contract satisfaction. Define
Here is right adjoint to pullback on subobjects: every admissible execution satisfies . Nonempty fibers remain an environment obligation.
Proposition 5.1 (witness semantics). A specified global code factors through exactly when its execution fiber is contained in .
Proof. Since is -truncated, represents a subobject. The adjunction identifies with , the required fiber condition.
Internal truth of says that is an effective epimorphism. It need not furnish a global code . For example, in sheaves on a circle, the sheaf of local sections of the nontrivial double covering is locally inhabited but has no global section. The operational capability definition requires a global executable witness, with its locality and cost certificates.
Finite-limit constructions express invariant intersections and pullbacks. Progress, by contrast, refers to complete executions and temporal quantification. Transporting the latter requires preservation of the corresponding execution objects and quantifiers; left exactness by itself does not assert preservation of arbitrary dependent products or countable limits. We make no claim that passing to an infinity-topos resolves a coordination obstruction.
Fix an infrastructure protocol . Let parameterize ranking, access, payments, or metrics, participant strategies, and admissible disturbances and schedules. A specified model produces histories . Response sets may encode bounded rationality or heterogeneity; their empirical validity requires evidence. Performative prediction [9] studies related feedback; compositional game theory supplies richer interfaces [10].
For finite actions , let be expected credited views, a separately specified desired contribution, and a cost. One possible utility is
Coefficients convert scores to common utility units. Views may yield revenue, status, or allocation: an assumed instrumental payoff. Historical YouTube research modeled expected watch time [8]; this does not establish any platform’s current objective.
Theorem 6.1 (incentive separation). Suppose infrastructure preserves its safety and progress contract under either participant action. Let actions have
With utility-maximizing selection, is uniquely selected when , when , and both are optimal at equality. Thus an incentive change can reverse selected behavior with the infrastructure protocol and its guarantee unchanged.
Proof. Subtract utilities: . Its sign determines the maximizing action. Infrastructure correctness is uniform over both actions by hypothesis.
This proves conditional influence, not universal control. For a population share using , an assumed replicator model yields
for . Differentiating verifies the solution. Selection depends on this assumed response law; preferences, learning, outside alternatives, and regulation can change it. Workloads outside require a new infrastructure proof.
Theorem 7.1 (metric descent). For histories , a metric , and a Boolean property , there is an exact metric-only classifier with if and only if
Proof. Factorization implies equality on each fiber. Conversely, define to be the common value of on the nonempty fiber over . This value is unique, so its definition requires no choice of a representative.
Categorical form. Let be an effective epimorphism between -truncated objects of an infinity-topos, and classify a subobject. There is a unique with precisely when
Proof. Necessity follows by composition. Effective descent identifies maps from with compatible maps from the Cech nerve of . Since is -truncated, the kernel-pair equality supplies the compatibility, with no further nontrivial higher coherence. Descent gives existence and uniqueness. For general , apply this to its image.
Consequently, if two histories have equal views but different welfare, legality, or preservation outcomes, views alone cannot give an exact certificate of that property. A sound but incomplete classifier can reject a mixed fiber entirely. The theorem concerns information sufficiency, not whether a reward increases a metric. Even a perfectly implemented counter and reward service can optimize a metric that fails to distinguish the desired histories.
Let be actor ’s deployable configurations, allowed responses, and allowed disturbances, specified independently of the desired conclusion. With fixed, define robustly enforceable properties
Proposition 8.1 (authority monotonicity and limits). If and all other data are unchanged, then . Moreover, precisely when some allowed configuration’s entire outcome set is contained in . Existence of a desirable response alone is insufficient.
Proof. The same witness remains available to . The second assertion expands the universal quantifiers. If every configuration has an allowed counter-response outside , none witnesses membership.
Operators, designers, advertisers, participants, and regulators may control different parameters. Server ownership need not confer authority over every reward; writing code need not authorize deployment. Testing social influence requires actual authority, response behavior, and measured outcomes. Stochastic responses require an explicit probability or expectation criterion.
The accompanying standard-library Python artifact exhaustively explores a finite reservation scheduler, checks invariants, and analyzes fair cycles for response progress. It contrasts weak fairness of component ticks with fairness of actual service actions; checks replica merge counterexamples and metric fibers; and computes the incentive threshold and replicator trajectories. Synthetic parameters are exactly those in Section 6. No user telemetry, current platform internals, or causal estimates of human behavior are used.
Finite exploration verifies only the encoded finite system; it does not verify production services or replace imported impossibility proofs. No proof-assistant verification is claimed. Source links were checked on 16 October 2026; access evidence and results accompany the sources.
Admissible executable protocols delimit guaranteed services; authorized configurations and participant responses delimit robust behavioral influence. Desirable outcomes require additional properties that metrics may fail to classify.
Authorship and automation. Anonymous is the responsible human author, who supplied the thesis and authorized submission. OpenAI Codex assisted with formalization, references, drafting, artifacts, and document checks. The work remains subject to editorial and independent mathematical review.
[1] B. Alpern and F. B. Schneider. Defining liveness. IPL 21(4):181-185, 1985. Report.
[2] M. Abadi and L. Lamport. The existence of refinement mappings. TCS 82(2):253-284, 1991. Report.
[3] M. J. Fischer, N. A. Lynch, and M. S. Paterson. Impossibility of distributed consensus with one faulty process. JACM 32(2):374-382, 1985. Paper.
[4] C. Dwork, N. Lynch, and L. Stockmeyer. Consensus in the presence of partial synchrony. JACM 35(2):288-323, 1988. Paper.
[5] M. Herlihy and N. Shavit. The topological structure of asynchronous computability. JACM 46(6):858-923, 1999. Paper.
[6] P. Bailis, A. Fekete, M. J. Franklin, A. Ghodsi, J. M. Hellerstein, and I. Stoica. Coordination avoidance in database systems. PVLDB 8(3):185-196, 2014. Paper.
[7] J. Lurie. Higher Topos Theory. Annals of Mathematics Studies 170, Princeton, 2009. Author version, Sections 5.5.6, 6.1, 6.3: truncation, descent, and topoi.
[8] P. Covington, J. Adams, and E. Sargin. Deep neural networks for YouTube recommendations. RecSys 2016, 191-198. Google Research.
[9] J. Perdomo, T. Zrnic, C. Mendler-Dunner, and M. Hardt. Performative prediction. PMLR 119:7599-7609, 2020. Paper.
[10] N. Ghani, J. Hedges, V. Winschel, and P. Zahn. Compositional game theory. LICS 2018:472-481. Preprint. Our elementary response-set model does not implement open games.