IsUnitary
plain-language theorem explainer
A matrix U is unitary when its conjugate transpose serves as both left and right inverse to the identity. Neutrino mixing analyses in the PMNS sector cite this predicate to enforce the algebraic unitarity condition. The definition is the direct conjunction of the two matrix equations without further hypotheses.
Claim. A matrix $U$ over a field or ring is unitary when $U^dagger U = I$ and $U U^dagger = I$.
background
The module Support.MatrixProperties supplies lightweight, project-local predicates for unitary and normal matrices. These avoid version differences in Mathlib by using the standard algebraic conditions: unitary requires both $U^* U = I$ and $U U^* = I$, while normal requires only that $U^*$ commutes with $U$. The local setting is purely algebraic and independent of Recognition Science units or forcing chains.
proof idea
The definition is a direct conjunction of the two matrix equations for left and right inverses under conjugate transpose.
why it matters
This definition supplies the unitary predicate required by the PMNSUnitarity structure, which adds the further condition that squared moduli match the framework weight tensor. It therefore anchors the algebraic side of the three-generation mixing problem inside the D = 3 sector of the Recognition Science chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.