IndisputableMonolith.Support.MatrixProperties
Support module defining standard matrix predicates used by the PMNS sector: unitarity (left and right inverse of the conjugate transpose) and normality. Downstream mixing-matrix types import these so Born-rule ladder weights sit on unitary frames. Content is definitional scaffolding over Mathlib, not a forcing-chain theorem.
claimA square matrix $U$ is unitary when $U^\dagger U = I = U U^\dagger$. A matrix $A$ is normal when $A A^\dagger = A^\dagger A$. The module packages these predicates for later use on mixing matrices.
background
Recognition Science places lepton mixing on a discrete $\phi$-ladder. The PMNS sector treats mixing weights as Born-rule factors $W_{ij} = \varphi^{-\Delta\tau_{ij}}$ over ladder steps, so the underlying frame must be a unitary matrix in the usual sense of quantum mechanics.
This support module sits outside the T0–T8 forcing chain. It only records Mathlib-facing predicates: unitarity (both-sided inverse of the conjugate transpose) and normality (commutation with the adjoint). No RS-native cost $J$, eight-tick structure, or dimension count is proved here.
The sole documented consumer is Physics.PMNS.Types, whose module doc states that PMNS mixing weights follow the Born rule over ladder steps.
proof idea
This is a definition module, no proofs. It introduces named predicates (IsUnitary, IsNormal) as thin wrappers or aliases over standard matrix algebra from Mathlib, so physics modules can state unitarity hypotheses without repeating conjugate-transpose identities.
why it matters in Recognition Science
Feeds the PMNS types layer: mixing matrices and Born-rule ladder weights need a clean unitary predicate before any claim about $\varphi^{-\Delta\tau}$ amplitudes can be stated. Without this support surface, PMNS would either inline Mathlib API or leave unitarity informal.
It does not advance the forcing chain (T5 $J$-uniqueness, T6 $\varphi$, T7 eight-tick, T8 $D=3$) and does not derive $\alpha$ or mass rungs. Its role is infrastructural: keep linear-algebra hygiene out of the physics files that cite the ladder Born rule.
scope and limits
- Does not prove any PMNS angle or mass prediction.
- Does not derive unitarity from Recognition Composition Law or $J$.
- Does not define the $\varphi$-ladder or Born weights themselves.
- Does not address CP phases or experimental bounds on mixing.