feat(ModularCurves): producer merge — integral Drinfeld Γ₁(N) functor sorry-free (★★) + Γ_H quotient engine + Hopf–Galois chart inputs

[CBirkbeck]

Whole-branch producer merge per the v10.172 cadence (dev/modular-curves, verification pinned at fd1a8ec).

Headline (axiom-clean {propext, Classical.choice, Quot.sound}, per-module attested by stream workers)

• ★★ STREAM-KM: gammaOneDrinfeldProblem — the integral Drinfeld [Γ₁(N)] moduli functor, sorry-free (no invertibility of N): exact-order transport hasExactOrder_pullSection, the T-E4a transport chain de-sorried, the KM 5.3.4 binomial core CharP.p_eq_zero_of_pow_mem_span, isGammaOne_pullAlong, torsionIdeal_baseChange + sectionsDivisor_baseChange.
• ★ STREAM-GH: base change commutes with the free quotient — exists_quotient_baseChange_of_free (KM 7.1.3(3c), full ∃!) on the GHB5a engine; GHC1 (corrected T-H4) and GHC3 (Loeffler Fact 3.8.1) as theorems; RelRepData.pullback/comparisonIso layers.
• STREAM-G0: Hopf–Galois per-chart inputs (GroupScheme/StableChartData.lean), incl. the general surjective_hom_of_isClosedImmersion_specMap (ForMathlib-worthy) and Module.Finite baseRing groupRing.
• QuotientLift morphism descent + PullSectionCanonicity transport layers.

WIP markers

main tolerates sorry as explicit WIP markers (CLAUDE.md); this branch carries the producers' current frontier sorries (e.g. chartPrecursorSpec_isClosedImmersion, the DrinfeldRegularity W2 leaf). The cleanup fleet only ever touches sorry-free declarations.

Verification / merge gate

No PR CI on this repo — a coordinator clean-room build (lake build ModularCurves in a detached worktree at fd1a8ec) is running. Hold merge until the green result is commented here.

🤖 Generated with Claude Code

[CBirkbeck]

Verification: was RED, now GREEN — ready for merge-go

At open, this branch had a 2-red cascade at committed state (not sibling WIP — both files were clean in git status), caught by a clean-room full-library build at the actual branch tip:

1. ForMathlib/QuotientLift.lean — a redundant duplicate of SchemeAction.epi_pullback_snd_quotientπ (an open-immersion-only copy of the general form now in SchemeQuotient.lean) + a stale free-action hypothesis order. Fixed in e6a04fe8d (dedup + realign; +8/−21).
2. Moduli/EngineDescent.lean — latent behind cleanup: golf padicLog_mul_of_norm_lt_one #1 (it imports QuotientLift, so lake skipped it until cleanup: golf padicLog_mul_of_norm_lt_one #1 built). Two call sites fed the old-order free-action hypothesis to the now-canonical-order consumers. Fixed in 61696bb83 (boundary adapters; +6/−2).

Root cause: STREAM-GH's GHB5a work changed the free-action hypothesis order to ∀ {T} (t) (g), g ≠ 1 → … in the SchemeQuotient/AffineQuotient layer; two older consumers weren't realigned. Both repairs are statement-preserving — no signature of any consumed result changed, no sorry added.

Clean-room result at 61696bb83: Build completed successfully (3798 jobs), real exit 0, zero errors. The only commit since (2cadc8134) is board/inbox markdown — no .lean change — so the current tip is green.

The remaining WIP sorrys on the branch are the producers' explicit frontier markers (chartPrecursorSpec_isClosedImmersion, the DrinfeldRegularity leaf, the gammaFullDrinfeldProblem rel-rep target); main tolerates these per CLAUDE.md, and the cleanup fleet only touches sorry-free declarations.

Held for your merge-go (coordinator opens + verifies; owner merges — the #5256 precedent). A follow-up cleanup ticket to unify the free-action hypothesis order project-wide will be filed once these files land on main.