The level-seven modular correspondence has no noncuspidal rational point

The symmetric bidegree-(7,7) polynomial G obtained by removing the diagonal from the level-seven hauptmodul modular equation is a plane model of X₀(49). An explicit rational map, discovered by exact q-expansion fits and verified here purely algebraically, sends every rational solution with s·B ≠ 0 to an affine rational point of the X₀(49) Weierstrass model y² = x(x² + 21x + 112) whose abscissa is nonzero. The complete two-isogeny descent proved that the only rational points of that model are 0 and (0,0), so no such solution exists: the affine curve G = 0 has no rational point outside the singular cusp image (0,0).

theorem MazurTorsion.XZeroFortyNine.no_noncuspidal_correspondence_point {s B : ℚ} (hs : s ≠ 0) (hB : B ≠ 0) (hG : Kubert.orderSevenG7F s B = 0) : False

The affine level-seven modular correspondence has no rational point away from the singular cusp image: G(s,B) = 0 with s·B ≠ 0 is impossible over ℚ.