Manuscript I@2 · I.tex · corollary · 85631fa7
Corollary: Finite adaptive execution
Stability and represented measurements › Mixed states and finite adaptivity · lines 2097–2111 · proof included or linked
I@2#cor:adaptive
Every finite program with a first-order interface in a model of has its Born instrument. Its terminal classical observations are independent of the liberal scheduler.
Proof. Characterization identifies each reached readout's probabilities and positive-branch residuals. Induction on the finite remaining evaluation tree identifies all path maps and reported-output instruments. Scheduler independence follows from Corollary cor:scheduler.