The level-seven modular correspondence polynomial

This file exposes the symmetric bidegree-(7,7) polynomial used by the X₀(49) transfer. Its factorization as the off-diagonal part of the cross-multiplied level-seven j-identity gives the eventual order-49 tower an algebraic interface independent of the private transfer certificates.

Only the checked polynomial interface and its elementary boundary behaviour are recorded here. The quotient family and the identification with the modular correspondence remain separate steps.

def MazurTorsion.Kubert.orderSevenJNumerator (t : ℚ) : ℚ

The numerator in the level-seven Hauptmodul formula j(t) = J₇(t) / t⁷.

Equations

• MazurTorsion.Kubert.orderSevenJNumerator t = (t ^ 2 + 13 * t + 49) * (t ^ 2 + 245 * t + 2401) ^ 3

def MazurTorsion.Kubert.orderSevenG7F (s B : ℚ) : ℚ

The Fricke-twisted level-seven correspondence polynomial.

Equations

• One or more equations did not get rendered due to their size.

theorem MazurTorsion.Kubert.orderSevenG7F_comm (s B : ℚ) : orderSevenG7F s B = orderSevenG7F B s

The level-seven correspondence is symmetric in its two legs.

theorem MazurTorsion.Kubert.orderSevenJNumerator_crossDifference (s B : ℚ) : orderSevenJNumerator s * B ^ 7 - orderSevenJNumerator B * s ^ 7 = (s - B) * orderSevenG7F s B

The cross-multiplied equality of the two level-seven j-values factors as the diagonal times the correspondence polynomial.

theorem MazurTorsion.Kubert.orderSevenG7F_eq_zero_iff_crossMultiply {s B : ℚ} (hsB : s ≠ B) : orderSevenG7F s B = 0 ↔ orderSevenJNumerator s * B ^ 7 = orderSevenJNumerator B * s ^ 7

Off the diagonal, equality of the cross-multiplied level-seven j-values is exactly the correspondence equation.

@[simp]

theorem MazurTorsion.Kubert.orderSevenG7F_zero_left (B : ℚ) : orderSevenG7F 0 B = -678223072849 * B ^ 6

On the left boundary, the correspondence polynomial is a nonzero constant times the sixth power of the other coordinate.

@[simp]

theorem MazurTorsion.Kubert.orderSevenG7F_zero_right (s : ℚ) : orderSevenG7F s 0 = -678223072849 * s ^ 6

On the right boundary, the correspondence polynomial is a nonzero constant times the sixth power of the other coordinate.

theorem MazurTorsion.Kubert.orderSevenG7F_zero_left_iff (B : ℚ) : orderSevenG7F 0 B = 0 ↔ B = 0

The left boundary meets the affine correspondence only at the cusp image.

theorem MazurTorsion.Kubert.orderSevenG7F_zero_right_iff (s : ℚ) : orderSevenG7F s 0 = 0 ↔ s = 0

The right boundary meets the affine correspondence only at the cusp image.