Source and verification

This article explains family 310 of the October 6, 2026 OpenAI collection. Research conclusions are attributed to its manuscripts. The review covers statements, introductions, and selected proof mechanisms; it is not an independent verification of the complete proofs.

🏷️ A subgroup poset as a topological detector

Quillen’s conjecture connects a finite group’s normal subgroups to the topology of a simplicial complex built from its elementary abelian subgroups. Family 310 claims the stronger rational-homology form for every finite group and every prime. This post concentrates on the topological mechanism: construct cycles with a detectable coefficient, preserve that coefficient on restriction, and use it to prove nonbounding in a larger complex. (OpenAI, 2026)

Manuscript claim

Let be finite and prime. If its largest normal -subgroup is trivial, then

Homology is augmented: the empty complex has a nonzero group in degree .

The proof uses substantial existing reductions in finite-group theory and detailed local constructions for classical groups. We explain the homology and counting interfaces those results supply, without developing a separate survey of the classification of finite groups.

🏷️ Preliminaries: order complexes and augmented chains

An elementary abelian -group is a vector space over , regarded as an additive group. Its rank is its vector-space dimension. The poset consists of the nonidentity elementary abelian -subgroups of , ordered by inclusion.

The order complex of a poset has a vertex for each element and a simplex for each strictly increasing chain. Thus a -simplex here is a flag

Its boundary is the alternating sum of flags obtained by deleting one subgroup. Chains are rational linear combinations of these oriented simplices. A cycle has boundary zero; a homology class is nonzero when its cycle is not itself a boundary.

In the augmented chain complex, there is one generator in degree , and every vertex has boundary . Consequently an empty poset has . This handles primes not dividing uniformly: their elementary subgroup posets are empty, and they are not counterexamples to the theorem.

For a nonempty contractible complex all reduced homology vanishes. The claimed rational nonvanishing therefore implies Quillen’s original assertion that contractibility forces a nontrivial normal -subgroup.

The reverse implication is classical and has a useful poset proof. In the poset of all nonidentity -subgroups, put . The maps

contract the poset, because pointwise comparable order maps induce homotopic maps of order complexes. To pass to elementary abelian subgroups, apply the poset fiber theorem: inside any nontrivial finite -group , a central subgroup of order gives the elementary contraction . Here really is elementary abelian because is central of exponent .

For a finite complex, nonzero rational homology has positive integral free rank. The universal coefficient theorem then gives nonzero homology over every field in that degree. Thus the manuscript’s theorem also identifies acyclicity over any fixed field with the existence of a nontrivial -core.

🏷️ Top-degree cycles and supported coefficients

Write for the largest elementary abelian rank. The complex has dimension . A nonzero cycle in that top degree cannot be a boundary because there are no chains one degree higher. Nonzero homology in that degree is called the Quillen dimension property.

The proof uses two different targets:

  • At odd primes, the established reduction asks for this top-degree property for specified unitary extensions. A rank calculation must precede the cycle construction.
  • At two, the local cycle need not be in the largest degree of its group. Instead, a nonzero coefficient on a saturated flag is carried into the ambient group by a propagation argument.

A saturated flag ending at a rank- group contains every rank:

“Nonzero coefficient” means an actual coefficient of that oriented simplex. A nonzero list of parameters used to describe chains could still describe the zero chain, so parameter counts alone are insufficient.

🏷️ Frame cycles and boundary cancellation

A frame of an -dimensional space is a decomposition into lines. In a space with a form, the allowed lines are nondegenerate and mutually orthogonal. Independent scalar actions on the lines, modulo simultaneous scalars, give an abstract projective sign space

of rank . In applications the manuscript checks that these abstract sign spaces are realized by the required elementary subgroups.

A partition of the frame specifies a subgroup by requiring coordinates in each block to agree. Successive mergers of lines give flags of these subgroups. For an ordered frame, alternating over merger orders gives a coned apartment chain in degree . Its internal boundary faces cancel; remaining faces correspond to coarsened decompositions.

Different frames that agree outside a plane can have the same such boundary face. The manuscript imposes a plane relation: sum the coefficients over every allowed ordered decomposition of that plane into two lines and require the sum to be zero. These relations cancel the remaining faces.

The resulting space consists of actual cycle-coefficient assignments. For each fixed frame its local flag-coefficient space has dimension , and a complete flag remembers its top frame. For , the main quantitative statement is

Here is the set of allowed unordered frames. In the no-form, hermitian and both-line-type symmetric cases with field parameter at least five, the manuscript proves the uniform lower bound

Uniformity means that the estimate remains valid as grows over a fixed field, separately for each required isometry type. The one-fixed-line-type symmetric version has different constants and requires an odd field parameter at least seven.

Why the relation kernel cannot be discarded

The source encodes merger trees by multilinear Lie superbrackets. A Poincaré–Birkhoff–Witt decomposition expresses words as products of bracket pieces while retaining their supporting subspaces. This yields normalized formal series for the word algebra and its bracket pieces.

Let count line generators, count plane relations, and count the actual kernel of the relation map. The relation complex gives

The kernel records dependencies among relations. Setting it to zero without proof would corrupt the dimension estimate. Instead, a marked-factor argument proves

coefficientwise, where multiplies each supporting-space term by its dimension. Briefly, multiplying a leading kernel monomial by a bracket supported on an independent summand gives another nonzero kernel monomial. Marking the appended factor recovers the input. The sum of dimensions of all possible marked factors is bounded by the ambient dimension. This gives the inequality even with odd, exterior factors, because independent supports cannot repeat a factor.

For , differentiation then gives

When the coefficients of are nonnegative, this proves . It avoids dividing an inequality by a formal series whose inverse could have negative coefficients.

Plane counts evaluate the comparison. Without a form, a plane over has ordered complementary line pairs. A hermitian plane over has ordered orthogonal nondegenerate line pairs. Their reciprocal counts give the quadratic-series constants. In the symmetric case the source retains both determinant square classes throughout the calculation; averaging them would not establish a bound for each type.

🏷️ Decorations: paying for additional boundary equations

To work in larger elementary extensions, attach commuting order- directions to a sign group, requiring an internal direct product. These extra directions are called decorations. Shuffling the frame chain with their apartment chain introduces new boundary faces whenever one decoration is omitted.

Suppose there are full decorated data, and every partial datum missing direction has at least completions. The compatible frame cycles initially have dimension at least . Each partial datum imposes a vector equation of rank at most to cancel its missing-direction face. There are at most partial data of kind .

Consequently the surviving dimension is at least

A strict positive margin produces a nonzero cycle, provided the map from decorated coefficient data to actual flags is injective. The manuscript verifies this by recovering the frame, sign group and labelled decoration axes from selected full flags. Further coincidences among boundary faces are harmless because the imposed equations already cancel them; coincidences of full flags require this separate check.

This is a rank bound, so it does not assume independence of all imposed equations. When , there are no completion conditions and the sum is zero.

🏷️ Restriction using a fixed complement

A cycle may first be constructed in a group larger than the desired subgroup . Intersecting every vertex with can collapse flags, lose vertices or cancel coefficients. The source instead restricts a carefully chosen residue.

Suppose the cycle is supported on full flags ending at rank- elementary groups , with

and choose a supported top group attaining equality. Write . A building-cycle lemma supplies a supported full flag through a rank- complement with .

The lemma has a concrete proof: among supported flags choose one whose relative permutation against a reference flag has the most inversions. If two adjacent positions are increasing, the boundary equation at that panel supplies another supported completion with one more inversion. Hence a maximal choice is opposite to the reference flag, giving the desired complement.

Fix the saturated initial flag up to , retain only simplices containing it, and delete those initial vertices. This residue is still a cycle, up to the fixed sign in the boundary identity. Every continuation vertex contains the same and lies in some supported . Since ,

Equality forces . Thus intersection is injective on this residue, with inverse . No suffix flags merge, and the selected coefficient survives. The result is a nonzero cycle on full flags of rank in .

It is automatically nonbounding only when . Otherwise the next propagation argument supplies nonbounding. Maximal intersection index is needed only among supported top groups; it need not be constant over them.

🏷️ Propagating a coefficient into ambient homology

At two, work in a minimal counterexample. The group-theoretic reduction supplies a nonabelian simple component . Choose an elementary subgroup normalizing , intersecting it nontrivially, such that acts faithfully on and its centralizer has trivial -core. The allowed configurations form a family closed under the relevant faithful enlargements; choose maximal rank in that family.

Two consequences matter. Every order- element of lies in , and there is no strictly larger elementary for which remains faithful and has trivial -core. This is not an assertion that has maximal elementary rank in all of .

Suppose a cycle in has a nonzero coefficient on a saturated rank- flag ending at . Proper-subgroup induction gives a nonbounding cycle in . Faithfulness implies , and these two groups commute, so the product shuffle gives a cycle .

To prove that it stays nonbounding in , delete the faithful elementary overgroups of , largest first. The maximality condition makes each relevant centralizer poset contractible; explicit centralizer and product maps identify the remaining upper interval with that poset up to homotopy. Each deletion therefore preserves homotopy type, while the product cycle remains supported in the undeleted complex .

The residue map at satisfies

Saturation is essential: there is no missing elementary rank into which an extra vertex could be inserted before or within . On the product shuffle, a flag containing must take all its -steps first. Therefore its residue is exactly

where sends a centralizer subgroup to . The strict upper interval of in retracts to the centralizer poset by , and this retraction composed with is the identity.

If were a boundary, the residue identity followed by that retraction would make a boundary, contradicting its choice. This is the step that converts a single supported coefficient into ambient nonzero homology. It also works when the centralizer poset is empty: its augmented degree-minus-one class and the empty upper interval give the same contradiction.

🏷️ What the local constructions must supply

The remaining group-specific sections verify the dimension margins, injectivity of flag coefficients, permissible configurations and rank formulas needed above. At odd primes, the unitary assertion concerns with elementary abelian quotient; it does not assume that every such extension splits. At two, the local propositions exclude components of a minimal counterexample, rather than asserting a universal top-degree property for every extension.

Symplectic cycles are constructed directly in the selected extension. The last small orthogonal case, represented by , includes a separate equivalent-poset argument retaining the join of component and centralizer homology. It is not silently absorbed into the generic frame estimate.

The manuscript then combines these local conclusions with the established reductions to exhaust the possible counterexamples. This note audits the theorem conventions, augmented-chain arguments, coefficient bounds, decoration count, fixed-complement restriction and propagation interfaces. The full classification reductions, merger-coefficient/PBW identification and every classical-group case estimate remain substantive source inputs, not independently verified proofs here.

🏷️ Key steps and proof outlines

Saturation makes coefficient extraction commute with boundary

A nonzero coefficient is useful only if extracting it respects the chain complex. Fix a saturated flag

The residue keeps flags containing this prefix and deletes its first vertices. Every other flag maps to zero. The result lies in the augmented chains of the strict upper interval above .

No subgroup can appear before or between consecutive : there is no integer rank available. Thus any flag containing starts with exactly that prefix. Deleting a prefix vertex destroys the prefix and contributes zero to the residue. Deleting the th continuation vertex has boundary sign shifted by . Therefore

For example, when , the flag has residue . Of its three boundary faces, only retains the prefix, and its residue is the empty augmented chain. This equals the augmented boundary of . Including degree makes the identity valid even when the upper interval is empty. (OpenAI, 2026)

A maximal supported chamber supplies the needed complement

Restriction to a subgroup can merge different flags and cancel their coefficients. The proof prevents this by first choosing a complement inside a top group carrying a nonzero coefficient.

Let have rank , and suppose its intersection has codimension , with . The case needs no residue extraction: the maximal-index condition already puts every supported top group inside . Regard as a vector space and choose a reference full flag through . A chamber’s relative position to this reference flag is encoded by a permutation , via

Among supported chambers, maximize the inversion number of . If two adjacent entries are increasing, delete the intermediate subspace to form a panel. In the resulting two-dimensional quotient, exactly one line gives the increasing order of those entries; every other line reverses them and adds one inversion. The cycle equation says the sum of chamber coefficients around that panel is zero. Since the current coefficient is nonzero, another supported completion exists, contradicting maximality.

Hence a supported chamber has decreasing relative permutation. Its rank- vertex is complementary to . Take the saturated residue at the prefix ending at . For any surviving vertex inside a supported top group , the maximal-index hypothesis gives

Equality forces . The fixed complement therefore lets one recover from its intersection with , preventing coefficient collisions on restriction. The selected nonzero coefficient survives in a lower-degree cycle on .

Contractible deletions make room for a global nonbounding cycle

The propagation lemma starts with a local cycle carrying coefficient on , and a nonbounding centralizer cycle . Certain faithful overgroups would interfere with the desired residue calculation. Delete them in decreasing order of inclusion.

At a deletion vertex , the remaining upper interval retracts, up to poset homotopy, onto the elementary-subgroup poset of its centralizer: the maps are and . Their composites are the identity in one direction and pointwise below the identity in the other. The configuration’s maximality hypothesis makes that centralizer have a nontrivial normal -subgroup, hence a contractible elementary-subgroup complex. The link of is consequently contractible, so deleting it preserves homotopy type.

In the remaining poset, form the shuffle product . The factors commute and intersect trivially, so product coordinates are unique. A shuffle containing the entire prefix must take all the local-factor steps first; otherwise it would introduce a nontrivial centralizer coordinate too early. Its residue is therefore exactly

where . If were a boundary, the residue identity would make this a boundary in the upper interval. Applying its retraction back to the centralizer gives that is a boundary, a contradiction. This proves nonbounding even when the local cycle is not top-dimensional in the ambient group. The group-theoretic construction of configurations meeting the lemma’s hypotheses remains a separate source input.

🏷️ Manuscripts and verification scope

No family scope page was present at lean/docs/310.md in the pinned snapshot. This does not establish that all related formalization code is absent. No Lean build, axiom audit, or manuscript-to-formal-statement equivalence check was performed for these notes.

OpenAI collection provides prerequisites and the reading sequence; coverage register records completed and pending families.

🐻  OpenAI 2026. Rational homology and Quillen’s conjecture.