Theorem: Constructed transport contract

Fix a calibrated source experiment of scale $j$, resolution ${\epsilon }_j$, skeleton ${\Gamma }_j$, physical support $F_j$, declared support $K_j\supseteq F_j$, and labelled acquisition tuple $R_j$. Fix $g\in {\mathsf{P}}_{+}^{\uparrow }$.

For every sufficiently large target scale $n$, the substrate of Section sec:substrate admits a payload-independent realization with the following properties.

1. Its logical complete instrument equals the source complete instrument exactly, as in (eq:logicalidentity), with every untouched reference.

2. Its physical support satisfies

   $$d_{\mathrm{H}}(F_{j\to n},g{F}_j)\le C_g{\epsilon }_j+r_{{\Gamma }_j,j,g}(n),$$

   where one may take

   $$C_g=2L_g,r_{{\Gamma }_j,j,g}(n)={\delta }_{g{{\Gamma }_j}^{\mathrm{mid}},n}⟶0.$$

3. A legal declared target support is

   $$K_{j\to n}=g{K}_j\cup F_{j\to n},$$

   and it obeys

   $$d_{\mathrm{H}}(K_{j\to n},g{K}_j)\le C_g{\epsilon }_j+r_{{\Gamma }_j,j,g}(n).$$

4. For the actual acquisition tuples,

   $$\underset{\alpha }{\max }{d}_c(R_{j\to n,\alpha },g{R}_{j,\alpha })\le C_g{\epsilon }_j+r_{{\Gamma }_j,j,g}(n).$$

5. The corresponding named retained-wire supports obey the same form of estimate. For every matched set of changed payload vertices, the source and target changed-payload footprint unions also obey that form of two-sided Hausdorff estimate.

The coefficient $C_g$ is independent of the source graph's complexity. The threshold and the fine error may depend on the entire fixed finite source.

Proof. Apply Lemma lem:midpoint to the source. Apply $g$ to the resulting causal graph. Since $g$ preserves future causality, Sections sec:routing–sec:schedule construct a legal target realization at every sufficiently large $n$.

The triangle inequality, (eq:transformedmidpoint), and Lemma lem:finegeometry give

This proves (eq:Tphysical).

The set in (eq:declaredtarget) is compact and contains the actual target support. Every point of $g{K}_j$ belongs to it. Every additional point lies in $F_{j\to n}$, hence is within the displayed bound of $g{F}_j\subseteq g{K}_j$. This proves (eq:Tdeclared). It does not assert that the extra declared points are active physical sites.

Each source acquisition lies within ${\epsilon }_j$ of its source payload midpoint. The target acquisition is the actual output event of the corresponding payload map in its hub frame. Lemma lem:finegeometry gives

which is bounded by (eq:Tacquisition).

The same argument applies to individual retained supports. A source payload footprint is within ${\epsilon }_j$ of its midpoint. Its target singleton payload footprint is within the fine error of the transformed midpoint. Taking unions over changed vertices again uses a maximum. Empty changed sets are handled as the unchanged case, without assigning a Hausdorff distance to an empty set.

Theorem thm:identity proves the channel and reference statements. It also proves matched-skeleton naturality.