Reason: Proof of the removal-form insertion response lemma: tolerance transfer to the base clock family, cancellation in the exact identity, two second-order Taylor expansions of the label rates, and the window argument for the enlarged clock's discrepancy. Internally reviewed twice.
Proof
Throughout, c=(σ,γ) denotes a label, and for u≥0 we put ν(u)=#{k∈{1,…,m}:uk≤u}, so that p+,c0=pc0+ν and p+,c=pc for c=c0 by the definition of the perturbed clock family in Shared-Clock Point Insertion into the Open-Loop Aggregate Solution: Exact Response Identity, Crude Bound, and Linearisation Defect; ν is nondecreasing with values in {0,…,m}, and ιt=ν(Ct+,c0), ιt−=ν(Ctc0). Three elementary facts are used. (F1) ∣vc∣=2 for every label: vc=δγ−δσ with γ=σ has two coordinates equal to ±1 and the others 0, so ∣vc∣2=2 by claim 1 of Elementary Properties of the Euclidean Norm on Rn; and for vectors y1,…,yn∈Rl and real numbers λ1,…,λn one has ∣∑iλiyi∣≤∑i∣λi∣∣yi∣, by induction on n from claims 6 and 5 of the same lemma. (F2) The simplex is convex: for x,y∈Δl and τ∈[0,1] the point x+τ(y−x) has nonnegative coordinates (1−τ)xγ+τyγ summing to 1, so it lies in Δl; hence for x,y∈Δl and α∈A the segment between (x,α) and (y,α) lies in Δl×A⊆U×V, and the Euclidean distance between these two points is ∣y−x∣ (the control coordinates of the difference vanish). (F3) By condition 1 of Open-Loop Aggregate Solution Driven by Aggregate Transition Clocks each component of Σ, of Σ+ and hence of Y is a finite sum of constants times indicators of subintervals of [0,T], so it is measurable for the trace Borel σ-algebra by claims 1 and 2 of Arithmetic, Absolute Values, and Pointwise Limits of Measurable Real-Valued Functions, and bounded, the points Σs,Σs+∈GN⊆Δl having coordinates in [0,1]; and if F is a real function on U×V that is sequentially continuous on Δl×A, then s↦F(Σs,as) and s↦F(Σs+,as) are measurable by Sequentially Continuous Functions of Measurable Euclidean Maps are Measurable, the components of s↦(Σs,as) and of s↦(Σs+,as) being measurable (the control path by the definition of the open-loop aggregate solution, the state paths as just noted), and they are bounded whenever F is bounded on Δl×A.
Step 1 (Claim 1). Let c∈L and let 0≤u≤u′≤R be real with u′−u≤L. If c=c0 then pc=p+,c, and hypothesis (D+) gives ∣pc(u′)−pc(u)−(u′−u)∣≤D≤D+m. If c=c0 then pc0=p+,c0−ν, so
where the first bracket has absolute value at most D by (D+) and 0≤ν(u′)−ν(u)≤m because ν is nondecreasing with values in {0,…,m}; the triangle inequality for absolute values gives ∣pc0(u′)−pc0(u)−(u′−u)∣≤D+m. Thus p satisfies hypothesis (D) of Shared-Clock Point Insertion into the Open-Loop Aggregate Solution: Exact Response Identity, Crude Bound, and Linearisation Defect with tolerance D+m. All other data of that lemma (p, a, x0, c0, m, the insertion points, R, L, the conflict-freeness of (p,a,x0) and (p+,a,x0)) are unchanged, so its claims 1, 2 and 3 apply with D+m in place of D; substituting D+m for D in the formula for A0 gives exactly A0+. The two bounds stated under the assumption Λ1TA0+<L are claim 2 of that lemma so applied.
Two Taylor expansions. Fix s∈[0,T] and a label c. Apply part (ii) of Multivariate Taylor Expansion with Uniform Second-Order Remainder on the open set W=U×V⊆Rl+m to f=ψc, with the points x=(Σs+,as) and y=(Σs,as), whose segment lies in Δl×A by (F2), and with M2=3K: here h=y−x=(Σs−Σs+,0) has coordinates hi=0 for i>l, so ∑i=1l+m∂iψc(x)hi=gc(Σs+,as)⋅(Σs−Σs+), and ∣h∣=∣Σs−Σs+∣=∣Ys∣/N by (F2) and claim 5 of Elementary Properties of the Euclidean Norm on Rn. This gives
Multiplying by N (note N(Σs−Σs+)=−Ys) and rearranging, N(ψc(Σs+,as)−ψc(Σs,as))=gc(Σs+,as)⋅Ys+ρs+,c, where ρs+,c=N(ψc(Σs+,as)−ψc(Σs,as))−gc(Σs+,as)⋅Ys satisfies ∣ρs+,c∣≤Λ2∣Ys∣2/N≤Λ2(A0+)2/N by claim 1. Applying part (ii) instead with x=(Σs,as) and y=(Σs+,as) (same segment, same M2, now h=(Σs+−Σs,0) with Nh=(Ys,0)) gives likewise N(ψc(Σs+,as)−ψc(Σs,as))=gc(Σs,as)⋅Ys+ρs−,c, where ρs−,c=N(ψc(Σs+,as)−ψc(Σs,as))−gc(Σs,as)⋅Ys satisfies ∣ρs−,c∣≤Λ2(A0+)2/N. Both s↦ρs±,c are bounded (by these estimates) and measurable: s↦ψc(Σs,as) and s↦ψc(Σs+,as) are measurable by the Measurability paragraph, and the dot products are finite sums of products of measurable functions (claims 2 and 3 of Arithmetic, Absolute Values, and Pointwise Limits of Measurable Real-Valued Functions, using the measurability of s↦gc(Σs,as) from claim 1 of Shared-Clock Point Insertion into the Open-Loop Aggregate Solution: Exact Response Identity, Crude Bound, and Linearisation Defect and of s↦gc(Σs+,as) from the previous paragraph).
Discrepancy on the enlarged clock family. For a label c put dtc=p+,c(Ct+,c)−p+,c(Ctc)−(Ct+,c−Ctc). The two levels Ctc and Ct+,c lie in [0,R] and, by claim 1, are at distance at most Λ1TA0+<L, so hypothesis (D+) applied to the window they bound gives ∣dtc∣≤D (when Ct+,c<Ctc, apply (D+) to the window [Ct+,c,Ctc] and note that dtc merely changes sign).
Assembly. Substituting the consumed-time differences into the identity of claim 2,
where dt+=∑cvc(∫[0,t]ρs+,cds+dtc) and where, for each coordinate γ, linearity of the integral gives ∑cvcγ∫[0,t]gc(Σs+,as)⋅Ysds=∫[0,t]∑cvcγgc(Σs+,as)⋅Ysds=∫[0,t](E(Σs+,as)Ys)γds by the definition of E in Shared-Clock Point Insertion into the Open-Loop Aggregate Solution: Exact Response Identity, Crude Bound, and Linearisation Defect. The same substitution with gc(Σs,as) and ρ−,c gives the second identity with dt−=∑cvc(∫[0,t]ρs−,cds+dtc). Finally, by (F1) and the bounds just obtained, ∣dt±∣≤2∑c(Λ2T(A0+)2/N+D)=2l(l−1)(D+Λ2T(A0+)2/N), the set L having l(l−1) elements.