Abstract

We characterize the destructive computational-basis measurement primitive of a fixed strictly linear quantum lambda calculus. The admissible strategies are state sufficient, have normalized outcome laws, and assign pure conditional residuals to positive-probability branches. The argument separates two logical layers. First, Born probabilities and destructive projective update define a concrete calculus with type safety, a syntactic linear step bound, observational confluence, circuit adequacy, semantic no-cloning, and internal no-signaling. Second, only the measurement transition is left unknown. Composability, no-signaling, nullity, continuity, and a typed record equation are satisfied by the Born strategy and uniquely determine it within the stated class. Two independent finite constructions establish diagonal anchoring without the record equation. Whole-register records then determine coherent outcome laws, composability determines partial readout, and branch-specific continuation tests determine residual rays. We also prove resource-budgeted stability estimates and derive mixed-state, adaptive, and finite-instrument consequences. A static appendix constructs positive non-Born marginal assignments and exhibits their failure of operational nullity. Later record, decoder, instrument, and cutoff interfaces are kept separate from the premises of primitive uniqueness.