Lemma: Exact patch agreement

Two smooth flat completions agreeing on a neighbourhood of $D_f$, with the same ramp, switch there, and the same relevant initial data, give identical observable coefficients. Their restrictions transported by $\iota$ therefore give a well-defined supported presentation of those coefficients on the host.

Proof. At each coefficient order subtract the two flat Cauchy equations. Finite propagation makes their difference zero on the required retained past, successively for coordinates and scalar corrections. The relational formula and the same test then agree. Transport through the chart simply rewrites that same compact pairing.