Theorem: Complete finite adaptive composition

Every certificate of Definition def:certificate defines the complete history channel

It is CPTP, including every untouched reference.

For a finite reported label $y=g(a)$, the selective output is the sum of the corresponding leaf blocks. Every failure leaf remains in that sum or in an explicitly retained failure class.

The construction uses no consumed quantum name as a later input.

Proof. At a leaf, the remaining channel is the declared terminal output map, which may be included as a final node. Suppose every child continuation is complete. Pull its Kraus completeness identity back through the parent maps:

Backward induction over the finite tree proves the second identity in (eq:completehistory). The first expression is therefore completely positive and trace preserving.

Tensor each path map with $I_E$; the same completeness calculation proves the reference statement. Classical coarse-graining sums CP blocks and preserves their total trace. The declared failure convention excludes omitted leaves.

The type checks and Definition def:fresh prevent any later factor from referring to a consumed name.