IsUnitary
plain-language theorem explainer
Defines the predicate for a square matrix U to be unitary when its conjugate transpose is both a left and right inverse of U. Physicists constructing the PMNS mixing matrix in the Recognition Science framework cite this predicate to enforce the required algebraic unitarity. The definition consists of a direct conjunction of the two matrix equations with no lemmas or tactics applied.
Claim. A square matrix $U$ over a field or ring $α$ is unitary when $U^† U = I$ and $U U^† = I$, where $†$ denotes the conjugate transpose and $I$ is the identity matrix.
background
The module supplies lightweight, version-stable predicates for matrix properties that replace or supplement Mathlib's Matrix.IsUnitary and Matrix.IsNormal. The unitary condition is the standard algebraic requirement that the conjugate transpose acts as a two-sided inverse. Upstream results include the RS-native gauge U (tau0 = 1 tick, ell0 = 1 voxel, c = 1) and the active edge count A = 1, which fix the dimensional and scaling conventions used throughout the framework.
proof idea
The definition is a direct one-line algebraic statement that conjoins the left-inverse and right-inverse conditions using matrix multiplication and conjugate transpose from Mathlib. No lemmas are invoked and no tactics are required.
why it matters
This predicate is the algebraic prerequisite for the PMNSUnitarity structure, which adds the further requirement that the squared moduli match the phi-ladder weight tensor. It therefore anchors the unitarity constraint inside the D = 3 spatial setting of the Recognition framework and the eight-tick octave. The parent result is the PMNS unitarity forcing, whose existence claim remains quarantined while the unitarity component itself is certified here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.