λEnter Calculus CompanionRegistered manuscripts, kept distinct

Manuscript I@2 · I.tex · section · 85631fa7

Assumption ledger

Introduction and logical scope › Assumption ledger · lines 252–280

Back to manuscript
Declared, not derivedFinite-dimensional qubit kinematics, ordinary tensor composition, global pure states, coherent gates, state sufficiency, normalized outcome laws, pure positive-branch residuals, the structural conditions of Assumption ass:strategy-class, and the five requirements of Definition def:requirements.
Checked syntacticallyThe record transformation is definable and well typed using allocation and CNOT. Every quantum spectator is consumed or returned.
DerivedThe metatheory of the specified calculus; diagonal anchoring from the first four requirements; and, using records, Born laws and destructive projective residual rays for every admissible strategy.

No silent quantum deletion is added to the language. Algebraic partial traces used in proofs are not term-level weakening operations.