Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Unitary Rank Two Coordinates

Abstract

Actual unitary rank two coordinates 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 (coordinateMatrix).

Lean statement: D5/S3/FiniteGroups/NikolovSegal/Unitary/UnitaryRankTwoCoordinates.coordinateMatrix

Formalization. D5/S3/FiniteGroups/NikolovSegal/Unitary/UnitaryRankTwoCoordinates.coordinateMatrix (✓ std3).

Source. Repository-derived.

Commentary.

Change of basis by diag(τ,1): D⁻¹ A D.

Theorem 1.2 (coordinateMatrix conjugation).

Lean statement: D5/S3/FiniteGroups/NikolovSegal/Unitary/UnitaryRankTwoCoordinates.coordinateMatrix_conjugation

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

Source. Repository-derived.

Commentary.

The parameterized coordinateMatrix conjugation 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 (coordinateMatrix det).

Lean statement: D5/S3/FiniteGroups/NikolovSegal/Unitary/UnitaryRankTwoCoordinates.coordinateMatrix_det

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

Source. Repository-derived.

Commentary.

The parameterized coordinateMatrix det 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 (coordinateMatrix mul).

Lean statement: D5/S3/FiniteGroups/NikolovSegal/Unitary/UnitaryRankTwoCoordinates.coordinateMatrix_mul

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

Source. Repository-derived.

Commentary.

The parameterized coordinateMatrix mul 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 (coordinateMatrix inverse).

Lean statement: D5/S3/FiniteGroups/NikolovSegal/Unitary/UnitaryRankTwoCoordinates.coordinateMatrix_inverse

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

Source. Repository-derived.

Commentary.

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

Definition 1.6 (scaleSL).

Lean statement: D5/S3/FiniteGroups/NikolovSegal/Unitary/UnitaryRankTwoCoordinates.scaleSL

Formalization. D5/S3/FiniteGroups/NikolovSegal/Unitary/UnitaryRankTwoCoordinates.scaleSL (✓ std3).

Source. Repository-derived.

Commentary.

The parameterized scaleSL 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 (coordinateMatrix fixed).

Lean statement: D5/S3/FiniteGroups/NikolovSegal/Unitary/UnitaryRankTwoCoordinates.coordinateMatrix_fixed

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

Source. Repository-derived.

Commentary.

Each entry of the changed SU2 basis lies in the actual fixed subfield.

Definition 1.8 (fixedCoordinateMatrix).

Lean statement: D5/S3/FiniteGroups/NikolovSegal/Unitary/UnitaryRankTwoCoordinates.fixedCoordinateMatrix

Formalization. D5/S3/FiniteGroups/NikolovSegal/Unitary/UnitaryRankTwoCoordinates.fixedCoordinateMatrix (✓ std3).

Source. Repository-derived.

Commentary.

The literal fixed-field coordinate matrix, with membership proved entry by entry.

Theorem 1.9 (fixedCoordinateMatrix coe).

Lean statement: D5/S3/FiniteGroups/NikolovSegal/Unitary/UnitaryRankTwoCoordinates.fixedCoordinateMatrix_coe

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

Source. Repository-derived.

Commentary.

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

Definition 1.10 (toFixedSL).

Lean statement: D5/S3/FiniteGroups/NikolovSegal/Unitary/UnitaryRankTwoCoordinates.toFixedSL

Formalization. D5/S3/FiniteGroups/NikolovSegal/Unitary/UnitaryRankTwoCoordinates.toFixedSL (✓ std3).

Source. Repository-derived.

Commentary.

Actual SU2 → native SL2 over its fixed field.

Definition 1.11 (fromFixedSL).

Lean statement: D5/S3/FiniteGroups/NikolovSegal/Unitary/UnitaryRankTwoCoordinates.fromFixedSL

Formalization. D5/S3/FiniteGroups/NikolovSegal/Unitary/UnitaryRankTwoCoordinates.fromFixedSL (✓ std3).

Source. Repository-derived.

Commentary.

Inclusion into F followed by the inverse actual change of basis.

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