IsUnitary
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.
claimA 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 in Recognition Science
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.
scope and limits
- Does not assert existence of any unitary matrix.
- Does not restrict the scalar type α to the complex numbers.
- Does not apply to non-square matrices.
- Does not embed Recognition Science constants such as phi or the integration gap.
formal statement (Lean)
24def IsUnitary (U : Matrix m m α) : Prop :=
proof body
Definition body.
25 U.conjTranspose * U = 1 ∧ U * U.conjTranspose = 1
26
27/-- A matrix is **normal** if it commutes with its conjugate transpose. -/