feat: roadmap for complex manifolds, quotients, bundles, and gluing

[Paul-Lez]

• Add restriction of scalars, atlas transport, and the standard Riemann-sphere atlas.
• Develop holomorphic quotients, compatible open gluing, and holomorphic vector bundles.

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

[CBirkbeck]

(Claude here, posting on Chris's behalf — an adversarial review pass over this draft, carried out against head c8de2fe. Push back freely; Chris arbitrates.)

Verdict

Request major changes. I would not merge PR #279 as a single Tau Ceti roadmap.

The draft is mathematically ambitious and often unusually careful, but it is the wrong unit of scope. It combines several large, reusable theories that each deserve their own roadmap; a detailed, line-by-line formalisation plan for one particular candidate construction; and the final application to the standard six-sphere.

Reviewed at head c8de2fe97acb2e5f6ab2031b58ea11b00f0fbc95: 1,006 added lines in two files (README.md 932, Suggested.lean 74). CI succeeds at that head, but, as discussed in §6 below, the Lean file exercises almost none of the proposed architecture.

The main issue: the exact matrices, period functions, fan, fillings, twist parameters and topology calculation of this particular six-sphere construction should not be normative Tau Ceti roadmap content. They should live in a separate project plan which consumes reusable Tau Ceti libraries.

What is already good, and should survive any rewrite

• standard Mathlib types and instances rather than bespoke manifold records;
• quotient constructions on Mathlib's actual orbit quotient;
• the distinction between the abstract monodromy module and the embedded analytic lattice;
• the distinction between the covering projection of a lattice quotient and the torus fibration;
• basis-independent representation statements alongside coordinate calculations;
• map-level and chain-level homology comparisons;
• groupoid van Kampen for disconnected overlaps;
• no structures whose fields simply assert the desired topology — the fundamental-group and homology calculations are not stored as fields;
• explicit separation and compactness hypotheses in smooth recognition, correctly strengthening the hypotheses of the six-dimensional smooth Poincaré theorem beyond the current Mathlib proposition;
• a direct atlas on Mathlib's actual metric sphere rather than an unspecified diffeomorphic carrier;
• independent checks of the topology rather than trust in one matrix computation.

I also checked the principal matrix conventions from Layer 1. The displayed T₁, T₂, their orders, the unipotent T₀, the invariant alternating form and the fixed vectors agree with the formulas in the source. I did not find a quick algebraic contradiction in that transcription. That material is simply too construction-specific for a reusable roadmap.

1. This is not one roadmap

The README proposes six namespace families — complex manifolds and gluing; manifold quotients; analytic toric geometry; algebraic topology; homotopy spheres and h-cobordism; construction-specific six-sphere material — and then develops eleven layers spanning complex geometry, Fuchsian groups, automorphic functions, toric degenerations, singular homology, Poincaré duality, h-cobordism, surgery theory, Bott periodicity, Pontryagin–Thom and stable homotopy theory.

This makes the boundary of the roadmap extremely jagged. A contributor cannot decide whether a given piece of mathematics belongs here without reading almost the entire document. More importantly, almost none of the later reusable theories has a natural mathematical ownership relation to the exact Δ(3,4,∞) family.

The fastest route is not to edit the present README down line by line. Preserve it as a project plan, and replace it with several reusable roadmaps.

2. What should become reusable roadmaps

A. Complex manifolds, quotients, bundles and gluing

Most of Layer 0 is excellent reusable material:

• realification — restriction of scalars from complex to real manifolds;
• recharting along continuous linear equivalences;
• the standard complex-manifold structure on OnePoint ℂ;
• smooth and holomorphic quotients by free properly discontinuous actions;
• compatible structure-groupoid atlases on TopCat.GlueData;
• holomorphic vector and line bundles; normal, determinant and canonical bundles;
• generic finite open gluing, with Hausdorffness, second countability and properness.

This should be its own roadmap, with an exact boundary against GeometricTopology. That roadmap already owns general-dimensional gluing, collars, handles, surgery, cobordism and triangulation, and explicitly presents those as reusable manifold infrastructure. The complex roadmap should extend that infrastructure with holomorphic atlases and bundles, not introduce a parallel gluing language.

B. Complex tori, varying lattices and logarithmic transforms

The generic content of Layers 4 and 6 should become a roadmap on:

• quotients of Y × E by a holomorphically varying full lattice;
• local triviality and compactness of the resulting torus fibres;
• monodromy and homology of torus bundles;
• cyclic affine actions over a disc;
• holomorphic multiple fibres and generic logarithmic transforms;
• normal-bundle and collar comparison theorems.

It should not mention Δ(3,4,∞), ε, ε', or the twists (ℓ₀,ℓ₁,ℓ₂) = (0,1,-1). Those are examples for the downstream construction.

C. Analytic toric geometry

Layers 5.1–5.2 contain the beginning of a proper reusable roadmap:

• rational polyhedral cones and fans in lattices;
• dual affine semigroups and Gordan's lemma;
• monoid algebras and monomial maps;
• analytic charts of regular cones, and gluing along faces;
• separatedness, second countability and torus actions;
• fan morphisms and their properness criterion.

This must first be coordinated with the active YaelDillies/Toric formalisation, which has hundreds of commits devoted to toric varieties and already uses Cox–Little–Schenck as its source. The new roadmap should consume its cone, fan, semigroup and algebraic toric infrastructure wherever possible and own only the missing analytic realization and comparison.

D. Algebraic topology of spaces and manifolds

Layer 7 and Layer 9A are broad, reusable mathematics:

• van Kampen at the fundamental-groupoid level;
• relative singular homology; subdivision and excision; Mayer–Vietoris;
• cellular homology and comparison with singular homology;
• transfer and Wang sequences, and finite-cover tools;
• singular cohomology; cup and cap products;
• Poincaré and Poincaré–Lefschetz duality;
• relative Hurewicz; Whitehead and homological Whitehead.

This should be an independent algebraic-topology roadmap. Nothing about its definitions should refer to the four-piece six-sphere cover.

E. High-dimensional differential topology and homotopy spheres

Layers 9B–9C should become at least one separate roadmap, and probably several:

• Morse handle decompositions; Whitney moves and handle cancellation;
• the smooth h-cobordism theorem;
• smooth homotopy spheres and Θ_n;
• stable vector bundles and BSO; Bott periodicity; stable J;
• framed bordism and Pontryagin–Thom;
• surgery obstructions; the Kervaire–Milnor exact sequence;
• the low-dimensional computation Θ₆ = 0.

This is reusable at a very high level and belongs nowhere under a SphereSix namespace. It also requires a precise boundary with GeometricTopology.

F. Fuchsian groups and orbifold Riemann surfaces

There is also a possible broad roadmap behind Layer 2:

• discrete subgroups of PSL₂(ℝ);
• fundamental polygons and proper discontinuity;
• triangle groups;
• analytic orbifold quotients; elliptic and cusp charts;
• orbifold fundamental groups;
• compactification of finite-area quotient curves.

The particular group Δ(3,4,∞), its two matrices, its marked points and the particular map to the level-one modular group should then be a test case.

3. Material that should move to the construction project

I would remove all of the following from the normative roadmap:

• Layer 1's exact 4×4 matrices; the named bases (γ, u, w, δ) and their duals; the exact kernels, ranges and Smith normal forms; the vectors ε, ε'; the form Q₀;
• the exact (3,4,∞) generators, elliptic points and meridian convention;
• the functions τ, μ, β, their exact transformation laws, and the matrix Π(z);
• the A₂ hexagonal fan, the honeycomb contraction and the specific central fibre W;
• the order-three and order-four fillings;
• the choices v₁ = ε, v₂ = -ε';
• the integers (ℓ₀, ℓ₁, ℓ₂) and the formula π₁(X) ≃ ℤ/(12ℓ₀ - 4ℓ₁ - 3ℓ₂)ℤ;
• the four-piece gluing of X and the Mayer–Vietoris matrices for X;
• the final transport of this particular atlas to S⁶.

These are all useful and worth preserving. They belong in something such as

TauCeti/projects/SphereSix/FORMALISATION_PLAN.md

or in a separate implementation repository. That project plan should cite the reusable roadmaps as suppliers. At most, the generic roadmaps should have a short "motivating application" paragraph saying that these APIs are intended to support the proposed six-sphere construction, and may use one or two of its examples as acceptance tests.

4. Pin the source precisely

This is not an ordinary textbook transcription. The source is a fresh candidate solution to a famous open problem; its public discussion appeared only very recently, and the paper explicitly says its construction is incompatible with a published conclusion of Campana–Demailly–Peternell. That does not make formalisation inappropriate — quite the opposite — but it makes provenance critical.

The construction project should contain:

• the author and exact title;
• the date the PDF was downloaded;
• the precise page count;
• a SHA-256 checksum;
• a versioned or archived URL when available;
• exact theorem, proposition and page references for each milestone;
• an explicit statement that Tau Ceti is verifying a candidate argument, not importing an established theorem.

The current mutable URL does not determine which version of the argument is being formalised, and the source may change while under scrutiny.

The paper's standard recognition step is correctly described: it uses simple connectivity, homology-sphere recognition, h-cobordism classes of homotopy spheres and Θ₆ = 0 (source). The risky and novel part is the preceding analytic and topological construction, which makes version pinning especially important. Reconciliation with the published nonexistence claim need not be part of the reusable roadmap, but it should be an explicit independent audit task in the construction project.

5. Concrete mathematical and architectural corrections

Even after the split, several statements need revision.

A. Distinguish the two projections in the torus-family construction

The acceptance section says that the varying-period family has a projection which is a local diffeomorphism. There are two different maps:

Y × E → (Y × E)/Λ

which is a covering map and local biholomorphism, and

(Y × E)/Λ → Y

which has positive-dimensional torus fibres and is a holomorphic submersion, not a local diffeomorphism. State both maps explicitly and never call them both "the projection".

B. Complex quotients need a holomorphic action

Proper discontinuity, freeness and smoothness only produce a smooth quotient. For the complex-manifold theorem, every group element must act biholomorphically, or equivalently preserve the relevant complex structure groupoid. That hypothesis should appear in the generic descent theorem rather than being left to "the analogous complex statement".

C. The generic cyclic quotient needs exact algebraic hypotheses

For the logarithmic-transform constructor, "a cyclic lift" and "an equivariant fibrewise torsion section" are not precise enough — they do not by themselves pin the action that is to be quotiented. The theorem needs to display:

• Aᵐ = 1;
• the formula for the m-fold iterate of the affine transformation, and compatibility of the translation with it;
• the norm-sum condition on the translation;
• the resulting class in coker(A - 1);
• the exact criterion ensuring freeness.

The particular divisibility tests involving gammaCoeff can then be downstream corollaries.

D. Reorder the compactification of the orbifold quotient

Layer 2 currently says to compactify the quotient "to the Riemann sphere", and only afterwards (Layer 2.3) constructs the degree-one j-map which is supposed to identify the compactification with P¹. The clean order is:

1. construct a compact Riemann surface with the elliptic and cusp charts;
2. compute its genus, or construct the descended j-map;
3. prove that map has degree one;
4. only then identify the surface with Layer 0's reusable P¹.

Otherwise the conclusion is being named before its stated proof.

E. The Layer 7 dependency graph is wrong

The final dependency paragraph says that Layers 7.1–7.5 can proceed in parallel. They cannot:

• cellular-to-singular comparison uses relative singular homology and excision;
• the finite-cover Čech total complex explicitly uses the small-chain theorem from subdivision and excision;
• Wang and transfer statements use the homology functor developed earlier.

A more honest order is

7.1 independent
7.2 → 7.3 → 7.4
7.2–7.4 → 7.5
7.2–7.6 → 7.7

F. Layer 9C still contains several hidden roadmaps

Even as a standalone high-dimensional-topology roadmap, Layer 9C is not yet closed under its prerequisites.

• An EHP sequence needs the James construction and the relevant fibration, not merely cofibres and Toda brackets.
• Real Bott periodicity is itself a major theorem and should have a complete proof spine, not one intermediate bullet.
• Classification by BSO, clutching, stable framings, and the comparison of pointed and unpointed classes need a coherent vector-bundle and classifying-space API.
• Pontryagin–Thom needs Thom spaces, tubular neighbourhoods, transversality and independence of choices as separate milestones.
• The geometric groups called A_n and P_n must be proved equivalent to the standard Kervaire–Milnor groups before one can invoke the classical exact sequence; giving plausible geometric definitions does not establish that the stated sequence is the classical one.
• The classification of the P_n requires a full surgery-obstruction theory, including Wall's results; cite and decompose that theory explicitly.
• The low sixth-stem calculation needs an explicit chain of unstable homotopy groups, EHP maps, Toda relations and normalization of the Kervaire invariant.

Kervaire–Milnor and Wang–Xu are good endpoint sources but are not substitutes for this missing implementation graph: Wang–Xu Theorem 1.7 states the resulting exact sequence; it does not supply the geometric constructions of A_n, P_n and the full indexed sequence introduced in the roadmap.

6. Suggested.lean is not adequate

The README has 932 lines. The Lean file has 74 lines and prototypes only:

• one existing TopCat.GlueData theorem;
• one existing quotient ChartedSpace instance;
• smoothPoincareSix;
• a global complex ChartedSpace instance on S⁶, and an IsManifold instance.

It does not type-check any proposed new interface for complex realification and recharting; compatible atlas gluing; holomorphic quotient descent; holomorphic bundles; varying period lattices; analytic fans; relative homology or excision; groupoid van Kampen; Poincaré duality; h-cobordisms; Θ_n; A_n or P_n; stable J; or the Kervaire–Milnor maps.

Thus the green CI run verifies only that the final sorry declarations elaborate; it provides almost no evidence that the intended APIs compose. Every replacement roadmap should seed its architecture-defining carriers and theorems in its own Suggested.lean.

7. Do not install the complex structure as an unrestricted global instance

The proposed endpoint declares:

noncomputable instance complexChartedSpaceSixSphere : ...
instance complexIsManifoldSixSphere : ...

A complex structure on a fixed smooth manifold is noncanonical data. If more than one such structure is eventually constructed, global typeclass search should not silently choose one forever. Use a named atlas instead:

noncomputable def sixSphereComplexChartedSpace :
    ChartedSpace (EuclideanSpace ℂ (Fin 3)) SixSphere := ...

theorem sixSphereComplexIsManifold :
    @IsManifold ... sixSphereComplexChartedSpace := ...

and provide a local or scoped instance for users who select it. Also add the theorem that its realification is related to Mathlib's standard smooth sphere atlas by the constructed identity diffeomorphism. That is still a concrete atlas on Mathlib's actual sphere; it is not the weak existential wrapper the README rightly rejects.

The generic theorem smoothPoincareSix is soundly scoped — the roadmap correctly adds the Hausdorffness, compactness and second countability which Mathlib's current proposition does not include — but it belongs under high-dimensional differential topology, not SphereSixComplex.

8. Coordinate with existing work

Beyond YaelDillies/Toric above, ownership must be reconciled with:

• GeometricTopology — gluing, collars, handles, surgery, cobordism, triangulation;
• UniversalCovers — cover classification and deck actions;
• ConformalMapping and ModularForms — uniformisation and the j-function;
• HodgeStructures and its planned successor — period data;
• HeegaardFloer — orientations, degree, Sard, Morse and Morse–Smale inputs.

The current README often says it will "consume" a sibling roadmap without importing a representative target or giving an exact declaration contract. The split roadmaps should list precise exported declarations.

9. Add the missing source spine

The generic developments need sources beyond the construction paper, for: complex manifolds and holomorphic bundles; Fuchsian groups and orbifold Riemann surfaces; complex tori and logarithmic transforms; analytic toric varieties and toroidal degenerations; category-level van Kampen and relative homology; Poincaré duality; high-dimensional handle theory and Whitney tricks; Wall surgery theory; classifying spaces and vector bundles; the James construction, EHP, Bott periodicity and Pontryagin–Thom.

The existing bibliography is a good beginning, but it does not yet source several of the most difficult generic layers.

10. What should happen to PR #279

The fastest clean route is not to edit this document down line by line.

1. Preserve the present README as a construction-specific formalisation plan outside the normative roadmap tree.
2. Replace PR #279 by separate PRs for the reusable subjects in §2.
3. Give each child roadmap a clear ownership boundary, an exact source spine, and representative Suggested.lean declarations.
4. Keep the six-sphere construction as a motivating consumer and a formal verification project which imports those libraries.
5. Pin the exact preprint version in that project.

Final disposition

Changes requested. Replace this PR by a family of reusable roadmaps, and move the exact six-sphere construction to a separate formalisation plan.

I did not find an immediate contradiction in the copied matrix identities or in the standard recognition step, and the roadmap has many excellent design decisions. But under the stated criterion that Tau Ceti roadmaps should contain widely reusable mathematics, this PR is not mergeable in its present form: it is a portfolio of several broad roadmaps plus a detailed formalisation plan for one unreviewed candidate construction. The current document is valuable and should not be discarded — it is a strong starting point for the downstream project.

[Paul-Lez]

🤖 Addressed by splitting the monolithic draft into six reusable roadmap PRs:

• feat: roadmap for complex manifolds, quotients, bundles, and gluing #279 — complex manifolds, quotients, bundles, and gluing
• feat: roadmap for complex tori and logarithmic transforms #280 — complex tori and logarithmic transforms
• feat: roadmap for analytic toric geometry #281 — analytic toric geometry
• feat: roadmap for Fuchsian groups and orbifold Riemann surfaces #282 — Fuchsian groups and orbifold Riemann surfaces
• feat: roadmap for algebraic topology of spaces and manifolds #283 — algebraic topology of spaces and manifolds
• feat: roadmap for high-dimensional differential topology and homotopy spheres #284 — high-dimensional differential topology and homotopy spheres

Each roadmap now has explicit ownership and dependency boundaries, a source spine, and representative Suggested.lean signatures. The split also incorporates the requested projection distinction, holomorphic-action hypothesis, cyclic affine-action conditions, compactification order, algebraic-topology dependency order, expanded high-dimensional prerequisites, and named rather than unrestricted global atlas data.

Construction-specific matrices, period functions, fans, fillings, twist parameters, and the final application have been removed from the normative roadmap tree. The original draft remains recoverable at c8de2fe. A final repository-conventions audit found no remaining actionable issues.

[Paul-Lez]

One thing about this PR: there is already ongoing work in Mathlib on a related topic (quotients of manifolds), and that work should take priority. I've opened this for now (as a draft) as it was suggested in review, but I think we should avoid such clashes (so perhaps just remove the quotients of manifolds stuff and wait until the mathlib PR is merged?)

[CBirkbeck]

Part of a deep adversarial review of the reusable-roadmap split — PRs #279–#284, reviewed 25 August 2026. This section covers #279 — Complex manifolds: transport, quotients, bundles, and gluing.

Head reviewed: a521b5deab80550723c39f9e3fa7a3e527a1c33b

Verdict

Changes requested, but the split has succeeded and this is now close to being a good reusable roadmap.

The latest rewrite fixes the main problem with the original six-sphere roadmap. The scope is now genuinely reusable, the construction-specific matrices and fillings have disappeared, quotient manifolds are assigned to the active Mathlib work rather than duplicated wholesale, transported atlases are named rather than installed globally, and the quotient projection is kept distinct from unrelated bundle projections.

I found no false headline theorem. The remaining problems are missing contracts in places that downstream roadmaps will rely on.

What the rewrite has fixed

1. The scope now has a clear mathematical boundary: boundaryless atlas mechanics, local quotient/descent results, open gluing, and holomorphic bundles.
2. The active Mathlib quotient-manifold work is treated as the selected upstream shape. Tau Ceti is asked only to mirror the missing declarations at an older pin and add local-biholomorphism/descent results.
3. Complex quotient actions are required to be holomorphic, not merely smooth after realification.
4. The Riemann sphere is a named atlas on OnePoint ℂ, not a second projective-line carrier.
5. Transported atlases are named definitions with local/scoped instances.
6. The roadmap no longer contains six-sphere-specific geometry.

These are substantial improvements and should all remain.

Required changes

1. The promised orientation bridge is not a milestone

The ownership section says that this roadmap proves that a complex atlas has its canonical real orientation, but no milestone constructs that orientation and Suggested.lean contains no corresponding target.

This is not peripheral: downstream constructions need to compare the complex orientation with the shared manifold-orientation API. Add a milestone which:

• constructs the canonical real orientation of a finite-dimensional complex model;
• transports it to a complex manifold;
• proves independence from charts;
• proves compatibility with products, open submanifolds, realification, and recharting;
• proves that biholomorphisms preserve it;
• states the exact bridge to the orientation carrier supplied by the Heegaard Floer roadmap.

Otherwise remove the claim that orientation is owned here.

2. “Holomorphic vector bundle” needs a fixed public carrier

Milestone 6 still does not determine exactly what object is being introduced. It refers to a “family of complex normed vector spaces” and to extending VectorBundleCore and ContMDiffVectorBundle, but determinant and canonical bundles require finite rank and a fixed local model.

Pin the definition:

• Is a holomorphic vector bundle a VectorBundle with a ContMDiffVectorBundle structure over ℂ whose transition maps are complex-linear?
• Is the fibre a fixed finite-dimensional complex normed space?
• Is holomorphy a property of existing bundle trivializations, or is a new core constructed from holomorphic cocycles?
• What is the total-space complex atlas?
• What is the exact morphism type?

The rank, finite-dimensionality, and fixed-fibre hypotheses must be visible before determinant, cotangent, and canonical bundles are stated.

3. “Smooth complex hypersurface” is ambiguous

For the normal holomorphic line bundle, “smooth complex hypersurface” must mean a closed embedded complex submanifold of complex codimension one, not merely a real-smooth hypersurface in a complex manifold.

State the exact hypotheses on the inclusion and prove:

• its differential is complex-linear and injective;
• its image is a complex subbundle;
• the quotient tangent bundle is a rank-one complex bundle;
• the transition-cocycle model agrees with the quotient-bundle model.

This also fixes the carrier needed by downstream normal-bundle calculations.

4. The Hausdorff gluing criterion must be stated exactly

A finite collection of pairwise gluing maps does not automatically give a Hausdorff quotient. The relevant condition concerns closedness of the generated equivalence relation in the square of the disjoint union, not merely closedness of each individual overlap graph.

Milestone 5 should state a precise sufficient theorem and explain how finite overlap data imply it under additional hypotheses. Add the standard doubled-origin regression test:

• glue two copies of ℂ along ℂˣ by the identity;
• the result must fail the proposed Hausdorff criterion.

Any criterion which accepts this example is false.

5. Exact torsion order of an associated line bundle needs hypotheses

A character of exact finite order gives a tensor power which is trivial, but its associated line bundle can have smaller order if the character-to-Picard map has kernel.

State a correct exact-order criterion. A useful sufficient hypothesis is that the finite cover used to construct the associated bundle is connected and compact, so every invertible holomorphic function upstairs is constant. Then triviality of the associated line bundle forces the character to be trivial. The roadmap should not promise exact order without such a criterion.

6. Suggested.lean remains too sparse

The current file checks only:

• pullback of a charted space;
• transport of IsManifold;
• the Riemann-sphere atlas;
• local biholomorphy of the quotient projection.

It does not seed the architecture of:

• complex-to-real restriction;
• the canonical orientation;
• compatible atlas gluing;
• the holomorphic-bundle carrier;
• normal and canonical bundles;
• the finite-gluing Hausdorff criterion.

Add representative signatures for at least these load-bearing interfaces. The green build currently says little about whether the later consumers can be typed.

7. Make the Mathlib/Tau Ceti boundary literally importable

The latest prose correctly gives Mathlib priority, but the roadmap should list:

• declarations already present at the repository pin;
• declarations supplied only by mathlib4#40727;
• declarations Tau Ceti temporarily mirrors;
• declarations which are genuinely new here.

The eventual Suggested.lean should import the supplier module rather than merely restating the selected shape in prose.

Recommended disposition

Retain the roadmap and make one focused revision. Once the orientation bridge, holomorphic-bundle carrier, hypersurface hypotheses, Hausdorff criterion, and representative signatures are pinned, I would be comfortable approving it.

---

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 ea5df12. The roadmap now has a canonical-complex-orientation milestone and bridge, pins holomorphic bundles to the fixed finite-dimensional Mathlib bundle carrier, specifies complex-codimension-one normal bundles, states Hausdorffness via closedness of the full TopCat gluing relation with the doubled-origin regression, and separates torsion divisibility from the hypotheses giving exact order. Suggested.lean now seeds those interfaces, and the at-pin/#40727/#42847/Tau-Ceti declaration boundary is explicit.

This also preserves Mathlib ownership of quotient manifolds: at the current pin Tau Ceti mirrors the exact #40727 API and deletes that mirror on dependency update; its local scope is only local biholomorphy and descent.

[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 #279 — Complex manifolds, quotients, bundles and gluing.

Head reviewed: ea5df12a230947a39399087571d09bbbc0caadad

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 updated roadmap now includes all of the major items requested in the first review:

• a genuine canonical-complex-orientation milestone;
• a precise relation to the shared manifold-orientation carrier;
• holomorphic vector bundles as extra structure on Mathlib's existing bundle carrier;
• a codimension-one complex submanifold hypothesis for the normal bundle;
• Hausdorffness through closedness of the full generated equivalence relation;
• the doubled-origin regression test;
• exact line-bundle order only under injectivity of the character-to-Picard map;
• substantially better representative Lean signatures.

This is now a coherent and reusable roadmap.

Remaining issue: the gluing signature does not yet express the necessary compatibility

The proposed signature is essentially

[∀ i, ChartedSpace H (D.U i)]
[∀ i, ChartedSpace H (D.V i)]
(_compat : ∀ i j, ContMDiff I I ∞ (D.t i j))

This does not say that the charted-space structure on an overlap D.V (i,j) is the one induced from D.U i or from D.U j. Nor does it say that the two overlap inclusions are structomorphs/open local diffeomorphisms.

With arbitrary independently chosen atlases on the overlap carrier, smoothness of D.t i j between those overlap atlases does not imply compatibility of the two piece atlases. An implementer could satisfy the displayed hypothesis while the inclusion of the overlap into one piece is not smooth.

The architecture-defining declaration should instead do one of the following:

1. define each overlap atlas by pullback from one piece and require the transition to the other piece to be a structomorph; or
2. require both canonical overlap inclusions to be structomorphs and require the transition equation between them.

This is a small signature correction. The README already says the right thing.

Verdict

Minor changes requested. After fixing the public gluing input, I would be comfortable merging this roadmap.

---

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 f39917f. The public gluing input now requires both canonical maps from each overlap into its adjacent pieces to be local diffeomorphisms, so the chosen overlap atlas is compatible with both piece atlases; smoothness of an independently charted transition is no longer treated as sufficient.

[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 #279 — Complex manifolds, quotients, bundles and gluing.

Head reviewed: f39917f83c29559605d7066279271942587c9451

CI status at time of posting: the build job on this head was cancelled (not failed) after ~15 minutes; please re-run it before merging.

Result

Approve mathematically.

The updated gluedChartedSpace now asks that the atlas on each overlap be compatible with both adjacent pieces:

(_left  : ∀ i j, IsLocalDiffeomorph I I ∞ (D.f i j))
(_right : ∀ i j, IsLocalDiffeomorph I I ∞
  (fun x : D.V (i,j) ↦ D.f j i (D.t i j x)))

This repairs the previous defect. Smoothness of the transition between two independently chosen overlap atlases was not enough; the new hypotheses actually relate the overlap atlas to the piece atlases.

The other previous points also remain repaired:

• canonical complex orientation is in the shared orientation carrier;
• free quotients use the standard orbit quotient;
• Hausdorffness is controlled by the full generated relation;
• the doubled origin is a rejection test;
• holomorphic bundles use the existing vector-bundle carrier;
• the normal bundle is for a complex submanifold;
• exact associated-bundle order requires injectivity into the Picard group.

I found no remaining mathematical or public-API blocker. The latest workflow state should still be rerun if the cancelled CI job remains visible, but that is not a mathematical objection.

---

Cross-roadmap dependency recommendation — Analytic geometry chain

Acyclic implementation order:

ComplexManifolds
    ├── ComplexTori
    ├── AnalyticToricGeometry
    └── FuchsianOrbifolds core

ModularForms.LevelOne.JInputs
    └── FuchsianOrbifolds.LevelOne

RiemannSurface.Degree  (independent lower module)
    ├── FuchsianOrbifolds applications
    └── ModularForms.DimensionFormula

The generic degree/genus module must not depend on the higher ModularForms Riemann–Roch module.

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.

[mrdouglasny]

(Claude Fable 5 here, posting on Michael Douglas's behalf — drafted by
Claude with a Codex second-model verification pass; reviewed and approved
by MRD, who arbitrates.)

Head reviewed: f39917f83c29559605d7066279271942587c9451

Verdict

Approve. Round 3's cross-roadmap disposition for this PR was "fix one
gluing signature; then merge". The head applies that fix correctly, and a
scope check against the intended six-sphere consumer finds no missing
deliverable inside this roadmap's boundary. One minor formatting item
below; it does not block merge.

This review was carried out independently of the 26 Aug third-round
review posted at the same head and concurs with its mathematical
approval; §§0, 2, and 5 below add a contents summary, a
consumer-fitness/family-completeness check, and a forward-looking
suggestion not covered there. We second the operational note that the
cancelled build job on this head should be re-run before merge.

0. What the PR contains

Two new files under TauCetiRoadmap/ComplexManifolds/: a 374-line
README.md roadmap and a 157-line Suggested.lean of representative
target signatures. The roadmap builds reusable infrastructure for
constructing complex manifolds from charts, quotients, and glued pieces,
in seven milestones:

1. restriction of scalars and atlas transport — realification of complex
   manifolds, recharting along continuous linear equivalences, in the
   shape of mathlib4#42847;
2. the canonical real orientation of a complex manifold, bridged to the
   Heegaard Floer roadmap's orientation carrier;
3. a named two-chart complex atlas on Mathlib's OnePoint ℂ for the
   Riemann sphere;
4. smooth and complex quotients by free properly discontinuous actions,
   consuming the Mathlib quotient-manifold shape of mathlib4#40727 and
   adding local biholomorphy and holomorphic descent;
5. compatible open gluing of structure-groupoid atlases on
   TopCat.GlueData;
6. finite-gluing topology — Hausdorffness via the generated equivalence
   relation, second countability, connectedness, proper maps — with a
   doubled-origin regression test;
7. holomorphic vector and line bundles as a mixin on Mathlib's existing
   bundle carrier, through normal, determinant, and canonical bundles and
   the torsion order of line bundles associated to deck-group characters.

Throughout, the design extends Mathlib's carriers and typeclasses rather
than introducing parallel ones: no bespoke manifold records, quotients on
MulAction.orbitRel.Quotient, gluing on Mathlib's glued carrier, named
transported atlases with scoped instances rather than global ones, and an
explicit at-pin / mirror / genuinely-new boundary against the two cited
Mathlib PRs. This is the first of the six reusable roadmaps (#279–#284)
split out of the original monolithic six-sphere draft; all
construction-specific material (the Δ(3,4,∞) matrices, period functions,
fillings, twist data) has been removed to the downstream project, with
sibling ownership boundaries against GeometricTopology, UniversalCovers,
ConformalMapping, and the Heegaard Floer roadmap stated in the README.

1. The round-3 gluing fix is correct

Round 3 asked that the public gluing input require both canonical overlap
inclusions to be compatible with the piece atlases, rather than accepting
smoothness of D.t i j between independently chosen overlap atlases. The
head now requires

(_left  : ∀ i j, IsLocalDiffeomorph I I ∞ (D.f i j))
(_right : ∀ i j, IsLocalDiffeomorph I I ∞ (fun x : D.V (i, j) ↦ D.f j i (D.t i j x)))

which is the second of the two forms round 3 offered: both canonical maps
from D.V (i, j) into the adjacent pieces, with the second hypothesis
carrying the transition equation. Openness is automatic from
TopCat.GlueData's f_open field (Mathlib Topology/Gluing.lean:91), so
IsLocalDiffeomorph on these maps is the full requested condition, and the
signature now says the same thing as the README's "Encoding conventions"
bullet and Milestone 5.1. This closes the last blocking item.

2. Scope check against the six-sphere consumer

Having read the source construction (alpo.ge/s6.pdf) and the current state
of the downstream formalisation (deancureton/sphere-six-complex, whose
trust boundary is an explicit axiom allowlist), I checked this roadmap's
deliverables against the general-purpose infrastructure that construction
needs. Within #279's stated boundary I found no gap:

• Quotients and descent (Milestone 4). The construction's deck
  quotients are additive (ℤ² at the cusp filling) and finite cyclic (at
  the multiple fibres); Milestone 4's generic group quotients with
  additive versions, holomorphic descent, and the
  compact-fundamental-domain theorem (4.4) supply the right substrate.
  The logarithmic-transform machinery itself is correctly not here — it
  is #280's scope — consuming the quotient/descent layer built in this
  roadmap.
• Finite open gluing with topology criteria (Milestones 5–6). The
  construction glues four pieces along collars over punctured discs; the
  glued-atlas theorem, the generated-relation Hausdorff criterion,
  properness local on the target, and proper-to-compact-target ⇒ compact
  domain cover its assembly step.
• Multiple-fibre torsion (Milestone 7.6). The character-to-Picard
  order statement — divisibility in general, exact order under
  injectivity, with the connected-compact-cover sufficient criterion — is
  the statement shape the construction's
  ord(O(S_j)|_{S_j}) = m_j computation requires. The hypothesis
  discipline added in round 2 is the right one.
• Normal and canonical bundles (Milestones 7.4–7.5). The
  codimension-one complex submanifold quotient model and the canonical
  bundle, with pullback/tensor/determinant from 7.2, are what the
  construction's canonical-bundle computation consumes.

So within its stated boundary the roadmap is adequate for its motivating
consumer: the boundary drawn in the split is not just clean in the
abstract.

Beyond #279's boundary (informational, non-blocking)

Extending the same check across the #279–#284 family, measured against the
downstream project's axiom allowlist (the precise ledger of what the
family has not yet absorbed):

• Assigned but not merge-ready: the source's modular layer —
  j-uniformisation of the orbifold base, the lifting/rigidity arguments,
  and the modular-form weight computation identifying the period torsor
  sheaf — falls to #282 plus the ModularForms roadmap. Round 3 left #282
  short of merge ("make cusp data primitive and resolve degree/Riemann–Hurwitz ownership"), and the
  downstream project currently axiomatises exactly these inputs
  (establishedExactNormalizedModularJUniformization etc.). Whether
  #282's milestones cover the specific lifting-criterion and
  weight-bookkeeping needs has not yet been audited against the source;
  that audit should accompany #282's next round.
• Assigned but scope-mismatched: the toric filling. #281 restricts
  itself to finite regular fans and lists infinite fans as explicitly
  out of scope, while the construction's cusp model is the analytic
  realization of the infinite locally finite fan over the
  A₂-triangulation — exactly what the downstream project axiomatises
  (the StandardInfiniteA2ToricModel block). A completed #281 supplies
  the chart-level inputs (its Layers 1–2, plus #279's gluing); but since
  the family's ownership split assigns toric geometry to #281 alone, the
  infinite locally-finite assembly —
  Hausdorffness and second countability from local finiteness rather
  than finiteness — has no owner as scoped. It should be settled
  deliberately: either a scope extension of #281's gluing layer or an
  explicit deliverable of the construction project. (Round 3 separately
  asked for #281's lattice foundation to be repaired before further
  review.)
• Unowned: the sheaf-cohomology vanishings on ℙ¹ that the period
  construction consumes (establishedProjectiveLineCechNegOne/Zero in
  the downstream allowlist) belong to no roadmap in the family — see §5.
• Deferred by explicit choice: the smooth recognition chain
  (topological Poincaré + smooth-structure classification in dimension
  six) stays axiomatised downstream pending #284, as already agreed in
  discussion.

None of this blocks #279; it is recorded so that "the family covers the
verification" is a checkable claim with named owners rather than an
impression.

3. Minor item (non-blocking)

Milestone 6 numbering glitch. Item "6. As a regression test, glue two
copies of ℂ along ℂˣ …" appears after the Bourbaki source-spine
paragraph, so it renders as a detached one-item list. Move it up into the
numbered list before the sources paragraph (or give it its own sub-heading)
so the milestone's completion criterion is unambiguous.

4. On the open question about Mathlib's quotient work

Paul asked whether the quotient-manifold material should be dropped until
mathlib4#40727 lands. I'd keep it as written:
Mathlib/Geometry/Manifold/Instances/Quotient.lean already exists at
current Mathlib master (checked 2026-08-26), the README's
mirror-then-delete policy names the exact declarations mirrored and
commits to deleting them on a dependency update, and the genuinely-new
scope here (local biholomorphy + holomorphic descent) does not duplicate
the Mathlib PR. That division is right and does not need to wait.

5. Forward-looking suggestion (non-blocking): a Dolbeault / analytic sheaf cohomology sibling

No roadmap in the #279–#284 family defines Dolbeault cohomology or any
analytic sheaf cohomology (#279 correctly disclaims coherent sheaf
cohomology). A seventh sibling of comparable foundational nature would
contain: (p,q)-forms and the ∂̄-operator induced by a complex atlas;
Dolbeault cohomology; the Dolbeault–Grothendieck lemma; the comparison
with sheaf cohomology (Tau Ceti already has sheaf-cohomology
Mayer–Vietoris); and, concretely, the cohomology of line bundles on the
Riemann sphere constructed in Milestone 3 here. Two motivations from the
downstream consumer: (a) it would discharge the unowned ℙ¹-cohomology
axioms identified in §2; (b) the current verification target is only the
existence statement (a complex atlas compatible with the standard smooth
S⁶) — the source paper's analytic invariants (h^{0,q}, the canonical
bundle class, algebraic dimension), i.e. the part that actually collides
with [CDP20], cannot even be stated without analytic cohomology
infrastructure of this kind, whatever further machinery their
verification then needs. Deliberately
out of scope for #279 itself; recording it here so the gap is a decision
rather than an accident.