Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Compressed colour rank and crossing surgery

Abstract

Compressed colour rank and crossing surgery.

Theorem 1.1 (ascendingRank iff).

Lean statement: D5/S3/FiniteGroups/NikolovSegal/Equation47Colours.ascendingRank_iff

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

Source. Repository-derived.

Commentary.

The ascending rank is at most n exactly when the compressed generator list embeds as a sublist in colourBound(m,n).

Theorem 1.2 (signedRank link).

Lean statement: D5/S3/FiniteGroups/NikolovSegal/Equation47Colours.signedRank_link

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

Source. Repository-derived.

Commentary.

Joining words along opposite occurrences bounds the new rank by the sum of their ranks.

Theorem 1.3 (signedRank cancel).

Lean statement: D5/S3/FiniteGroups/NikolovSegal/Equation47Colours.signedRank_cancel

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

Source. Repository-derived.

Commentary.

Deleting adjacent opposite occurrences lowers the signed rank by at least one.

Theorem 1.4 (signedRank crossing).

Lean statement: D5/S3/FiniteGroups/NikolovSegal/Equation47Colours.signedRank_crossing

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

Source. Repository-derived.

Commentary.

The ordered ADCBE remainder of a literal crossing has no larger signed rank than the original word, with arbitrary generator colours and signs.

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