Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Part II A2GraphSupply

Abstract

Part II A2GraphSupply.

Theorem 1.1 (actual mixed graph root01 product).

Lean statement: D5/S3/FiniteGroups/NikolovSegal/PartIIA2GraphSupply.actual_mixed_graph_root01_product

Proof. Machine-checked in Lean as D5/S3/FiniteGroups/NikolovSegal/PartIIA2GraphSupply.actual_mixed_graph_root01_product (✓ std3). ∎

Source. Repository-derived.

Commentary.

For positive q, M > q(4q+1), and field size greater than 4(4q+1)^q, arbitrary diagonal/field/graph tuples and positive divisors e of q admit nonzero torus parameters and genuine corrections fixed before every first-root target. The correction identity uses H for graph positions and diag2n for the others. Ordered actual root values have exponent (if graph then 2 else 1)*(q/e).

Theorem 1.2 (actual mixed graph root12 product).

Lean statement: D5/S3/FiniteGroups/NikolovSegal/PartIIA2GraphSupply.actual_mixed_graph_root12_product

Proof. Machine-checked in Lean as D5/S3/FiniteGroups/NikolovSegal/PartIIA2GraphSupply.actual_mixed_graph_root12_product (✓ std3). ∎

Source. Repository-derived.

Commentary.

Under the same positive-q, M > q(4q+1), field-size > 4(4q+1)^q and positive-divisor conditions, arbitrary mixed graph tuples cover the second simple root. Nonzero torus parameters and corrections precede every target, using tau(H) at graph positions and the second-root diag2n elsewhere. The ordered exponent remains (if graph then 2 else 1)*(q/e).

Theorem 1.3 (actual mixed graph central product).

Lean statement: D5/S3/FiniteGroups/NikolovSegal/PartIIA2GraphSupply.actual_mixed_graph_central_product

Proof. Machine-checked in Lean as D5/S3/FiniteGroups/NikolovSegal/PartIIA2GraphSupply.actual_mixed_graph_central_product (✓ std3). ∎

Source. Repository-derived.

Commentary.

For positive q, M > q(4q+1), and field size greater than 4(4q+1)^q, arbitrary diagonal/field/graph tuples and positive divisors e of q admit one correction tuple before every central-root target. Ordered actual central transvection values have the original exponent q/e, including graph positions.

Nikolov and Segal, On finitely generated profinite groups, I: Strong completeness and uniform bounds, Annals of Mathematics 165 (2007), 171-238, DOI 10.4007/annals.2007.165.171, Section 10, Proposition 10.2 and equations (45)-(50) (pages 228-232). Part II: Products in quasisimple groups, Annals of Mathematics 165 (2007), 239-273, DOI 10.4007/annals.2007.165.239, Theorem 1.2, Lemma 4.1 (pages 247-248), Section 6, Proposition 6.2, and Lemma 7.1(a) with its A2 orbital application (pages 257-261). These are formal adaptations and consequences of published mathematics, using actual matrix geometry, finite-field arithmetic and Sylow arguments. No originality claim or redistribution of the papers is made. The scalar, twisted and transitive conclusions here concern the SL3 family. Other families, CFSG exhaustion, general central covers, the full all-simple scalar supplier, all-length Proposition 10.2, width and restricted Burnside bounds, and strong completeness remain open.

References