Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

From transitive blocks to conditional absorption

Abstract

An independent transitive simple-group value supplier yields exact large-minimal-normal absorption through the actual factor orbits.

Definition 1.1 (The independent transitive supplier).

Lean statement: D5/S3/FiniteGroups/NikolovSegal/TransitiveCoverage.TransitiveSimpleCommutatorSupplier

Formalization. D5/S3/FiniteGroups/NikolovSegal/TransitiveCoverage.TransitiveSimpleCommutatorSupplier (✓ std3).

Source. Repository-derived.

Commentary.

Fix natural q, m and C. For every finite nonabelian simple group S with C less than its order, every finite nonempty index type I, and every tuple k of automorphisms of I to S indexed by Fin m, suppose permutations sigma and component automorphisms beta satisfy k(i)(x)(sigma(i)(j)) = beta(i)(j)(x(j)). If the subgroup generated by sigma is transitive, the supplier requires PrescribedCommutatorCoverage(I to S,q,m,k). This means an inner tuple y is chosen before every target t, after which a commutator tuple c may depend on t. This supplier is UNPROVED in this formal development.

Definition 1.2 (Uniform choice before all groups and tuples).

Lean statement: D5/S3/FiniteGroups/NikolovSegal/TransitiveCoverage.UniformTransitiveSimpleCommutatorSupplier

Formalization. D5/S3/FiniteGroups/NikolovSegal/TransitiveCoverage.UniformTransitiveSimpleCommutatorSupplier (✓ std3).

Source. Repository-derived.

Commentary.

For every positive natural q, there must exist natural m and C with m positive such that TransitiveSimpleCommutatorSupplier(q,m,C) holds. The length and cutoff are chosen before the simple group, index type, factor count and prescribed tuple. This uniform statement is UNPROVED in this formal development.

Theorem 1.3 (Coverage from actual invariant orbits).

Lean statement: D5/S3/FiniteGroups/NikolovSegal/TransitiveCoverage.minimal_normal_coverage_of_transitive_supplier

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

Source. Repository-derived.

Commentary.

Let G be any finite group and N any minimal nontrivial normal subgroup. Fix natural q,m,C and assume TransitiveSimpleCommutatorSupplier(q,m,C), noncommutativity of N, and that every actual minimal normal factor of N is nonabelian simple of order greater than C. Then every prescribed k from Fin m to MulAut(N) satisfies PrescribedCommutatorCoverage(N,q,m,k). The full socle and trivial center follow from minimal normality. The actual orbit product is constructed, and ambient factor conjugacy supplies isomorphisms to a representative simple group on each block. Transport retains the genuine component automorphisms and the exact generated permutation action. The supplier applies on each transitive orbit; equivariance combines their value sets with the same q and exact m.

Theorem 1.4 (Exact conditional minimal-normal absorption).

Lean statement: D5/S3/FiniteGroups/NikolovSegal/TransitiveCoverage.absorption_of_transitive_supplier

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

Source. Repository-derived.

Commentary.

Fix natural q,m,C,cutoff with cutoff at least four and twice C less than cutoff factorial. Under TransitiveSimpleCommutatorSupplier(q,m,C), LargeMinimalNormalAbsorption(q,m,cutoff) holds: for every finite G, minimal nontrivial normal N with alpha(N) greater than cutoff, a in N and x in the exact m-term ordered q-power value set of G, a times x belongs to the same value set. Large-alpha structure supplies the actual large simple factors; block coverage for the corrected automorphisms and the prescribed coset-power identity give the conclusion. The existing generator decomposition consumes precisely this absorption interface.

The source is Part I, DOI 10.4007/annals.2007.165.171, printed pages 227–228. The supplier is a centerless simple-group, chosen-length specialization sufficient for this reduction. Published Proposition 10.2 also treats quasisimple groups and every length m at least z(q); its full printed statement is not formalized here. The supplier is unproved in this formal development, not an open research conjecture. Uniform power width, restricted Burnside bounds and unconditional strong completeness remain unproved.

References