Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Part IIUnitary Radical Boundary Field Product

Abstract

Actual part iiunitary radical boundary field 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.

Definition 1.1 (axis).

Lean statement: D5/S3/FiniteGroups/NikolovSegal/Unitary/PartIIUnitaryRadicalBoundaryFieldProduct.axis

Formalization. D5/S3/FiniteGroups/NikolovSegal/Unitary/PartIIUnitaryRadicalBoundaryFieldProduct.axis (✓ std3).

Source. Repository-derived.

Commentary.

The parameterized axis statement describes the actual unitary geometry or prescribed ordered-product construction. Its Lean telescope retains every field, rank, involution, input and equality hypothesis shown.

Theorem 1.2 (actual unitary radical boundary field product).

Lean statement: D5/S3/FiniteGroups/NikolovSegal/Unitary/PartIIUnitaryRadicalBoundaryFieldProduct.actual_unitary_radical_boundary_field_product

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

Source. Repository-derived.

Commentary.

ONE genuine unitary torus tuple precedes ALL targets. Actual commutator VALUES reconstruct the chosen exceptional row, vanish on ALL other noncorner rows, and retain the real ordered corner. Both boundary orientations and all original positive s|q are included.

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