feat: roadmap for Fuchsian groups and orbifold Riemann surfaces

[Paul-Lez]

• Develop the effective projective action, Fuchsian groups, polygon presentations, and covolume.
• Construct elliptic quotient charts, choice-independent cusp compactifications, and finite-index maps.

Sources: Beardon, Katok, and Farkas–Kra.

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 #282 — Fuchsian groups and orbifold Riemann surfaces.

Head reviewed: 589f06749b9f9ab40e4a50d737f35336da4194e4

Verdict

Changes requested.

This is much closer than the original construction-specific layer. It has the correct broad scope, uses the effective projective action, distinguishes free and elliptic quotient points, and puts compactification before the j-line identification. I found no false main theorem, but several definitions and ownership boundaries are still too loose.

1. Cusp width is not intrinsic without a normalization

Let σ take a cusp to infinity and write its positive stabilizer generator as

[
z\longmapsto z+w.
]

Replacing σ by

[
z\longmapsto a,σ(z)+b,\qquad a>0,
]

changes the width to (aw), while

[
q'(z)
=\exp!\left(\frac{2\pi i(aσ(z)+b)}{aw}\right)
=\exp!\left(\frac{2\pi i b}{aw}\right)q(z).
]

Thus an arbitrary cusp does not have a canonical positive real width. The coordinate germ is well defined only up to multiplication by a nonzero constant unless a scaling normalization has been chosen.

Replace “a cusp has a unique positive width” by a choice-dependent cusp datum containing a normalized conjugation and positive generator. Then prove:

• the exact change law under another normalized representative;
• independence of the compactified complex structure;
• the width-ratio and ramification formula under finite-index subgroup inclusions.

For arithmetic subgroups one can later add canonical normalizations relative to a fixed rational boundary coordinate.

2. Consume Mathlib's invariant upper-half-plane measure

At the exact Mathlib pin, UpperHalfPlane.Measure.lean already defines the measure

[
dx,dy/y^2,
]

proves local finiteness, and proves invariance under the GL₂(ℝ) action.

Layer 2 should consume this measure. It may still own:

• the comparison with hyperbolic Riemannian volume;
• measurable fundamental domains;
• covolume;
• independence of the chosen fundamental domain;
• Gauss–Bonnet and quotient-area formulas.

It should not reconstruct a second measure.

3. Resolve ownership of degree and Riemann–Hurwitz

Layer 5 develops generic local multiplicity, degree of maps of compact Riemann surfaces, divisor pullback, and Riemann–Hurwitz. Existing roadmaps already assign the compact-Riemann-surface Riemann–Hurwitz API to the modular-forms development, and the Belyi roadmap waits for that supplier.

Choose one owner:

• move the generic degree/Riemann–Hurwitz theory here and update ModularForms and Belyi to consume it; or
• consume the exact shared declarations here and keep only the Fuchsian quotient applications.

Do not merge two generic theorem families with slightly different carriers or signs.

4. “Orbifold fundamental group” needs an actual object

The scope and completion criterion mention orbifold fundamental groups, but the layers construct group presentations from polygons without selecting a public orbifold groupoid or orbifold fundamental-group carrier.

Either:

• define a reusable orbifold fundamental group/groupoid and compare it with the Fuchsian group; or
• say explicitly that this roadmap proves the standard polygon presentation of Γ and does not introduce a general orbifold fundamental group.

The current terminology is ambiguous.

5. Finite-index functoriality needs the local formulas

The compactification is said to be functorial for finite-index subgroup inclusions. State and prove:

• the extension of the quotient map to cusp points;
• ramification index at a cusp as the ratio of compatible cusp widths;
• ramification at elliptic points from stabilizer indices;
• multiplicativity in subgroup towers;
• the degree formula.

These are needed by modular curves and Belyi maps and are more useful than a bare functoriality assertion.

6. Type the triangle-group parameter ∞

The roadmap asks for one theorem family covering (p,q,∞). The public type must distinguish a cusp from a finite elliptic order, for example with WithTop ℕ, Option ℕ, or a dedicated finite-or-cusp type. The hyperbolic inequality and presentation must be written in that type.

Do not leave infinity as notation with no carrier.

7. Pin the hypotheses of the polygon theorems

The Poincaré polygon theorem and its converse require exact hypotheses on:

• geodesic finite-sidedness;
• side-pairing transformations;
• cycle transformations and angle sums;
• local finiteness/no-overlap;
• ideal vertices;
• non-elementarity and finite area in the converse;
• the choice of centre for a Dirichlet domain.

List these as separate milestones. “Prove the polygon theorem” is not yet unambiguous enough for an agent.

8. Strengthen the projective-action interface

Suggested.lean defines a monoid homomorphism into permutations and proves injectivity and MDiff. It does not seed:

• the topology and topological-group structure on PSL₂(ℝ);
• continuity of the action jointly in group and point;
• compatibility with Mathlib's SL₂ action;
• the discrete-subgroup-to-properly-discontinuous theorem;
• the coarse quotient or cusp compactification.

Add representative declarations for those interfaces.

9. Expand Suggested.lean beyond formulas

The current file checks the formula for q and z^m, but not the main new objects. Add signatures for:

• a Fuchsian subgroup input;
• the effective action;
• the free-locus quotient;
• the elliptic quotient chart;
• cusp data and its change law;
• the compactified carrier and atlas;
• extension of invariant meromorphic functions;
• the shared degree map;
• the level-one j biholomorphism.

What should remain

• effective PSL₂ rather than an SL₂ action with central kernel;
• covering only on the free locus;
• local cyclic quotient charts at elliptic points;
• construction of the compact Riemann surface before identifying it with P¹;
• a generic (p,q,∞) theorem rather than hard-coded (3,4,∞);
• explicit meridian conventions and q-expansion order formulas;
• the reusable rather than six-sphere-specific scope.

Recommended disposition

One revision should be enough if the cusp datum, existing measure, generic degree ownership, finite-index formulas, and representative signatures are fixed.

---

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 aff6d0e. Cusp width is now choice-dependent normalized data with the exact scaling and q-coordinate change laws; the compactified atlas is proved independent of that choice. The roadmap consumes Mathlib’s invariant upper-half-plane measure and the modular-forms compact-surface degree/Riemann–Hurwitz supplier, defines only polygon presentations rather than a generic orbifold fundamental group, adds all finite-index cusp and elliptic ramification formulas, types finite-versus-cusp triangle parameters, and lists the full polygon hypotheses. Suggested.lean now seeds the effective PSL action, free locus, cusp data, typed triangle parameters, and compactification carrier. The PR body now foregrounds the standard Fuchsian sources.

[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 #282 — Fuchsian groups and orbifold Riemann surfaces.

Head reviewed: aff6d0ea546f1f9fa246f97bdd4e4069f988baa2

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 update correctly handles:

• choice-dependent cusp widths and their coordinate-change law;
• use of Mathlib's existing invariant measure;
• typed finite/cusp triangle parameters;
• explicit Poincaré-polygon hypotheses;
• finite-index cusp and ramification behavior;
• the scope wall excluding a general orbifold-groupoid carrier;
• a much more representative compactification carrier in Suggested.lean.

Two issues remain.

1. CuspDatum does not say that the chosen element generates the full cusp stabilizer

The current structure stores a scaling, an element called positiveGenerator, a positive width, and a conjugation formula. It does not store:

• the cusp or its orbit;
• proof that the scaling sends that cusp to infinity;
• proof that the chosen element generates the full stabilizer of that cusp.

This matters. Suppose the primitive cusp stabilizer is generated by

$$ z\mapsto z+1. $$

The present structure also accepts the element z ↦ z+2 with width 2. Its coordinate

$$ q=e^{\pi i z} $$

is invariant under translation by 2, but not under the actual stabilizer generator z ↦ z+1. It therefore does not descend to the quotient cusp, and it is not a cusp chart.

The structure needs an actual cusp representative and a theorem/field saying that the conjugated stabilizer is exactly wℤ, with the selected generator corresponding to +w.

2. The claimed degree/Riemann–Hurwitz supplier does not currently exist

The README now names an exact module and declarations:

TauCeti.Analysis.Complex.RiemannSurface.Degree
RiemannSurface.localMultiplicity
RiemannSurface.degree
...
RiemannSurface.riemannHurwitz

and assigns them to the merged ModularForms roadmap. Those names and that module do not currently appear in the repository or in the merged ModularForms roadmap.

A prose contract with a supplier which has not actually promised or seeded those declarations is not a dependency.

Choose one of these routes:

1. amend the ModularForms roadmap in a companion PR so it genuinely owns and seeds the exact module;
2. make this Fuchsian roadmap the owner of the generic compact-Riemann-surface degree API; or
3. split that API into a dedicated compact-Riemann-surfaces roadmap consumed by both.

The existing ModularForms roadmap also says it constructs the analytic modular quotient and compactification itself. That should be revised to consume this Fuchsian roadmap, otherwise the two roadmaps still overlap substantially.

3. The compactified carrier should expose its construction

CompactifiedQuotient Γ := by sorry is still an opaque arbitrary Type. Since the roadmap insists that the carrier is built from the coarse quotient plus cusp orbits, the representative signature should expose that sum/quotient construction or a specific gluing carrier. Otherwise the most important non-circularity condition remains only prose.

Verdict

Changes requested. The local mathematics is much better; the main remaining work is to make cusp normalization primitive and to resolve the real ownership of compact-Riemann-surface degree theory.

---

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 6a1fe5f, with the existing ModularForms overlap removed in companion #288. Cusp data now store the cusp representative, scaling to infinity, and a generator of the full stabilizer; the compactification carrier visibly adjoins cusp orbits to the coarse quotient; and this roadmap now owns and seeds the generic compact-surface genus, degree, divisor-pullback, degree-one, and Riemann--Hurwitz APIs.

[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 #282 — Fuchsian groups and orbifold Riemann surfaces.

Head reviewed: 6a1fe5fd7955e8e61efa225d8c9ccf311dec0156

What has been fixed

The previous issues are repaired:

• cusp data now store a cusp representative, a scaling to infinity, and a generator whose powers are exactly the full stabilizer;
• a proper power of the primitive parabolic is rejected;
• the compactified carrier is visibly the disjoint sum of the coarse quotient and cusp orbits;
• the generic compact-surface degree API is now owned here rather than attributed to a nonexistent supplier;
• ModularForms has been revised to consume this quotient rather than build a competing carrier.

Remaining issue: genus and Riemann–Hurwitz still need a non-circular proof spine

Layer 5 currently says:

1. define analytic genus;
2. define local multiplicity and degree;
3. derive Riemann–Hurwitz from the canonical-divisor pullback formula.

At the same time, the ownership section assigns analytic Riemann–Roch, cohomology and automorphy sheaves to ModularForms, while ModularForms consumes the genus and Riemann–Hurwitz API from this roadmap.

That is safe only if the lower construction is made explicit and does not use the later ModularForms Riemann–Roch layer. At present Suggested.lean contains an opaque

noncomputable def genus ... : ℕ := by sorry

followed by riemannHurwitz, so the dependency is not pinned.

A robust correction would be one of:

• define genus topologically by
  $\chi(X)=2-2g$, consuming AlgebraicTopology's finite-CW Euler characteristic, and prove analytic/topological compatibility;
• prove Riemann–Hurwitz by a topological branched-cover/Euler-characteristic argument;
• put compact-surface genus, canonical-divisor degree and Riemann–Hurwitz in a small independent RiemannSurface.Degree supplier which neither imports ModularForms nor depends on its Riemann–Roch layer.

The present prose may be implementable, but it does not yet rule out a circular implementation.

Verdict

Changes requested. The Fuchsian quotient and cusp architecture are now good; the generic genus/Riemann–Hurwitz foundation needs one explicit acyclic route.

---

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.

[Paul-Lez]

🤖 Addressed in 4f13956. RiemannSurface.Degree now gets genus from the AlgebraicTopology finite-CW Euler characteristic, proves the branched-cover Euler-characteristic formula by excision and covering multiplicativity, and derives Riemann–Hurwitz by rewriting. It imports no ModularForms or analytic Riemann–Roch module. The coordinated acyclic Degree / LevelOne.JInputs import graph is pinned with #288. Focused Lean check: lake env lean TauCetiRoadmap/FuchsianOrbifolds/Suggested.lean.