UnitaryOperator
plain-language theorem explainer
UnitaryOperator defines the type of n-by-n complex matrices U satisfying U U† = I. Researchers deriving quantum mechanics from ledger conservation in Recognition Science cite this when establishing that time evolution preserves probabilities and norms. The declaration is a direct structure definition with a matrix field and the algebraic unitarity condition.
Claim. A unitary operator on an $n$-dimensional complex vector space is a matrix $U$ in $M_n(ℂ)$ such that $U U^† = I$, where $†$ denotes the conjugate transpose.
background
The QFT.Unitarity module derives quantum unitarity from ledger conservation, with the module documentation stating that the ledger is a conserved quantity implying information preservation and therefore U†U = UU† = I. This structure supplies the evolution operator whose norm-preserving property is asserted in the downstream theorem unitary_preserves_norm. The module imports Constants, Cost, and EightTick, placing the definition inside the Recognition Science setting where ledger rules replace the usual postulates of quantum mechanics.
proof idea
The declaration is introduced directly as a structure definition containing the matrix field and the is_unitary predicate. No lemmas or tactics are applied; it functions as the foundational type for later statements on probability conservation.
why it matters
This definition supplies the mathematical object required by the downstream theorem unitary_preserves_norm, which records that unitary evolution preserves the norm of quantum states. It occupies the central slot in the QFT-009 derivation of unitarity from ledger conservation, as described in the module documentation and the associated paper 'Information Conservation as the Origin of Unitarity'. Within the Recognition Science framework it supports the claim that information conservation forces the reversibility and probability preservation characteristic of quantum time evolution.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.