IndisputableMonolith.Support.MatrixProperties
This module supplies definitions for unitary and normal matrix properties in the Recognition Science support layer. It is imported by the PMNS.Types module to enable mixing weight calculations via the Born rule on ladder steps. The core definition states that a matrix is unitary when it serves as both left and right inverse to its conjugate transpose. No theorems are proved here; the module consists entirely of foundational declarations.
claimA matrix $U$ is unitary when $U U^dagger = I = U^dagger U$. A matrix $N$ is normal when it commutes with its conjugate transpose, $N N^dagger = N^dagger N$.
background
The module IndisputableMonolith.Support.MatrixProperties imports Mathlib and introduces two sibling definitions: IsUnitary and IsNormal. IsUnitary encodes the property that a matrix is both a left- and right-inverse of its conjugate transpose. These declarations sit in the Support domain and are used downstream to handle linear-algebraic structures appearing in physics models.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module feeds IndisputableMonolith.Physics.PMNS.Types, whose doc states that the PMNS mixing weights follow the Born rule over the ladder steps with Weight W_ij = exp(-Δτ_ij * J_bit) = φ^-Δτ_ij. It supplies the matrix properties required for unitary transformations in that context.
scope and limits
- Does not prove any theorems about eigenvalues or spectra.
- Does not specify matrix dimensions or explicit entries.
- Does not reference the forcing chain T0-T8 or RCL.
- Does not define J-cost, defectDist, or the phi-ladder.