Write Tra for the consumed clock time of a generic clock label a (a triple (i,σγ) or a pair (i,υ)), Ya for the corresponding clock, and Y^a for the residual clock of the statement. Recall from Solution of the Controlled N-Agent Dynamics that the consumed clock times are defined on all of Ω, vanish off the regular event, and satisfy Tra≤βˉr with βˉ=max(B,B~); by part (iv) of Existence, Uniqueness, and Regularity for the Controlled N-Agent Dynamics each Tra is Frsys-measurable.
Step 1: pathwise part of (a). For every ω and every clock, u↦Y^ua=YTra+ua−YTraa starts at 0, is nondecreasing, integer-valued, right-continuous, and has unit jumps, all inherited from the counting path of Ya; so every residual path is a counting path.
Step 2: grid approximation. Fix δ>0. For each clock let Ja be the smallest nonnegative integer with Tra≤Jaδ; then Ja≤⌈βˉr/δ⌉, and the events Cj={Ja=ja for all a}, over the finitely many integer vectors j, partition Ω and lie in Frsys, since each Tra is Frsys-measurable. For an integer vector k write Ck′={Tra≤kaδ for all a} and
Hk=σ(ς01,…,ς0N; Yua, 0≤u≤kaδ, all a),
so that Hk⊆Hj whenever k≤j componentwise. By the clock-reading bound (vi) with caps kaδ, each Ck′ agrees up to a null event with an event of Hk. Since
Cj=Cj′∖a⋃Cj−ea′
(where j−ea decrements the a-th cap; the set subtracted for ja=0 is empty), the cell Cj agrees up to a null event with an event Gj∈Hj. Moreover, for F∈Frsys, the clock-reading bound with caps jaδ gives H′∈Hj with F∩Cj′ equal to H′∩Cj′ up to a null event; intersecting with Cj⊆Cj′ and replacing Cj by Gj,
F∩Cj agrees up to a null event with HjF:=H′∩Gj∈Hj,soP(HjF)=P(F∩Cj).
Define the grid residuals Y^ua,δ=YJaδ+ua−YJaδa, which on Cj equal Yjaδ+ua−Yjaδa. For fixed j, the family of σ-algebras consisting of Hj together with σ(Yjaδ+ua−Yjaδa:u≥0), one per clock, is independent: the family consisting of σ(ς01,…,ς0N) and the full clock σ-algebras is independent by N-Agent Driving System, within each clock the pre-jaδ σ-algebra and the shifted-increment σ-algebra are independent, which we check as follows. The lemma Increments Are Independent of the Natural Filtration Past gives, for any s<t, that the single increment Yta−Ysa is independent of the natural filtration of Ya up to time s; it does not by itself cover the whole shifted σ-algebra, so we build the latter from finitely many increments. Fix 0=u0<u1<⋯<up, nonnegative integers m1,…,mp, an event E of the σ-algebra generated by the variables Yua with u≤jaδ, and set Aq={Yjaδ+uqa−Yjaδ+uq−1a=mq}. The event E∩A1∩⋯∩Ap−1 lies in the natural filtration of Ya up to time jaδ+up−1, so the cited lemma applied at that time gives P(E∩A1∩⋯∩Ap)=P(E∩A1∩⋯∩Ap−1)P(Ap); descending induction on p yields P(E∩⋂qAq)=P(E)∏qP(Aq). The sets ⋂qAq, together with Ω and ∅, form a π-system generating σ(Yjaδ+ua−Yjaδa:u≥0), so Dynkin's Pi-Lambda Theorem upgrades the displayed factorization to independence of the two σ-algebras. The two levels then combine by factorizing P(D0∩⋂a(Pa∩Ra))=P(D0)∏aP(Pa∩Ra)=P(D0)∏aP(Pa)P(Ra) over the generating intersections; these intersections form a π-system generating the joint σ-algebra of the family, so Dynkin's Pi-Lambda Theorem again upgrades the factorization to independence of the whole family; each shifted process is a homogeneous Poisson process with rate 1 (independent increments and Poisson increments are preserved by a deterministic shift).
Step 3: the limit identity. Let 0=u0<u1<⋯<up, let mqa be nonnegative integers (q∈{1,…,p}, finitely many clocks), write π(μ;m)=e−μμm/m! for the Poisson probabilities, and fix F∈Frsys. Take δ=δn=2−n. The caps Jaδn decrease to Tra pointwise as n→∞ (they lie in [Tra,Tra+δn)), so by right-continuity of the clock paths, for every ω and every u,
Y^ua,δn⟶Y^ua(n→∞),
and since all values are integers the corresponding indicator variables converge pointwise. For each fixed n, partitioning by the cells, replacing F∩Cj by HjF (a null modification, changing no expectation), and using that on Cj the grid-residual indicator product is a function of the shifted processes of the cell while HjF∈Hj — but noting that the indicator product must first be rewritten cellwise, 1Cj∏1{⋯}=1Cj∏1{(Yjaδ+uqa−Yjaδa)−(Yjaδ+uq−1a−Yjaδa)=mqa}, and then 1Cj replaced by 1Gj up to a null event — the independence of Step 2 gives
E[1F∩Cja,q∏1{Y^uqa,δn−Y^uq−1a,δn=mqa}]=P(HjF)a,q∏π(uq−uq−1;mqa).
Summing over j and using ∑jP(HjF)=∑jP(F∩Cj)=P(F), then letting n→∞ with dominated convergence,
E[1Fa,q∏1{Y^uqa−Y^uq−1a=mqa}]=P(F)a,q∏π(uq−uq−1;mqa).
Step 4: conclusion. Taking F=Ω and one clock at a time, the increments of Y^a over any finite partition 0=u0<u1<⋯<up anchored at 0 are independent with the Poisson distributions of parameters uq−uq−1 (the joint probability mass function factorizes into the required product for every such partition, and events involving the increments of integer-valued variables are unions of such atoms). For times 0<v1<⋯<vp not anchored at 0, apply this to the partition 0<v1<⋯<vp and sum the resulting product formula over all values of the leading increment Y^v1a−Y^0a, whose Poisson probabilities sum to 1; this marginalization gives the same factorization and the same Poisson laws for the increments over v1<⋯<vp. Moreover Y^0a=0; with Step 1 this proves (a): each residual clock is a homogeneous Poisson process with rate 1 all of whose paths are counting paths.
For (b): for each clock, the collection of events {Y^u1a=w1,…,Y^upa=wp} over finite time sets and integer values, together with Ω and ∅, is a π-system generating σ(Y^ua:u≥0) (the variables are integer-valued, so these cylinder atoms generate). Step 3 shows that for every F∈Frsys and every choice of one such event Ea per clock (finitely many clocks, the remaining ones taken to be Ω),
P(F∩a⋂Ea)=P(F)a∏P(Ea),
since P(Ea) is exactly the corresponding product of Poisson probabilities by (a). Fixing all but one entry and letting the remaining entry range over a π-system, Dynkin's π-λ theorem upgrades each π-system in turn to the generated σ-algebra, one at a time; after finitely many applications this yields the factorization for arbitrary events from Frsys and from the residual clock σ-algebras, which is the asserted independence of the family. The final assertion of the statement follows since the time-r states are Frsys-measurable by part (iv) of Existence, Uniqueness, and Regularity for the Controlled N-Agent Dynamics, so all requirements of N-Agent Driving System hold for the initial states σr1,…,σrN and the residual clocks. ■