Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Unitary Width Rank Three Roots

Abstract

Actual unitary width rank three roots 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 (scalar norm surjective).

Lean statement: D5/S3/FiniteGroups/NikolovSegal/Unitary/UnitaryWidthRankThreeRoots.scalar_norm_surjective

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

Source. Repository-derived.

Commentary.

Extend the genuine unit norm surjection to the zero scalar as well.

Definition 1.2 (shortUpper).

Lean statement: D5/S3/FiniteGroups/NikolovSegal/Unitary/UnitaryWidthRankThreeRoots.shortUpper

Formalization. D5/S3/FiniteGroups/NikolovSegal/Unitary/UnitaryWidthRankThreeRoots.shortUpper (✓ std3).

Source. Repository-derived.

Commentary.

The parameterized shortUpper 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.3 (shortUpper matrix).

Lean statement: D5/S3/FiniteGroups/NikolovSegal/Unitary/UnitaryWidthRankThreeRoots.shortUpper_matrix

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

Source. Repository-derived.

Commentary.

The parameterized shortUpper matrix 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.4 (shortUpper positive).

Lean statement: D5/S3/FiniteGroups/NikolovSegal/Unitary/UnitaryWidthRankThreeRoots.shortUpper_positive

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

Source. Repository-derived.

Commentary.

The parameterized shortUpper positive 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.5 (row shortUpper).

Lean statement: D5/S3/FiniteGroups/NikolovSegal/Unitary/UnitaryWidthRankThreeRoots.row_shortUpper

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

Source. Repository-derived.

Commentary.

Exact ordered right multiplication, in all three coordinates.

Theorem 1.6 (row shortLower).

Lean statement: D5/S3/FiniteGroups/NikolovSegal/Unitary/UnitaryWidthRankThreeRoots.row_shortLower

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

Source. Repository-derived.

Commentary.

The parameterized row shortLower 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.7 (rankThree row isotropic).

Lean statement: D5/S3/FiniteGroups/NikolovSegal/Unitary/UnitaryWidthRankThreeRoots.rankThree_row_isotropic

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

Source. Repository-derived.

Commentary.

The parameterized rankThree row isotropic 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.8 (rankThree normalize last).

Lean statement: D5/S3/FiniteGroups/NikolovSegal/Unitary/UnitaryWidthRankThreeRoots.rankThree_normalize_last

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

Source. Repository-derived.

Commentary.

For a nonzero first row coordinate, a single genuine upper short root makes the last coordinate exactly one. Its trace equation is DERIVED from isotropy and the actual scalar norm surjection, including characteristic two.

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