Diagonal Defect Across Three Scales

Abstract

Coherent projections through an intermediate scale obey the Lipschitz diagonal-defect bound.

Theorem 1.1 (Diagonal scale defects compose).

$$\begin{gathered} \forall S:\mathrm{Type},[\mathrm{Preorder}(S)],T,U:S\to \mathrm{Type},k,i,j:S,E:T_j,L:\mathrm{NNReal}, \\ [\mathrm{PseudoMetricSpace}(U_i)],[\mathrm{PseudoMetricSpace}(U_k)],k\le i\le j,P_{j,i}:T_j\to T_i,P_{i,k}:T_i\to T_k,P_{j,k}:T_j\to T_k,Q_{j,i}:U_j\to U_i,Q_{i,k}:U_i\to U_k,Q_{j,k}:U_j\to U_k,Delt{a}_j:T_j\to U_j,Delt{a}_i:T_i\to U_i,Delt{a}_k:T_k\to U_k,P_{j,k}=P_{i,k}\circ P_{j,i}\wedge Q_{j,k}=Q_{i,k}\circ Q_{j,i}\wedge \mathrm{LipschitzWith}\left(L,Q_{i,k}\right)\Rightarrow \\ \mathrm{naturalityDefect}\left(P_{j,k},Q_{j,k},Delt{a}_j,Delt{a}_k,E\right)\le L\cdot \mathrm{naturalityDefect}\left(P_{j,i},Q_{j,i},Delt{a}_j,Delt{a}_i,E\right)+ \\ \mathrm{naturalityDefect}\left(P_{i,k},Q_{i,k},Delt{a}_i,Delt{a}_k,P_{j,i}(E)\right). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S0/Diagonal/Naturality/ScaleDefectComposition.diagonal_scale_defect_comp_le (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let k <= i <= j be three scales. Each scale has a table carrier T_s, an output carrier U_s, and a diagonal map Delta_s. The table projections P and output projections Q are typed separately.

The direct projections are publicly required to equal the composites P_(i,k) after P_(j,i) and Q_(i,k) after Q_(j,i). Output carriers at i and k carry the pseudometrics used by the three defects.

If Q_(i,k) is L-Lipschitz, insert Q_(i,k) Delta_i P_(j,i)(E) between the endpoints. The metric triangle inequality and the Lipschitz distance bound give L times the j-to-i defect plus the i-to-k defect at P_(j,i)(E).

The pointwise defect is imported from the frozen diagonal-naturality family and is exactly dist(Q Delta(E), Delta(P(E))). Pinned Mathlib supplies dist_triangle and LipschitzWith.dist_le_mul.

References

• Truth anchor: D5/S0/Diagonal/Naturality/ScaleDefectComposition.diagonal_scale_defect_comp_le
• Dependency: D5/S0/Diagonal/Naturality/NaturalityDefectComposition