feat: roadmap for high-dimensional differential topology and homotopy spheres

[Paul-Lez]

• Develop James/EHP, Bott periodicity, bundle classifiers, and Pontryagin–Thom.
• Build h-cobordism and surgery theory through the classification of homotopy spheres and θ₆.

Sources: Bott, Kervaire–Milnor, Browder, and Wall.

Motivating consumer: Levent PDF

AI assistance: Codex (GPT-5) and Codex 5.6 Sol.

[CBirkbeck]

Part of a deep adversarial review of the reusable-roadmap split — PRs #279–#284, reviewed 25 August 2026. This section covers #284 — High-dimensional differential topology and homotopy spheres.

Head reviewed: 225d2d6f490780a26ebf31c6679ab9515c0b2671

Verdict

Major changes requested.

The split has made the scope reusable, and the roadmap now acknowledges James constructions, a full Bott proof, Pontryagin–Thom, comparison of geometric and historical A_n/P_n, and Wall surgery. That is a genuine improvement. I found two false statements and several foundational gaps which must be repaired before the roadmap is ready.

1. The proposed proof of the James equivalence is false for connected X

Stage 3B says that for connected CW X, the roadmap will use the filtration, homology calculation, simple connectivity, and homological Whitehead to prove

[
JX\simeq\Omega\Sigma X.
]

Connectedness does not imply either side is simply connected. For example,

[
X=S^1,\qquad
J(S^1)\simeq\Omega S^2,
]

and both spaces have fundamental group (\mathbb Z).

Thus the proposed proof cannot use the simply connected homological Whitehead theorem at the stated generality.

Repair this in one of two ways:

1. restrict the theorem and all its consumers to simply connected X; or
2. prove the full connected James theorem by also controlling π₁ and the universal covers, or by a suitable Whitehead theorem with local coefficients.

If low-dimensional EHP calculations use (X=S^1), the second route or a separate low-dimensional theorem is necessary.

2. A framed normal bundle does not have sphere Thom space

Stage 5 says that for a framed normal bundle its Thom space is identified with “a suspended sphere”. This is false.

For a rank-(k) trivialized bundle over (M),

[
\nu\cong M\times\mathbb R^k,
]

one has

[
\operatorname{Th}(\nu)
\cong M_+\wedge S^k
=\Sigma^k M_+,
]

not (S^k) unless (M) is a point.

The Pontryagin–Thom representative is obtained by

[
S^{n+k}
\longrightarrow \operatorname{Th}(\nu)
\cong \Sigma^k M_+
\longrightarrow S^k,
]

where the last map collapses (M) to the non-basepoint.

Correct the statement, the collapse-map target, and every subsequent inverse/naturality diagram.

3. Specify the convenient category for loop spaces and filtered colimits

The roadmap repeatedly uses:

• compact-open mapping spaces;
• loop–suspension adjunction;
• James constructions;
• filtered colimits of topological groups;
• classifying spaces;
• stable orthogonal groups.

Naive colimits and products in ordinary TopCat do not automatically have the convenient exponential and compact-generation properties used by these theorems.

Choose an exact framework:

• compactly generated weak Hausdorff spaces/k-spaces with comparison to Mathlib's spaces; or
• a restricted CW-based construction in ordinary spaces with every mapping-space and colimit theorem proved directly.

State how stable SO, BSO, loop spaces, and homotopy classes are formed in that framework. This is a prerequisite, not an implementation detail.

4. The Bott-periodicity proof still hides an analytic roadmap

The revised Bott section is much better, but it still assumes a large missing substrate. Bott's Morse-theoretic proof requires more than finite-dimensional Morse theory:

• finite-dimensional broken-geodesic approximations to path spaces;
• comparison of those approximations with the actual path space;
• invariant metrics and symmetric-space geodesics;
• Hessian and Morse–Bott critical manifolds;
• index and nullity calculations;
• compactness/Palais–Smale or the exact finite approximation replacing it;
• attachment of negative disc bundles;
• increasing-connectivity estimates.

The Heegaard Floer finite-dimensional Morse supplier does not provide this automatically.

Either split real Bott periodicity into a separate roadmap or add these objects and theorem dependencies explicitly.

5. Resolve smallness and universes for Theta_n, A_n, and P_n

The geometric cycles quantify over smooth manifold carriers. The collection of all such types is not automatically a small Type-0 quotient.

The current Suggested.lean returns unparameterized AddCommGrpCat objects, which silently restricts or hides the universe issue.

Choose one approach:

• universe-polymorphic groups of cycles in Type u, with a proved invariance under universe lift;
• a small skeleton encoded by finite triangulations/handle data;
• a bounded Euclidean-embedding code with an essential-surjectivity theorem.

The final theorem for an arbitrary M : Type u must explain how its sphere represents an element of the selected Theta_6.

6. Stable parallelizability versus parallelizability needs an exact theorem

Stage 6 defines a “parallelizable filling” but stores a stable tangent framing, and later promises conversion to honest parallelizability in the surgery range.

State the theorem with its actual hypotheses:

• dimension;
• nonempty boundary or spine dimension;
• orientation;
• obstruction/cancellation of a trivial line;
• compatibility with collars.

Do not use “parallelizable” before the honest trivialization has been constructed.

7. Pin the standard A_n and P_n definitions before using the exact sequence

The roadmap correctly says that the convenient defect-disc and collared-filling models are not definitionally Kervaire–Milnor's groups. The comparison is nevertheless still too informal.

For each historical group, provide:

• the exact cycle and equivalence relation from the source;
• the map from the convenient Lean model;
• the inverse;
• compatibility with addition;
• comparison of the boundary and defect maps.

Only after these isomorphisms may the classical exact sequence be transported to the convenient carriers.

8. Wall's odd-dimensional groups need formations, not a generic “Witt group of forms”

The phrase “appropriate Witt group of nonsingular quadratic data” must distinguish:

• even-dimensional quadratic forms;
• odd-dimensional formations.

The later statement that odd skew formations are stably hyperbolic is correct in the simply connected (\mathbb Z)-case, but the public wallSurgeryObstructionGroup must be defined with the dimension-dependent carrier which makes that theorem meaningful.

9. The sixth-stem representative and Kervaire normalization need a precise source chain

Stage 9 is much improved, but “the plumbing/Toda construction” should be replaced by exact constructions and references:

• the unstable representative of ν²;
• its stabilization;
• the framed six-manifold obtained under Pontryagin–Thom;
• the quadratic refinement;
• the Arf calculation;
• the comparison with the map coker J_6 → P_6.

This is the normalization that makes the final exact-sequence argument work.

10. The final orientation-preserving conclusion is not represented in Lean

Suggested.lean concludes only

Nonempty (M ≃ₘ S⁶).

The roadmap also promises an orientation-preserving diffeomorphism after matching orientations. Add the oriented carrier and a theorem that the chosen diffeomorphism preserves it. A plain Diffeomorph does not remember this conclusion.

11. Suggested.lean does not validate the geometric definitions

Every principal group is currently introduced as

noncomputable def ... : AddCommGrpCat := by sorry

with a docstring saying what the body should be. This does not type-check:

• the cycle carrier;
• the equivalence relation;
• connected sum;
• framed bordism;
• filtered colimits;
• the maps in the exact sequence.

Add representative structures for cycles and actual quotient/colimit signatures, together with the universal properties which prevent arbitrary implementations from satisfying the file.

12. Import the corrected algebraic-topology supplier

The roadmap consumes #283 throughout. Once #283 is corrected, Suggested.lean should import its representative module and #check the exact Hurewicz, Whitehead, duality, and finite-CW declarations rather than leaving that interface solely in prose.

What should remain

• the reusable rather than six-sphere-specific scope;
• the separate treatment of the index-two/index-three Whitney case in dimension six;
• the geometric definition of Theta_n;
• the explicit James/EHP proof spine;
• the decision to prove the full Bott cycle rather than postulate two vanishings;
• construction of both directions of Pontryagin–Thom;
• comparison of convenient A_n/P_n models with the historical ones;
• a full Wall-surgery theorem rather than a table lookup;
• the explicit chain through ν², the Kervaire invariant, and Theta_6=0;
• honest compactness, separation, and countability hypotheses in smooth recognition.

Recommended disposition

Do not merge until the James and Thom-space errors are corrected and the topological category, Bott substrate, universes, and geometric group carriers are pinned. This roadmap is likely best split once more into stable homotopy/Bott and h-cobordism/surgery/homotopy-sphere roadmaps, although a single broad normative roadmap is possible if every internal boundary is explicit.

---

Cross-roadmap notes (apply across the #279–#284 split)

• PRs #280, #282, #283, and #284 still use the Levent six-sphere PDF as the link in the PR body. These are now general-purpose roadmaps. The construction paper should be described only as a motivating consumer; each PR body should instead foreground the standard sources listed in its README.
• Every downstream roadmap should import or #check the exact representative interfaces of its supplier once those suppliers land. Prose references alone are not enough to prevent incompatible carriers.
• The intended merge order is:
  #279 and corrected #283 first; #280 after both; #281 after #279 and an exact algebraic toric supplier; #282 after #279 and a reconciled compact-Riemann-surface degree API; and #284 after corrected #283 plus its geometric-topology and Morse/transversality suppliers.

[Paul-Lez]

🤖 Addressed in 90921a9. The James proof now handles connected fundamental groups through universal covers and local coefficients; the framed Thom space is Sigma^k M_+ with the correct augmentation; and the roadmap pins one compactly generated topology substrate plus the full Bott-specific Morse--Bott approximation. Geometric cycle groups are small explicit quotient and colimit constructions; stable versus honest parallelizability, historical A_n and P_n comparisons, parity-dependent Wall carriers, the normalized nu-squared and Kervaire chain, and the orientation-preserving endpoint are explicit. The corrected algebraic-topology supplier is now an ordered merge and literal import-check gate.

[CBirkbeck]

Part of the second deep review of the reusable-roadmap split — PRs #279–#284, reviewed 26 August 2026 against the updated heads. This section covers #284 — High-dimensional differential topology and homotopy spheres.

Head reviewed: 90921a951472203b76abff700acee2a934bb960b

All six updated branches pass their current CI. The comments below concern the mathematics and the proposed public APIs, not elaboration failures.

What has been fixed

The README is now far more serious and mathematically explicit:

• it supplies a compactly generated-space substrate;
• fixes the connected James proof using universal covers/local coefficients;
• gives X=S¹ as a regression test;
• corrects the Thom-space factorization;
• expands Bott through broken geodesics and Morse–Bott attachments;
• introduces a smallness strategy;
• separates stable and honest parallelizability;
• distinguishes even-dimensional forms from odd-dimensional formations;
• normalizes the unstable representative of ν²;
• makes oriented recognition explicit.

The prose roadmap has responded well. The main problem is that the architecture in Suggested.lean does not encode the geometry it claims to encode.

1. A pointwise orientation function is not a manifold orientation

SmoothClosedOrientedCycle stores

orientationAt : M → Orientation ℝ E ι

with no continuity or chart compatibility. The final oriented Poincaré theorem likewise accepts arbitrary pointwise functions oM and oS.

This is false. On connected S⁶, choose oM to equal the standard orientation at one point and its negative elsewhere. The type accepts this input. The orientation sign of the derivative of a diffeomorphism is locally constant, hence constant on a connected manifold, so no diffeomorphism can satisfy the displayed pointwise equation.

Use the actual shared Manifold.Orientation I M ι object, or Manifold.OrientedManifold, whose data include chart compatibility and local constancy. Do not replace it by its pointwise evaluation function.

2. The framing structures are vacuous

The file defines an honest tangent framing as

frameAt : M → E ≃L[ℝ] E

and a stable framing similarly by pointwise equivalences between fixed model spaces.

These maps do not refer to the tangent bundle. Every space admits the proposed TangentFraming by taking the identity equivalence at every point. In particular, the definition would “frame” S², despite its tangent bundle being nontrivial.

A tangent framing must be a smooth vector-bundle equivalence

$$ TM\simeq M\times\mathbf R^n, $$

and a stable framing must be an equivalence

$$ TM\oplus\varepsilon^r\simeq\varepsilon^{n+r}, $$

with the collar-relative compatibility stored for fillings.

The same problem propagates into FramedCycle, AlmostFramedCycle, the historical A_n carrier and Pontryagin–Thom.

3. The filling carrier has no manifold-with-boundary relation

StableFramedFillingCycle currently stores only:

• a code;
• an unrelated boundary code;
• a homotopy marking of that boundary code;
• a pointwise “stable framing”.

It does not say:

• the realization is a compact connected oriented manifold with boundary;
• the second realization is its boundary;
• there is a boundary inclusion/identification;
• a collar is chosen;
• the framing is product-compatible on that collar.

Consequently stableFraming_destabilizes does not have the hypotheses stated in the README and is not a meaningful version of the relative destabilization theorem.

This carrier should consume the actual manifold-with-boundary/collared-cobordism object from GeometricTopology rather than place two unrelated atlas codes beside each other.

4. SmoothAtlasCode does not contain the laws needed for its realization

The public structure stores charts, transitions and a groupoid-membership condition, but not:

• source/target equations;
• identity and inverse laws;
• cocycle laws;
• cover/surjectivity data;
• separation conditions.

The docstring says “the implementation adds” these laws, but they need to be fields or derived from a pre-existing gluing structure if this is the public code used to define the small skeleton. Otherwise gluingSetoid and its realization are unconstrained.

5. The Pontryagin–Thom maps are bare functions

PontryaginThomFactorization stores

collapse : Sphere (...) → thomSpace
augmentation : thomSpace → Sphere k

rather than continuous pointed maps. Since continuity at the collapsed complement and pointedness are central theorems, the carrier should at least expose ContinuousMap/pointed-map data.

6. The Wall carriers do not encode quadratic forms or formations

EvenWallForm currently has:

pairing : Matrix ... ℤ
quadratic : Fin rank → ℤ
unimodular : IsUnit pairing.det

A quadratic refinement is a function on the whole module ℤ^r, not on the basis index, and it must satisfy the relevant polarization and parity identities. The pairing also needs the (-1)^q-symmetry law.

OddWallFormation similarly lacks the conditions saying its displayed submodules are isotropic direct summands/lagrangians and form a genuine quadratic formation.

As written, WallSurgeryClass is a quotient of arbitrary matrices and functions, not Wall's L_n(ℤ).

Verdict

Major changes requested. The README is now strong, but the representative Lean carriers for orientation, framing, boundary fillings and surgery data are mathematically wrong. They need to be rebuilt around the actual shared geometric objects before this roadmap can merge.

---

Cross-roadmap disposition (applies across #279–#284)

• #279: fix one gluing signature; then merge.
• #280: add the complex-linear analytic input and group-valued connecting API; then merge.
• #281: repair the lattice foundation and monomial-domain theorem before further review.
• #282: make cusp data primitive and resolve degree/Riemann–Hurwitz ownership.
• #283: fix the low-degree relative-homotopy carrier; then merge.
• #284: keep the revised README, but substantially rewrite Suggested.lean around genuine manifold orientations, tangent-bundle trivializations, collared boundary data and actual quadratic forms/formations.

[Paul-Lez]

🤖 Addressed in e7d1d6e. The representative Lean interfaces now use a chart-compatible manifold-orientation quotient; canonical tangent-bundle trivializations; the actual intrinsic boundary with an outward-normal-first, half-open collar; a lawful finite atlas with canonical quotient topology; continuous pointed Pontryagin--Thom maps built from a normal prebundle and tubular neighbourhood; and whole-module Wall forms plus genuine formations and generated stable equivalence. The final recognition signature consumes manifold orientations themselves. The focused Lean check and static checks pass.

[CBirkbeck]

Part of the third adversarial review of the reusable-roadmap split (#279–#284) and companion roadmaps (#288, #81, #250), reviewed 26 August 2026 against the current heads. This section covers #284 — High-dimensional differential topology and homotopy spheres.

Head reviewed: e7d1d6ea67be787c8c6b04f62341bc222f430df7

What has been fixed

The mathematical carriers that were previously wrong are now substantially repaired:

• orientations use Manifold.Orientation;
• tangent framings trivialize the actual tangent bundle;
• stable and normal framings use bundle trivializations;
• fillings carry collared manifold-with-boundary data;
• Pontryagin–Thom uses pointed maps and an actual normal bundle;
• Wall forms use bilinear forms, quadratic refinements and genuine lagrangians;
• SmoothAtlasCode now has cover, inverse and cocycle laws.

The README is now a serious roadmap.

1. Supplier-owned APIs are still redeclared in public namespaces

Suggested.lean defines, in the root/shared namespaces, substantial versions of:

• Manifold.OrientationLift and Manifold.Orientation;
• tangent coordinate changes and orientation preservation;
• TauCetiRoadmap.GeometricTopology collar and boundary carriers.

The README simultaneously says that Heegaard Floer owns orientation and GeometricTopology owns collars and cobordisms.

There is a legitimate need to mirror an open Mathlib or sibling interface before it lands. But that mirror should be visibly temporary:

• place it in an internal namespace;
• record an exact deletion/import gate;
• avoid presenting it as a second public owner.

Otherwise the supplier PR will collide with declarations already exported by this roadmap.

2. The central geometric quotient API has disappeared from Suggested.lean

The earlier representative file at least exposed:

• the h-cobordism relation;
• the quotient defining Theta_n;
• framed bordism;
• the almost-framed and filling groups;
• the Kervaire–Milnor maps and exactness;
• Theta_6 = 0.

The corrected file now seeds the substrate, framing and Wall carriers, but contains no representative Theta_n quotient or Kervaire–Milnor sequence declarations. A search of the current file finds no Theta, homotopySphereGroup, or geometric h-cobordism quotient.

Because Suggested.lean is the architecture check, the absence matters: CI can no longer distinguish the intended geometric group from an arbitrary AddCommGrpCat inserted later.

Add at least representative declarations for:

• geometric h-cobordism witnesses and their setoid;
• HomotopySphereClass and Theta_n;
• framed/almost-framed/filling quotients;
• the three Kervaire–Milnor maps;
• exactness at one displayed segment;
• the final Theta_6 theorem.

These should use the newly corrected orientation, framing and collared-boundary carriers.

Verdict

Major changes requested to Suggested.lean; the README can largely remain.

---

Cross-roadmap dependency recommendation — Topology chain

AlgebraicTopology (with based relative homotopy)
    ↓
HomotopySpheres

HomotopySpheres should import the supplier declarations and expose its geometric quotient API rather than mirror shared carriers indefinitely.

Recommended disposition (all nine PRs)

1. Merge after routine CI: #279, #280, #281.
2. Small focused repairs: #283, #81.
3. Coordinate and repair together: #282 and #288.
4. Rewrite the representative architecture before merge: #284.
5. Complete the class-field endpoint and state the global-function-field scope: #250.

[Paul-Lez]

🤖 Addressed in 4f6e2f3. The orientation and collar supplier mirrors are now internal and have exact deletion/import gates. The representative API restores geometric h-cobordism witnesses and the literal Type-0 HomotopySphereClass / Theta quotient, the framed, almost-framed, and filling bordism quotients, all three Kervaire–Milnor maps, the displayed exactness segment, and Theta_6 = 0. Focused Lean elaboration passes with no errors.