{"id":"palomar/PALOMAR-2026-10-06-000011","url":"https://github.com/alialiev78/gs_Lean_formalization/tree/1270ba6cf3050f53a4beb98f0d65ab7459d4494b","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-06-000011-v1.json","repo":"https://github.com/alialiev78/gs_Lean_formalization","tags":["math.DG","math.NA","math.RA","msc:15A23","msc:15B10","msc:53B21","msc:57N35","matrix-factorization","differential-geometry","orthogonal-matrices"],"score":0,"title":"Structured orthogonal and unitary matrices: factorization, geometry and singularities","trust":"high","domain":"math.DG","source":"palomar","authors":["Ali Aliev"],"reviews":0,"subject":"math.DG","summary":"Block-diagonal matrix factors interleaved with fixed coordinate permutations define low-parametric matrix families. This formalization proves orthogonal-factor sufficiency for two and three real layers, its complex unitary analogue, and explicit four-layer counterexamples over both fields. It establishes an exact two-factor cell-rank criterion and real and unitary cosine-sine exhaustion for the (p,2,p) shuffle family. Two-layer images with complete within-layer block sharing, arbitrary overlap and arbitrary fixed carriers have a smooth atlas in the inherited matrix topology, an exact tangent…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-06","reactions":{},"formalized":true,"formalizes":[{"title":"Riemannian Structure and Optimization for a Class of Low-Parametric Orthogonal Matrices","identifier":"arXiv:2609.27982","relationship":"formalizes"}]}