IndisputableMonolith.Support.MatrixProperties
The Support.MatrixProperties module supplies definitions for unitary and normal matrices. It is imported by the PMNS.Types construction in Physics. This is a definition module with no proofs or theorems.
claimA matrix $U$ is unitary when $U^ opbar U = I = U U^ opbar$, where $ opbar$ is the conjugate transpose. A matrix $N$ is normal when $N N^ opbar = N^ opbar N$.
background
The module resides in the Support domain and imports only Mathlib. Its documentation states that a matrix is unitary if it is both a left- and right-inverse of its conjugate transpose. The sibling declarations IsUnitary and IsNormal supply these two properties for use in matrix constructions elsewhere in the framework.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module is imported by IndisputableMonolith.Physics.PMNS.Types, whose documentation states that the PMNS mixing weights follow the Born rule over the ladder steps with $W_{ij} = \phi^{-\Delta au_{ij}}$. It therefore supplies the matrix-algebraic prerequisites for the mixing construction.
scope and limits
- Does not contain any theorems or proofs.
- Does not define concrete matrices used in physics models.
- Does not depend on Recognition Science forcing-chain results.