Unitary Inner UNormalization
Abstract
Actual unitary inner unormalization supplies the parameterized matrix, finite-field or ordered-product identities consumed by the whole-SU K5 width and intrinsic prescribed-product proof paths. All original hypotheses and actual carriers are retained; this source provides no oracle for bare automorphism recognition.
Theorem 1.1 (mem specialUnitary iff hermitian).
Lean statement: D5/S3/FiniteGroups/NikolovSegal/Unitary/UnitaryInnerUNormalization.mem_specialUnitary_iff_hermitian
Proof. Machine-checked in Lean as D5/S3/FiniteGroups/NikolovSegal/Unitary/UnitaryInnerUNormalization.mem_specialUnitary_iff_hermitian (✓ std3). ∎
Source. Repository-derived.
Commentary.
The subgroup is the literal determinant-one anti-diagonal Hermitian carrier.
Theorem 1.2 (inner positiveU correction).
Lean statement: D5/S3/FiniteGroups/NikolovSegal/Unitary/UnitaryInnerUNormalization.inner_positiveU_correction
Proof. Machine-checked in Lean as D5/S3/FiniteGroups/NikolovSegal/Unitary/UnitaryInnerUNormalization.inner_positiveU_correction (✓ std3). ∎
Source. Repository-derived.
Commentary.
Every bare actual SU automorphism admits one genuine SU inner correction before all targets. Native finite Sylow conjugacy is applied to the proved literal Sylow, and native normalizer functoriality preserves its actual Borel.
The results concern special-unitary matrix groups over finite fields. Their geometric setting is Nikolov and Segal, On finitely generated profinite groups, II: Products in quasisimple groups, Annals of Mathematics 165 (2007), 239-273, DOI 10.4007/annals.2007.165.239. Prescribed-product statements retain their field-size, rank and automorphism hypotheses.