Source and verification
This article explains family 308 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.
🏷️ The realization problem
Homology often admits a simple quotient that is surprisingly difficult to realize by a finite topological object. Smith–Toda complexes ask for an especially sharp example: kill the first chromatic generators themselves, rather than unspecified powers of them.
Family 308 contains two constructions. The first claims that, for every fixed height, such a finite complex exists at a prime that may depend on the height. The second supplies a particular height-four complex at the prime 1009. Their mechanisms differ: varying-prime rational algebra and finite descent in the first, explicit obstruction groups and a quantitative homotopy relation in the second. (OpenAI, 2026) (OpenAI, 2026a)
The two conclusions
For each integer , the first manuscript claims that there exists a prime admitting a finite -local spectrum with canonical Brown–Peterson homology
It does not give an explicit bound on the required prime. The second manuscript claims a finite at , with the same canonical quotient-comodule requirement.
The quantifiers matter. The first theorem allows to depend on ; it does not choose one prime valid at every height. Both conclusions concern ordinary finite spectra localized at , and neither requires a ring structure on the final complex.
🏷️ Preliminaries: spectra, quotients and chromatic generators
A spectrum is the stable version of a pointed space: suspending becomes invertible, and a map has a cofiber that behaves like a mapping cone. A finite spectrum is built from finitely many sphere cells. Localization at makes multiplication by every integer prime to invertible. Thus a finite -local cell construction retains finitely many cells while allowing such denominators in attaching maps.
Brown–Peterson homology, denoted , is a generalized homology theory at the prime . Its coefficient ring is
These generators organize chromatic height. The desired quotient retains and kills the first powers of . A periodicity self-map that acts by a higher power of does not by itself construct this quotient.
There is also a comodule condition. The cooperations record natural homology operations; a -module equipped with their coaction contains more information than its underlying graded module. Here “canonical” means the quotient coaction generated by the image of the bottom sphere in degree zero.
The basic cofiber calculation explains the construction target. Suppose is cyclic on a bottom unit , and a map restricts on that unit to a class whose Hurewicz image is , where is a unit and is a nonzerodivisor modulo . Because the induced homology map is -linear and the module is cyclic, it is multiplication by everywhere. The cofiber long exact sequence then gives
The hard step is producing with the correct first-power Hurewicz image. Regularity finishes the homology calculation only after that step.
🏷️ Varying primes without losing varying degrees
The first manuscript works in a categorical ultraproduct of ordinary -local spectra over a nonprincipal ultrafilter on odd primes. Operationally, a sequence represents an object, and two pieces of finite data agree when they agree on a set of primes belonging to that ultrafilter. Such sets are called large. Finite intersections remain large. (OpenAI, 2026b)
Every fixed nonzero integer is invertible at all but finitely many primes. Consequently mapping spectra in this ultraproduct are rational. This supplies characteristic-zero algebra models, but it does not erase spheres whose dimensions grow with . The construction retains formal weights representing the sequences of dimensions .
Starting with the sphere unit , it seeks maps and cofibers
Here dimensions denote primewise sequences; is multiplication by . The ultraproduct has the multiplication needed for these finite constructions. The proof does not descend a full commutative algebra structure on every to individual primes.
Why an Euler parameter appears
To obtain the next attaching class, the manuscript applies a -fold permutation power with affine symmetry . A power operation need not preserve cofibers. The comparison involves a cube whose size grows with , so controlling individual pieces by unrelated bounds would not suffice.
The uniformity theorem says that one Euler map, associated to twice the reduced permutation representation, annihilates the whole comparison object. Inverting that map in an auxiliary category makes the power exact. Write for its Euler parameter. Before inversion, reduction modulo recovers the sphere degree needed for the next attachment.
This creates a delicate order of operations: normalize the attaching class while it still exists before inversion, then reduce modulo . An arbitrary class that exists only after adjoining has no such reduction.
Why tensor testing needs a completion argument
The normalization uses a universal coefficient algebra and a finite-cell Koszul algebra that kills specified cycles. These auxiliary algebras have actual primewise commutative models. A connectivity estimate at weights growing with gives the necessary equivalences only after tensoring with .
Tensoring with need not detect equivalences of arbitrary -modules. The manuscript therefore proves that the actual target belongs to the class detected by this test, using the Amitsur completion
This totalization combines all iterated tensor powers and their compatibility maps. Because is perfect, tensoring with it commutes with the relevant totalization, and the augmented diagram becomes split after that tensor. On the required local targets this recovers the original object. Normalization consequently preserves algebra maps and chosen nullhomotopies, rather than producing only unrelated homotopy classes.
These uniform-power, connectivity and target-locality statements are substantial inputs from the manuscript. They are the construction machinery, not consequences of rationality alone.
🏷️ Detecting the correct first power and descending
For detection, use complex cobordism . Let be the coefficient of in its formal-group -series, with . The manuscript’s Thom-corrected power calculation identifies a leading Euler term that is a unit times . (OpenAI, 2026b)
The error control is essential. Lower powered coefficients vanish after the earlier attachments; lower coefficients are divisible by ; quadratic terms therefore become divisible by . The remaining comparison has the form
where are units, is the normalized next class, and represents the next cobordism coefficient. Injectivity of multiplication by permits cancellation; reduction modulo then identifies the next Hurewicz image up to a unit. The required injectivity comes from the vanishing of an odd homotopy group in the relevant Euler layer, using even cobordism homology and even sphere degrees. It is not assumed for an arbitrary completed algebra.
The ordinary multiplicative map takes the successive coefficient ideals to the Hazewinkel ideals. No compatibility of that map with power operations is used: the power calculation is already completed in cobordism.
Only finitely many attaching maps, unit maps, cofiber equivalences, specified homotopies and Hurewicz equalities are needed at fixed . They descend together to a common large set of primes. At each of those primes the regular-sequence calculation computes all homology degrees at once. Thus no intersection of infinitely many large sets, one for each degree, is required.
The stated theorem then chooses one prime in that common large set. The required prime may depend on the fixed height; no effective estimate is supplied.
Finally, a map between finite -local spectra can be written with . Multiplication by is an equivalence on its localized finite-spectrum source, so its cofiber is the localization of a finite cofiber, which can be realized by finitely many cells. The bottom sphere surjects onto the resulting cyclic -module and fixes its canonical coaction. This is the finite realization step.
🏷️ Prime 1009: an explicit obstruction calculation
The second manuscript fixes and constructs from . It first constructs a binary, two-sided unital multiplication on by cell-extension obstruction theory. Associativity is not required. (OpenAI, 2026a)
The Adams–Novikov spectral sequence starts with cobar cohomology of the -comodule and computes stable homotopy. Its filtration-zero edge detects which primitive homology elements are Hurewicz images. Put
Writing internal degree as , a class of filtration and weight lies in stem . Sparsity forces every possible differential from to have target
A normalized cobar cochain of length has reduced factors, each of positive weight. This bounds the candidates. In the target ranges, the manuscript compares three adjacent cochain degrees, so both kernels and images agree with an additive-cooperation model. Matching only the middle vector space would not identify cohomology.
A further May filtration breaks this model into exterior and polynomial generators indexed by base- digits. Finite weight counts leave only four possible rows:
| Parameter | How the manuscript removes it |
|---|---|
| A relation supplied by , followed by an injective multiplication on actual cobar cohomology | |
| Frobenius-kernel and coefficient-filtration calculations make the target cohomology zero | |
| A second Frobenius calculation rules out corrected cocycles, not merely their leading monomials | |
| A homotopy annihilation relation kills the target before its possible differential page |
For the middle rows, a Frobenius extension separates a finite infinitesimal kernel from a quotient. Kernel cohomology is a nontrivial coefficient module for that quotient. Filtering the coefficient action produces another spectral sequence. The proof checks that the proposed source and target of each eliminating differential exist on that page, and controls adjacent degrees and possible corrections. An initial May-page list by itself would not establish the claimed vanishing.
🏷️ The last obstruction needs a deadline
Let be the filtration-two, weight- detector of a sphere class . The last target is covered by multiplication by from a much smaller group:
The source has permanent classes represented by homotopy elements . The manuscript proves
The geometry behind this relation uses a two-cell spectrum obtained from the cofiber of a sphere class , shifted so its top cell has dimension zero. A relation permits a lift of to . Taking such lifts and averaging over permutations uses the fact that is a unit at ; the resulting symmetric retract is still finite.
A separate cobar and finite-filtration argument makes the relevant symmetric map null. To use the merely binary product on , first choose a parenthesization and multiply the factors, then symmetrize the factors. The scalar factors involve an even-degree power of , so the required value does not depend on an unproved associativity of .
Eventual annihilation is insufficient: the obstruction must disappear before it can be the target of the last differential. A permanent source detector multiplied by has filtration and represents zero homotopy. Finite convergence therefore forces it to be hit by a differential of length at most . The numerical comparison is
Multiplying by the remaining power shows that the entire last target has disappeared in time. This page bound is the point where a homotopy relation becomes an obstruction-theoretic construction.
🏷️ Attaching the final cells
With every possible differential removed, survives. No differential enters filtration zero, so the edge gives an actual map whose Hurewicz image is . Compose with the binary multiplication on to obtain a self-map. Its bottom-cell value and cyclic -module structure force multiplication by on all homology.
The cofiber then has the required quotient. It has 32 cells indexed by subsets , in dimensions
No multiplication on this final cofiber is needed.
Both manuscripts thus end with the same regular cofiber mechanism, but earn its input differently. The varying-prime construction preserves a finite diagram through rational models and descent; the explicit-prime construction eliminates all differential targets with enough quantitative control to attach the next first-power cell.
This note checks the stated conclusions and selected construction, detection, cochain-comparison and final-obstruction interfaces. It does not independently verify the full uniform-power and connectivity arguments, every May enumeration, the symmetric null-map calculation, or the foundational convergence results.
🏷️ Key steps and proof outlines
First-power realization reduces an infinite homology calculation to finite data
The varying-prime construction ultimately needs only a finite tower at a fixed height. At stage , assume the homology of is the polynomial quotient by the earlier regular generators, with bottom class . Suppose the constructed self-map sends to a unit multiple of the next generator .
Every homology class is for a coefficient , so linearity determines the map on all degrees as multiplication by that unit times . Regularity makes this map injective. The cofiber exact sequence then has no kernel contribution and computes its cokernel as the next quotient. This is an inductive calculation of the entire graded module from one Hurewicz equality per stage.
That observation is what makes descent from the ultraproduct legitimate. At fixed height there are finitely many maps, specified nullhomotopies, unit comparisons, and first-power equalities to retain. Their validity can be imposed on one common large set of primes by finite intersection. The regular-sequence argument then computes every degree at each chosen prime. Intersecting a separate large set for every homology degree would be an unjustified infinite-intersection step. (OpenAI, 2026b)
The canonical comodule claim also follows from one structural map. The bottom sphere surjects onto the cyclic quotient in homology. Naturality of the cooperation coaction therefore determines the coaction on every quotient class from that on the sphere’s coefficient module. A graded-module isomorphism without this bottom map would not identify the coaction.
Clearing denominators preserves a genuinely finite spectrum
A map between localizations of finite spectra has the form , with . Multiplication by is an equivalence after -localization, so changing the source or target by this equivalence identifies the cofiber of with the localization of the cofiber of .
After a finite suspension, is represented by a cellular map between finite models. Its mapping cone is finite; desuspending gives a finite spectrum. Iterating this observation proves finiteness of the descended tower. This is stronger than merely constructing a compact-looking object in the auxiliary algebraic category.
A binary unit suffices for the explicit annihilation relation
The prime-1009 construction uses a two-sided unital binary multiplication on without assuming associativity. Its last obstruction is removed by proving
for the relevant low-filtration representatives .
Earlier stem calculations give lifts of and of the scalar class to , where is the auxiliary finite spectrum in the source. Smash one lift of with scalar lifts, then multiply the factors using one fixed binary tree. The top projection is .
This assertion uses only the two unit homotopies. Induct through the binary tree: a subtree without is a scalar times the unit, and the unique subtree containing is the product of its scalars times . The scalar has even degree, so no sign ambiguity appears.
Only after this multiplication does the argument project the remaining factors onto their symmetric retract. Their top projection is permutation-invariant, so averaging retains the same scalar product. It does not permute or reassociate the already multiplied factors. Composing with the source’s actual symmetric null map contributes one further factor of , proving the displayed annihilation. (OpenAI, 2026a)
Homotopy zero must force disappearance before the dangerous page
Let detect the permanent sphere class , and let be the permanent filtration-five class represented by . The product has filtration
It supports no outgoing differential because it is a product of permanent classes. Its homotopy product is zero, so convergence forces it to disappear. If it is initially nonzero, it must be hit by an incoming differential. A differential of length landing in filtration starts in filtration , hence .
The prospective last differential from occurs at length , with , and
Thus the annihilated class vanishes strictly before that page. A further permanent power of covers every candidate target by the source’s comparison surjection. This converts an eventual homotopy relation into a usable deadline, completing the obstruction argument before the realizing cofiber is formed.
🏷️ Manuscripts and verification scope
- Finite Smith–Toda complexes at varying primes — pinned manuscript and companion source.
- A finite Smith–Toda complex V(4) at the prime 1009 — pinned manuscript and companion source.
No family scope page was present at lean/docs/308.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.