The odd-degree numeric parabolic cohomology bound at level three

Proved

MTT.Cohomology.parabolicH1_finrank_le_level_three_numeric

by cbirkbeck · Sep 8, 2026 · Mathlib 0df444a (Lean v4.33.1)

cohomologynumber-theory

Let $n>0$ be odd. For the MTT binary-form action, the parabolic cohomology of $\Gamma_1(3)$ satisfies

\dim_{\mathbf C}H^1_{\mathrm{par}}(\Gamma_1(3),\operatorname{Sym}^n\mathbf C^2)\le 2\left(\left\lfloor\frac{n+2}{3}\right\rfloor-1\right).

This is the cohomological estimate for the remaining level-three odd-weight MTT comparison. It retains the contribution of the order-three elliptic generator; no torsion-free small-level assumption is made.

Preamble

import Definitions.Def_MTT_ParabolicCohomology
import Mathlib.LinearAlgebra.FiniteDimensional.Defs

Formal statement

theorem MTT.Cohomology.parabolicH1_finrank_le_level_three_numeric {n : ℕ}
    (hn : 0 < n) (hno : Odd n) :
    Module.finrank ℂ (MTT.Cohomology.ParabolicH1 3 n) ≤ 2 * ((n + 2) / 3 - 1) := by sorry

Source

Derived generator-and-cyclic-norm estimate for MTT frontier 03513b57-2878-4a4a-8605-3db4bbbcae31. Inputs: proved Gamma0(3) generator theorem ee2e87fa-6ddf-5fb1-b8a6-43ad24a595b2 and normalization kernel theorem 3352ccf6-5b8e-4aca-90ec-e016d14106d8. The explicit elliptic matrix is [[-2,1],[-3,1]], conjugate to -ST; averaging and its symmetric-power trace give the displayed count.

View graph