Disagreement Ledger and Cascade Containment for One-Agent-Moved Reconstructions
lemmaProbabilitylem:one-agent-move-ledger-2026aAdopt the setting, notation, and hypotheses of Shared-Clock Coupling of One-Agent-Moved Reconstructions: the controlled -agent dynamics with transition-rate family on states with rate bound and Lipschitz constant , the horizon , the driving system with transition clocks , the policy , the moved agent and the moved initial states of claim 1 of One-Agent-Move Ratio of the Record Density Kernel (which agree with the original initial states off ), the observation record space , the two fixed reconstruction data sets with reconstructed state paths , and domains , , the record-frozen control paths , and the reconstructed transition consumed times , . Assume additionally the transition-rate floor: a real with for all states , all , and all in the probability simplex . Fix and write for the intersection of the probability-one events of claim (d) of Measurable Reconstruction of the Controlled N-Agent Dynamics from Observation Records, at every point of which and the two reconstructed collections are solutions of the controlled dynamics for the record-frozen policy , on the original and on the moved driving system respectively --- two driving systems on the same probability space sharing the same clocks and differing only in the initial state of agent .
Fix an agent . For a transition label of agent (an ordered pair of distinct states), write , , , and define the reconstructed counters and , the evaluations of the counting path of the clock at the consumed levels. Define pathwise, for : the frontier consumed time ; the frontier count ; and the gap . Say that the label has a frontier crossing at if for every . The dependence of all of these objects on and on is suppressed throughout.
Fix and consider the disagreement set ; by claim 1 below it is the union of a finite, possibly empty, family of maximal nonempty subintervals (its connected components), each containing its left endpoint, called its onset, and the two state paths agree, and are constant, on a left neighbourhood of every onset. The length of an interval is the difference of its supremum and its infimum. Call such a maximal interval clean if exactly one of the two state paths jumps at its onset (both paths being constant on a left neighbourhood of and piecewise constant, jumping at means differing at from the value on a left neighbourhood); for a clean interval, with the common value of both paths on a left neighbourhood of , the jumping solution is called leading and the other trailing, the leading transition at is for some state , the label is the onset clock, and the onset level is the value of the leading -consumed time at . Call a clean interval ordered if the trailing -consumed time at is strictly less than . Let denote the set of times with , where is the onset and the supremum of the interval , at which some transition counter of agent jumps in at least one of the two solutions (a finite set, by claim 1); note that includes the time at which the interval ends by a counter jump, when it so ends. Call the interval bad if one of the following holds: (i) it is not clean; (ii) it is clean but not ordered; (iii) it is clean and ordered, , and it is not the case that at (a minimum, by claim 1) exactly one counter jump occurs among the two solutions, namely a jump of the trailing solution's onset-clock counter. The witness of a bad interval is its onset in cases (i) and (ii), and in case (iii), case (iii) being understood to apply only when (i) and (ii) do not.
Then at every the following hold.
1. (Structure) Each transition counter of agent in either solution is nondecreasing, right-continuous, integer-valued, and has finitely many jumps in , each of unit size, and in each solution at most one transition counter of agent jumps at any given time; both state paths of agent are piecewise constant with finitely many jumps. The disagreement set of agent is the union of a finite, possibly empty, family of maximal nonempty intervals; distinct maximal intervals are separated, each contains its left endpoint, every onset is strictly positive, and the two state paths agree, and are constant, on a left neighbourhood of every onset. Each frontier count is nondecreasing and right-continuous with jumps of unit size, and the label has a frontier crossing at exactly when jumps at . Finally, the number of maximal intervals satisfies , where , the sum over ordered pairs of distinct states.
2. (Resolution) Every maximal interval that is not bad is clean and ordered and, with onset and onset clock , has length at most . Every clean ordered interval has a frontier crossing of its onset clock at its onset; and for every clean ordered interval with onset and onset clock , and every time in the interval such that no transition counter of agent jumps in either solution at any time of , one has .
3. (Cascade containment) If some bad interval of agent has witness at most , then there are times and transition labels , of agent such that has a frontier crossing at , has a frontier crossing at , , and .
Loading…
Prerequisites
No prerequisites tracked.
Dependents
No dependents yet.
Dependent proofs
No dependent proofs yet.
No relations recorded yet.