Skip to content

fix: align modular forms with the Fuchsian roadmap - #288

Draft
Paul-Lez wants to merge 7 commits into
TauCetiProject:mainfrom
Paul-Lez:codex/modular-forms-fuchsian-alignment
Draft

fix: align modular forms with the Fuchsian roadmap#288
Paul-Lez wants to merge 7 commits into
TauCetiProject:mainfrom
Paul-Lez:codex/modular-forms-fuchsian-alignment

Conversation

@Paul-Lez

Copy link
Copy Markdown

🤖 Companion to #282.

  • Makes ModularForms consume the Fuchsian quotient, cusp compactification, and generic degree and Riemann--Hurwitz APIs.
  • Keeps congruence arithmetic, analytic Riemann--Roch, automorphy sheaves, and dimension formulas in ModularForms.

@CBirkbeck CBirkbeck left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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 #288 — ModularForms companion revision.

Head reviewed: 125fb08030a324b62f3c448483f5f76a1b038bf6

What is good

The companion revision now says the right things:

  • FuchsianOrbifolds owns the analytic quotient and compactification;
  • ModularForms owns congruence-subgroup arithmetic, automorphy sheaves, analytic Riemann–Roch and dimension formulas;
  • no second quotient carrier is introduced in ModularForms.

Remaining issue: the dependency graph is still cyclic at roadmap level

FuchsianOrbifolds Layer 6 consumes from ModularForms:

  • the normalized level-one j;
  • modular invariance;
  • the q-expansion;
  • exact elliptic orders.

ModularForms Layer 10 consumes from FuchsianOrbifolds:

  • the compactified quotient;
  • genus;
  • local multiplicity and degree;
  • Riemann–Hurwitz.

This can be implemented acyclically, but the roadmaps do not yet specify the module split. Suggested.lean for ModularForms still imports only Mathlib and does not #check the Fuchsian contracts.

Pin the dependency as something like

ModularForms/LevelOne/JInputs
        ↓
FuchsianOrbifolds/LevelOne
        ↓
FuchsianOrbifolds/RiemannSurface/Degree
        ↓
ModularForms/DimensionFormula

or move the level-one j application into a separate consumer module. The essential condition is that no single ModularForms module imports Fuchsian while being imported by the Fuchsian module it consumes.

After #282 lands, add literal imports and #checks for the exact contracts in the higher ModularForms module.

Verdict

Changes requested.


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

Copy link
Copy Markdown
Author

🤖 Addressed in 678e6ea, stacked on the coordinated #282 contract commit 4f13956. The README now pins the literal acyclic split: lower ModularForms.LevelOne.JInputs points to Fuchsian.LevelOne; independent RiemannSurface.Degree points to both Fuchsian applications and the higher ModularForms.DimensionFormula; only that higher module imports the Fuchsian compactification. Suggested.lean now imports the stacked Fuchsian contract file and literally #checks the compactification, finite-map, genus, local-multiplicity, degree, divisor-pullback, degree-one, and Riemann–Hurwitz declarations. Focused verification: lake build TauCetiRoadmap.ModularForms.Suggested completed successfully (8703 jobs). Once #282 merges, its files disappear from this PR diff while these import checks remain.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants