Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Lemma 4.1 with ordered genuine corrections

Abstract

Lemma 4.1 with ordered genuine corrections.

Theorem 1.1 (twisted product of corrected scalar).

Lean statement: D5/S3/FiniteGroups/NikolovSegal/PartIILemma41.twisted_product_of_corrected_scalar

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

Source. Repository-derived.

Commentary.

For any group, corrected scalar PRODUCT coverage for an arbitrary beta tuple and correction g implies ordered twisted PRODUCT coverage for every additional automorphism tuple a. The proof absorbs ordered constants into a single constant fixed before the target and constructs genuine xi and eta.

Theorem 1.2 (twisted input of scalar one).

Lean statement: D5/S3/FiniteGroups/NikolovSegal/PartIILemma41.twisted_input_of_scalar_one

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

Source. Repository-derived.

Commentary.

The precise scalar PRODUCT input at q=1, with its pre-target inner corrections, implies the twisted PRODUCT input at the same length.

Theorem 1.3 (uniform transitive supplier of scalar products).

Lean statement: D5/S3/FiniteGroups/NikolovSegal/PartIILemma41.uniform_transitive_supplier_of_scalar_products

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

Source. Repository-derived.

Commentary.

The uniform large-simple scalar PRODUCT statement for every positive q conditionally supplies the literal uniform transitive supplier. The q=1 case gives the twisted input by Lemma 4.1, and the cutoff is the maximum of the two scalar cutoffs. Scalar existence is still an explicit unproved premise.

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 8, Lemma 8.3 and Proposition 8.4, Section 9, Proposition 9.1 (pages 223-226), and 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 and Lemma 4.1 (pages 247-248). These are formal adaptations and conditional consequences of published mathematics, with elementary finite-set growth supporting bounded-small coverage; no originality claim or redistribution of the papers is made. Large-simple scalar PRODUCT existence, quasisimple central covers, all-length Proposition 10.2, uniform width and restricted Burnside bounds, and full strong completeness remain unproved.

References