All measurements may be moved to terminal readout

Give a finite history tree height $0$ when its root is a leaf; otherwise give it height one plus the maximum height of its finitely many child subtrees. For height $0$, there is a single empty history, no instrument is applied, and the leaf's terminal POVM is unchanged. Thus the branch-operator invariant holds at height $0$.

Let the root be internal and suppose the invariant holds for all trees of height at most $k$. For each root outcome $a$, [F2] replaces the root instrument and its edge unitary $S_{h,a}$ by a coherent record with the same unnormalized operator $Y_a$ on the child input and the reference, for every input operator $X$, while retaining a separate orthogonal label register $e_a$. The outcome set is finite by [F1].

Each child subtree has height at most $k$, so apply the induction hypothesis to its input operator $Y_a$ with the already retained history labels included in the finite reference. The operator need not be normalized or positive because the invariant is stated for every operator. The child constructions are controlled on the root's observed record; distinct labels occupy orthogonal record subspaces by [F1]–[F2], so the continuations preserve each full-history branch separately and do not merge histories.

By finite induction [F5] from step 1.1 and the preservation argument in step 2.1, every finite history tree has equal measured and coherently deferred unnormalized branch operators for each complete history and every finite reference.

For a leaf history $h$ and terminal outcome $z$, apply the same effect $F_z^h\otimes I_R$ to the equal branch operators from step 3.1 and take traces. This gives equal joint probabilities. The preterminal data-reference outputs conditioned on history $h$ agree after dividing their equal branch operators by the common positive history probability; zero-probability branches are never normalized by [F3]. Equality of the operators for arbitrary $R$ preserves reference correlations. Any required dilation and block controls remain explicit operation-model costs as stated.