Deterministic Causal Online Processes

Definition

pd_online_trace

by wenxinzhang · Aug 12, 2026 · Mathlib c5ea003 (Lean v4.30.0)

competitive-analysisonline-algorithmsprimal-dualtransition-systems

This module provides a minimal interface for deterministic online algorithms.

An online process consists of request, state, and decision types, an initial state $s_0$ , and a transition map $\mathrm{step}\colon S\times R\to S\times D$ that sees only the current state and the newly arriving request. For a finite request list $r_1,\dots,r_n$ the module defines the state reached after processing the list, the complete trace of post-transition states and decisions, and the list of decisions alone; each is available both from the designated initial state and from an arbitrary starting state.

The module proves two append laws: for all request lists $H$ and $T$ ,

\mathrm{stateAfter}(s,\,H \mathbin{+\!\!+} T) \;=\; \mathrm{stateAfter}\bigl(\mathrm{stateAfter}(s,H),\,T\bigr),

and the corresponding decomposition of traces. These laws express causality — an algorithm cannot inspect the future of the request stream — and they are the induction interface used by the load-balancing analysis to reason about prefixes of the arrival sequence.

Formalization Note Failure, rejection, and certificates are not built into the interface; they are represented in the user-chosen state and decision types. The two append laws are proved inside this definition module, so importing it makes them available without a separate theorem node.

Definition code

import Mathlib.Data.List.Basic

/-!
A deliberately small deterministic interface for online algorithms.

The transition sees only the current state and the newly arrived request.  Consequently every
value produced by `traceFrom` is causal by construction; an algorithm cannot inspect the suffix
of the request list.
-/

namespace PrimalDual.Online

/-- A deterministic online process.  Failure, rejection, and certificates can be represented in
the user-chosen `State` and `Decision` types rather than being built into the common interface. -/
structure Process (Request State Decision : Type*) where
  initial : State
  step : State → Request → State × Decision

namespace Process

variable {Request State Decision : Type*}

/-- The state reached after processing a finite request sequence, starting from `state`. -/
def stateAfterFrom (process : Process Request State Decision) : State → List Request → State
  | state, [] => state
  | state, request :: requests =>
      stateAfterFrom process (process.step state request).1 requests

/-- The state reached from the process's designated initial state. -/
def stateAfter (process : Process Request State Decision) (requests : List Request) : State :=
  process.stateAfterFrom process.initial requests

/-- The post-transition state and decision produced at every arrival. -/
def traceFrom (process : Process Request State Decision) :
    State → List Request → List (State × Decision)
  | _, [] => []
  | state, request :: requests =>
      let next := process.step state request
      next :: traceFrom process next.1 requests

/-- The complete post-transition trace from the designated initial state. -/
def trace (process : Process Request State Decision) (requests : List Request) :
    List (State × Decision) :=
  process.traceFrom process.initial requests

/-- Decisions produced from an arbitrary starting state. -/
def decisionsFrom (process : Process Request State Decision) (state : State)
    (requests : List Request) : List Decision :=
  (process.traceFrom state requests).map Prod.snd

/-- Decisions produced from the designated initial state. -/
def decisions (process : Process Request State Decision) (requests : List Request) :
    List Decision :=
  process.decisionsFrom process.initial requests

/-- Processing a prefix and then a suffix is the same as processing their concatenation. -/
theorem stateAfterFrom_append (process : Process Request State Decision) (state : State)
    (headRequests tailRequests : List Request) :
    process.stateAfterFrom state (headRequests ++ tailRequests) =
      process.stateAfterFrom (process.stateAfterFrom state headRequests) tailRequests := by
  induction headRequests generalizing state with
  | nil => rfl
  | cons request rest ih =>
      simp only [List.cons_append, stateAfterFrom]
      exact ih (process.step state request).1

/-- A trace over a concatenation is the prefix trace followed by the suffix trace started from
the prefix's final state.  This is the reusable causal-prefix law for later online proofs. -/
theorem traceFrom_append (process : Process Request State Decision) (state : State)
    (headRequests tailRequests : List Request) :
    process.traceFrom state (headRequests ++ tailRequests) =
      process.traceFrom state headRequests ++
        process.traceFrom (process.stateAfterFrom state headRequests) tailRequests := by
  induction headRequests generalizing state with
  | nil => rfl
  | cons request rest ih =>
      simp only [List.cons_append, traceFrom, stateAfterFrom, List.cons_append]
      exact congrArg (process.step state request :: ·) (ih (process.step state request).1)

end Process

end PrimalDual.Online

Source

Niv Buchbinder and Joseph (Seffi) Naor, The Design of Competitive Online Algorithms via a Primal--Dual Approach, https://www.tau.ac.il/~nivb/download/pd-survey.pdf, Section 2.3 (Online Computation), pp. 107--109; applied to irrevocable job assignments in the unrelated-machines problem discussed in Chapter 8.

Read-back

What the Lean code literally says, in plain math · gpt-5

PrimalDual.Online.Process. For three explicit type parameters $\mathsf{Request}$ , $\mathsf{State}$ , and $\mathsf{Decision}$ , each lying in an arbitrary universe and subject to no typeclass assumptions, this declaration defines a process value to consist of an element $\mathsf{initial}\in\mathsf{State}$ and a total function $\mathsf{step}$ which, for every $s\in\mathsf{State}$ and $r\in\mathsf{Request}$ , returns one ordered pair in $\mathsf{State}\times\mathsf{Decision}$ . It imposes no equations or additional properties on these fields. Supplying a process necessarily supplies an inhabitant of $\mathsf{State}$ ; thus no process value exists when $\mathsf{State}$ is empty. If $\mathsf{Request}$ is empty, every request list is empty and the step function has no actual request input; if $\mathsf{Request}$ is inhabited while $\mathsf{Decision}$ is empty, no process value can exist.

PrimalDual.Online.Process.stateAfterFrom. For implicitly universally quantified types $\mathsf{Request}$ , $\mathsf{State}$ , and $\mathsf{Decision}$ , with no typeclass assumptions, and for an explicit process $P$ , this declaration defines a function of an explicit starting state $s_0\in\mathsf{State}$ and an explicit finite request list. On the empty list it returns $s_0$ . On a list $[r_1,\ldots,r_n]$ , it recursively sets $(s_i,d_i)=P.\mathsf{step}(s_{i-1},r_i)$ for $i=1,\ldots,n$ and returns $s_n$ , discarding every $d_i$ ; equivalently, after the first request it recurses on the remaining list from the first coordinate of the step result. This recursion is structural on the request list and covers all finite lists, including the empty list. The supplied process already contains an initial state even though this definition uses the separately supplied starting state.

PrimalDual.Online.Process.stateAfter. For implicitly universally quantified types $\mathsf{Request}$ , $\mathsf{State}$ , and $\mathsf{Decision}$ , with no typeclass assumptions, an explicit process $P$ , and an explicit finite request list $[r_1,\ldots,r_n]$ , this declaration starts with $s_0=P.\mathsf{initial}$ , recursively sets $(s_i,d_i)=P.\mathsf{step}(s_{i-1},r_i)$ , and returns $s_n$ , discarding the decisions. In particular, for the empty request list it returns exactly $P.\mathsf{initial}$ . The declaration adds no hypothesis on the list or on the process fields.

PrimalDual.Online.Process.traceFrom. For implicitly universally quantified types $\mathsf{Request}$ , $\mathsf{State}$ , and $\mathsf{Decision}$ , with no typeclass assumptions, and for an explicit process $P$ , this declaration defines a function of an arbitrary explicit starting state $s_0$ and an explicit finite request list. For the empty list and every starting state, it returns the empty list. For $[r_1,\ldots,r_n]$ , it recursively computes $(s_i,d_i)=P.\mathsf{step}(s_{i-1},r_i)$ and returns exactly $[(s_1,d_1),\ldots,(s_n,d_n)]$ : the first output is the complete step result on $s_0,r_1$ , and the remaining trace is generated from $s_1$ and the remaining requests. Thus the starting state itself is not an output entry, while each request contributes one post-step state-and-decision pair; the recursion is structural and includes $n=0$ .

PrimalDual.Online.Process.trace. For implicitly universally quantified types $\mathsf{Request}$ , $\mathsf{State}$ , and $\mathsf{Decision}$ , with no typeclass assumptions, an explicit process $P$ , and an explicit finite request list $[r_1,\ldots,r_n]$ , this declaration sets $s_0=P.\mathsf{initial}$ , recursively computes $(s_i,d_i)=P.\mathsf{step}(s_{i-1},r_i)$ , and returns $[(s_1,d_1),\ldots,(s_n,d_n)]$ . It does not include $P.\mathsf{initial}$ as a trace entry. For the empty request list it returns the empty list, and it imposes no nonemptiness or other hypotheses.

PrimalDual.Online.Process.decisionsFrom. For implicitly universally quantified types $\mathsf{Request}$ , $\mathsf{State}$ , and $\mathsf{Decision}$ , with no typeclass assumptions, an explicit process $P$ , an explicit starting state $s_0$ , and an explicit finite request list $[r_1,\ldots,r_n]$ , this declaration recursively computes $(s_i,d_i)=P.\mathsf{step}(s_{i-1},r_i)$ and returns exactly $[d_1,\ldots,d_n]$ , obtained by taking the second coordinate of every pair in the corresponding trace and discarding all recorded post-step states. For the empty request list it returns the empty decision list. No hypothesis is imposed on the starting state or list.

PrimalDual.Online.Process.decisions. For implicitly universally quantified types $\mathsf{Request}$ , $\mathsf{State}$ , and $\mathsf{Decision}$ , with no typeclass assumptions, an explicit process $P$ , and an explicit finite request list $[r_1,\ldots,r_n]$ , this declaration starts from $s_0=P.\mathsf{initial}$ , recursively computes $(s_i,d_i)=P.\mathsf{step}(s_{i-1},r_i)$ , and returns precisely $[d_1,\ldots,d_n]$ . It therefore discards every state component and returns the empty list when the request list is empty, with no further hypotheses.

PrimalDual.Online.Process.stateAfterFrom_append. For implicitly universally quantified types $\mathsf{Request}$ , $\mathsf{State}$ , and $\mathsf{Decision}$ , with no typeclass assumptions, and universally for every explicit process $P$ , starting state $s$ , head request list $H$ , and tail request list $T$ , this theorem asserts the unconditional equality $\mathsf{stateAfterFrom}_P(s,H\mathbin{+\!\!+}T)=\mathsf{stateAfterFrom}_P(\mathsf{stateAfterFrom}_P(s,H),T)$ , where $\mathsf{stateAfterFrom}$ repeatedly replaces the current state by the first coordinate of $P.\mathsf{step}$ on the next request and returns the starting state on an empty list. If $H$ is empty, both sides are the state obtained by processing $T$ from $s$ ; if $T$ is empty, both sides are the state obtained by processing $H$ from $s$ ; if both are empty, both sides equal $s$ . There are no length, nonemptiness, or compatibility hypotheses. For type triples admitting no process value, the universal process binder has no instance.

PrimalDual.Online.Process.traceFrom_append. For implicitly universally quantified types $\mathsf{Request}$ , $\mathsf{State}$ , and $\mathsf{Decision}$ , with no typeclass assumptions, and universally for every explicit process $P$ , starting state $s$ , head request list $H$ , and tail request list $T$ , this theorem asserts the unconditional list equality $\mathsf{traceFrom}_P(s,H\mathbin{+\!\!+}T)=\mathsf{traceFrom}_P(s,H)\mathbin{+\!\!+}\mathsf{traceFrom}_P(\mathsf{stateAfterFrom}_P(s,H),T)$ . Here the trace recursively contains, in order, the complete state-and-decision pair returned by each step, while $\mathsf{stateAfterFrom}_P(s,H)$ is obtained by recursively retaining only each step’s state coordinate; both operations return their respective starting state or empty output on an empty request list. If $H$ is empty, the first trace on the right is empty and the suffix begins from $s$ ; if $T$ is empty, the suffix trace is empty; if both are empty, both sides are empty. There are no hypotheses on either list or on the process fields. For type triples admitting no process value, the universal process binder has no instance.

Human review

Endorsed by Shuze Chen · Aug 19, 2026
Endorsed by wenxinzhang · Aug 19, 2026
Confirmed by the mission captain (proposal self-audit).

View graph