Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Part IIUnitary Radical Prescribed Product

Abstract

Actual part iiunitary radical prescribed product 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 (actual unitary radical prescribed four batch).

Lean statement: D5/S3/FiniteGroups/NikolovSegal/Unitary/PartIIUnitaryRadicalPrescribedProduct.actual_unitary_radical_prescribed_four_batch

Proof. Machine-checked in Lean as D5/S3/FiniteGroups/NikolovSegal/Unitary/PartIIUnitaryRadicalPrescribedProduct.actual_unitary_radical_prescribed_four_batch (✓ std3). ∎

Source. Repository-derived.

Commentary.

Full actual V* prescribed D Phi PRODUCT in four ordered batches. The four correction tuples (one global tuple) precede EVERY target. Middle, both exceptional root pairs and the noncommutative corner are truly reconstructed from actual unitary witnesses.

Theorem 1.2 (actual uniform unitary radical prescribed product).

Lean statement: D5/S3/FiniteGroups/NikolovSegal/Unitary/PartIIUnitaryRadicalPrescribedProduct.actual_uniform_unitary_radical_prescribed_product

Proof. Machine-checked in Lean as D5/S3/FiniteGroups/NikolovSegal/Unitary/PartIIUnitaryRadicalPrescribedProduct.actual_uniform_unitary_radical_prescribed_product (✓ std3). ∎

Source. Repository-derived.

Commentary.

Chosen positive length/cutoff BEFORE ALL fields/ranks/diagonal-SIMILITUDE/field tuples. ONE actual SU inner correction precedes every FULL radical target; ordered exact-length commutator VALUES, actual V* witnesses and every original positive divisor power are retained. Whole SU/bare classification are further obligations.

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.

References