Two structural facts anchor the theory of indefinite causal order, and this paper proves both as explicit theorems and checks them line by line in a machine proof assistant. The first is a record fact: a process without a definite order must keep, on its control memory, a record of the orders it superposes, and erasing that record by blurring the control returns a plain mixture of definite orders. The second is a classification fact: on the canonical slice of processes, a single straight-line certificate decides exactly which processes are ordered and which are not. Working over an abstract algebra of order operators, so that each result holds in any faithful concrete model, the paper proves a short, connected set of statements. Blurring the order record always lands the process in the definite-order set, which is the mathematical heart of record-erasure. A process sits in that definite-order set exactly when it is unchanged by blurring, so that any surviving control coherence is an irreducible record. The number of orders a process populates is at most the size of its control memory, which is the record form of the memory cost studied elsewhere in the program. On the canonical slice the certificate takes a specific value that varies in a straight-line way across the slice, so that indefiniteness holds precisely on one side of a line, with an explicit decomposition into definite orders on the other side. And a tempting finer diagnostic built from the process's intrinsic flow is shown to over-count, because it tracks a product of the two dials rather than the true boundary. Every theorem is stated over an abstract ring so that it transfers to any faithful model, and every statement in the paper has been checked in a machine proof assistant with no assumptions beyond the three standard foundations of mathematics; the correspondence to the formal development is tabulated in an appendix. The contribution is a small, dependable, reusable core that turns the program's paper-level results about indefinite causal order into a durable, independently checkable formal library, and by forcing complete rigour it guards against hidden gaps of the kind that informal arguments can conceal. The paper is careful about scope, noting that the definite-order set reached by full blurring is contained in, but does not exhaust, the whole ordered set, and that the finer flow-based diagnostic is only a necessary sign of indefiniteness, not a sufficient one. What it secures is a machine-checked foundation on which the geometric, thermodynamic, and resource-theoretic parts of the program can safely rest.
Two structural facts anchor the theory of indefinite causal order, and this paper proves both as explicit theorems and checks them line by line in a machine proof assistant. The first is a record fact: a process without a definite order must keep, on its control memory, a record of the orders it superposes, and erasing that record by blurring the control returns a plain mixture of definite orders. The second is a classification fact: on the canonical slice of processes, a single straight-line certificate decides exactly which processes are ordered and which are not. Working over an abstract algebra of order operators, so that each result holds in any faithful concrete model, the paper proves a short, connected set of statements. Blurring the order record always lands the process in the definite-order set, which is the mathematical heart of record-erasure. A process sits in that definite-order set exactly when it is unchanged by blurring, so that any surviving control coherence is an irreducible record. The number of orders a process populates is at most the size of its control memory, which is the record form of the memory cost studied elsewhere in the program. On the canonical slice the certificate takes a specific value that varies in a straight-line way across the slice, so that indefiniteness holds precisely on one side of a line, with an explicit decomposition into definite orders on the other side. And a tempting finer diagnostic built from the process's intrinsic flow is shown to over-count, because it tracks a product of the two dials rather than the true boundary. Every theorem is stated over an abstract ring so that it transfers to any faithful model, and every statement in the paper has been checked in a machine proof assistant with no assumptions beyond the three standard foundations of mathematics; the correspondence to the formal development is tabulated in an appendix. The contribution is a small, dependable, reusable core that turns the program's paper-level results about indefinite causal order into a durable, independently checkable formal library, and by forcing complete rigour it guards against hidden gaps of the kind that informal arguments can conceal. The paper is careful about scope, noting that the definite-order set reached by full blurring is contained in, but does not exhaust, the whole ordered set, and that the finer flow-based diagnostic is only a necessary sign of indefiniteness, not a sufficient one. What it secures is a machine-checked foundation on which the geometric, thermodynamic, and resource-theoretic parts of the program can safely rest.
Indefinite causal order acquires a clean geometric home in this paper. The processes allowed by the theory fill one convex body, the kind of region carved out by a matrix inequality, while the processes with a definite order fill that body's shadow, the flatter silhouette cast when the body is projected down. A process is genuinely indefinite precisely when it lands in the gap between the body and its own shadow. This single picture explains at a glance why detecting indefinite order requires a certificate: a shadow can be strictly smaller than the object that casts it. The paper shows that the valid processes are exactly the positive part of a structured operator system of a definite size, which is the technical meaning of the convex body in question, and that the ordered processes are the shadow of the combination of the two definite-order regions. Indefinite order lives in the gap between the two, and that gap is exactly what the separating certificates detect. The paper then reads each process through an intrinsic notion of flow that the process itself defines, a kind of built-in clock, and finds that for the canonical indefinite process this flow is order-entangled, its two order-halves refusing to commute, whereas for definite orders the flow simply respects the order. It is careful to show that this flow-based diagnostic over-counts: it also flags some ordered processes, so it is a weaker signal than the exact certificate boundary. On the two-dial canonical slice the paper gives an exact classification, with a circular region of validity, a straight-line boundary of separability, and a lens-shaped region of genuine indefiniteness in between. The contribution is a way of seeing why indefinite causal order behaves as it does: it is the discrepancy between a body and its shadow, which is exactly why a witness, a supporting plane of the shadow, is needed to certify it. The flow-based reading adds an intrinsic, clock-like description of order-entanglement, while the paper honestly flags that this finer description is only a necessary sign and not a sufficient one, since it over-counts. By recasting causal nonseparability in the language of operator systems and their shadows, the paper connects a foundational quantum property to well-developed convex geometry and sets up the multipartite and thermodynamic sequels.
It is now settled which indefinite-order processes can actually be built in the laboratory; the question this paper takes up is how expensive building one is, and it answers with a single cost measure that is intrinsic to the process, applies universally, and can be computed. The cost is the amount of control memory any realization must carry to keep the different orders straight. The paper bounds this memory from below by a quantity it reads off the process alone, the order rank, and shows that indefiniteness of order forces a permanent record of at least that size into the future of the process, a record no clever construction can hide. The paper defines the order rank of a process as the fewest separate future measurements whose blurring would render the process ordered, a definition that needs no reference to how the process is built. It then proves that the control memory of any realization can itself be blurred in a way that orders the process, so the memory can never be smaller than the order rank; indefinite order therefore compels information about which order occurred to be written into the global future, an unavoidable record. When the order is stored in a dedicated record subsystem, the order rank turns out to equal a standard measure of how entangled that record is with the rest, so an ordered process is exactly one whose record is unentangled, and a single averaged measurement can read the number of superposed orders straight off a process. This yields a full ladder of processes graded by how many orders they mix. For the switchable process on many parties the orders are perfectly distinguishable and the cost is exactly the number of possible orderings, which grows faster than exponentially; and every intermediate cost is achieved by some process. The order rank is faithful, unchanged by local rearrangement, strictly reduced by throwing away a party, and independent of the separate noise-robustness measure, as a purely classical but maximally robust example makes plain. The contribution is a clean, computable price tag for indefinite causal order and a theorem that this price cannot be evaded: a nonseparable process must broadcast a record of its orders into the future, of a size fixed by the order rank. By identifying that rank with a familiar entanglement measure of the record, the paper connects the cost of indefinite order to well-understood mathematics and supplies a single-measurement way to certify it. It also draws a careful line, showing that the order rank and the more commonly used noise-robustness are two genuinely different resources rather than two names for one, so that a process can be highly robust yet cheap, or costly yet fragile.
Process matrices describe correlations with no definite order of operations, and the property that sets a genuinely indefinite process apart from an ordinary mixture of ordered ones is called causal nonseparability. This paper gives a careful, self-contained account of why the whole framework hangs together consistently, across three levels at once, the level of plain probabilities, the level of quantum measurement rules, and the level of classical logical consistency. Its main practical result is an exact, written-out certificate that detects the indefiniteness of the canonical process by hand, replacing a numerical computer search with a formula a reader can check with pencil and paper. Working in a convenient basis in which the relevant bookkeeping operations act especially simply, the paper derives the certificate in closed form as the identity minus two specific order-sensitive terms. It shows that the two natural pieces of this certificate are well-behaved in the technical sense required, each with an explicit, exactly known set of values and an explicit proof of positivity written as a sum of squares. Evaluated on the canonical indefinite process, the certificate returns a specific negative number exactly, which is precisely the signal of indefiniteness. The paper then abstracts the construction into a general recipe, a theorem stating that any certificate of this shape is valid whenever a simple sum-of-squares condition holds on its two pieces. Alongside this it lays out, level by level, how the framework stays consistent, from the requirement that probabilities behave, through the quantum measurement rule, to the classical fixed-point picture in which a would-be paradoxical loop has, or fails to have, a unique consistent resolution. Every numbered result is also formally verified in a machine proof assistant, to the authors' knowledge the first such verification for this framework, with the correspondence to the formal statements collected in an appendix. The value of the paper is to turn what had been the output of an opaque numerical optimizer into a transparent, reusable, and independently machine-checked object that anyone can audit and build on. By exhibiting an exact certificate and a general recipe for producing more, it lowers the barrier to certifying indefinite causal order, and by verifying the whole consistency core in a proof assistant it supplies a dependable formal foundation for later work. The paper is modest about what it adds, presenting the physics of the canonical process as already known and offering instead an exact and verifiable rendering of it.
The clean geometric picture of indefinite order, a body of valid processes and the shadow of ordered ones, is here lifted from two parties to many, and to the physically buildable switchable process. The decisive new feature appears with three or more parties: being ordered no longer means committing to one fixed sequence in advance, because the order can be decided on the fly, conditioned on earlier results. As a consequence the ordered set is strictly larger than the mere collection of all fixed sequences, and indefinite order for many parties means falling outside even this enlarged, flexible set. Constructing the many-party body of valid processes forces a from-scratch re-derivation of the rules a valid process must obey, which yields a tidy closed formula for the size of the valid space at every number of parties, and the body is again the matrix-inequality kind. For three or more parties the ordered set is the shadow of a branching tree of quantum-controlled sub-processes, and this shadow is strictly bigger than the collection of fixed sequences; the paper makes the difference exact. A known classical loop-like process is shown to lie outside both the fixed-sequence set and the larger flexible set, while an explicit flexible process lies inside the flexible set but outside the fixed one; noise-robustness numbers put a precise size on the gap, and a noisy version of the loop process becomes indefinite exactly past a specific amount of mixing. The switchable process, dressed with a global past and future, turns out to be a purely extreme process whose indefiniteness lives entirely in the coherence of its control, so that blurring the control returns exactly the ordered mixture of the two sequences. Two results carry over from the two-party work: the flow-based diagnostic, which over-counts in the two-party case, is for many parties neither necessary nor sufficient, catching the switchable process yet blind to the classical loop; and the ordered set obeys the axioms of a reversible resource, so in bulk it is recyclable with no stubborn leftover form while remaining costly one copy at a time. The advance is to show that indefinite order for many parties is genuinely richer than for two, because ordered behaviour there is flexible and dynamical rather than fixed, and the separable set is correspondingly larger; measuring the exact gap between the flexible and fixed sets is a concrete step into the long-open multiparty classification. The paper also sharpens the limits of the flow-based diagnostic, showing it misses classical indefiniteness entirely, and it confirms that the bulk-reversibility story survives the jump to many parties. The switchable process emerges as the right physical target: buildable, genuinely indefinite, yet carrying its indefiniteness cleanly in its control.
Quantum theory permits processes with no definite order of operations, yet the everyday world has a perfectly definite one that everybody agrees on. This paper explains the gap with the same mechanism physics already uses to explain why the world looks classical at all: the environment quietly monitors a system and, in doing so, singles out a preferred set of stable alternatives and stamps redundant copies of the outcome all around. Applied to the order of operations, this monitoring selects definite orders as the surviving, stable possibilities and drives every process toward having a definite order. Because the order is copied into many parts of the surroundings, it becomes objective, a fact that independent observers each read off separately and agree upon. The paper makes the argument in four steps. First, it lets an environment gently blur the order information of the simplest indefinite process and shows that a certificate of indefiniteness weakens and crosses over to zero at a definite time, after which the process is ordered; the ordered set, once reached, is never left again, which is the mark of a genuine selection rule. Second, it proves a selection theorem for the switchable process: a standard criterion picks out the two definite orders as the stable survivors, and does so for any environment that couples through the physical thing that sets the order, not merely for one specially chosen coupling; the resulting blurring turns the process into a plain mixture of the two definite orders. Third, when many independent fragments of the environment each record the order, the order is broadcast redundantly, so it becomes objective in the precise sense that separate observers reading separate fragments all agree without disturbing the process; the order-coherence the process loses is exactly the order-information the environment gains. Fourth, it computes the blurring rate from concrete physical environments and turns it into a sharp observability threshold in terms of mass, separation, surrounding vacuum, and available time, which for proposed gravitational versions of the experiment becomes a crossover mass above which indefinite order could still be seen. The payoff is a physical account of why the large-scale world is causally definite and why observers agree about the order of events: definite causal order is einselected and then redundantly broadcast, exactly as a classical fact is. The paper is careful about scope, distinguishing the moment a process first becomes ordered from the later, fully settled state in which the order has been completely resolved and copied, and noting that macroscopic order-markers sit far inside the definite regime. By tying the disappearance of indefinite order to a computable environmental rate, it converts a foundational puzzle into a concrete experimental threshold that says when indefinite order should, and should not, be observable.
Making causal order definite is not free. A process that holds several orders in superposition is compelled to write into its future a record of which orders it superposed; wiping that record clean to leave a single definite order carries an unavoidable energy price. This paper shows that the price is set entirely by how many orders the process held, not by how strongly indefinite it was, and that it is at least the minimum amount of work physics demands to erase the corresponding amount of information. The paper identifies the entropy carried by the order record as the logarithm of the number of superposed orders, and then applies the classic principle that erasing information costs a minimum amount of work proportional to that entropy. Resetting the order to a definite value therefore dissipates at least that much work, a floor fixed by the order count alone. The paper shows that the environmental monitoring that makes order definite is precisely the process that writes and broadcasts the record: monitoring exports the full record entropy into the surroundings at the monitoring rate, so that afterwards erasing it to keep a single definite order dissipates at least the stated amount. Along the way the order-coherence plays the role of an order parameter for a smooth settling-down of the process, and the paper is careful to establish that this settling is a gentle, mean-field crossover with a finite response and no true critical point. The result puts the emergence of a definite causal order on a thermodynamic footing, and points in the opposite direction to the existing thermodynamics of indefinite order. That line of work asks whether the ordinary laws of heat are bent when order is superposed, and treats indefinite order as a useful resource; here indefinite order is instead a liability that must be paid off, and the question is the cost of removing it. The paper draws its boundaries plainly: the bound is a statement about erasing or resetting the record, not a claim that the blurring itself costs work, and the crossover it describes is mean-field rather than critical. What it delivers is a clean, quantitative price for the everyday fact that the world has a definite causal order.