Challenge: the five-coset bound on X_1(11) #
This is the remaining arithmetic input to the compiled order-eleven reduction. The downstream file already proves that this proposition classifies every rational point on the selected genus-one model.
Every rational point on the selected X_1(11) model differs from one
of the five visible torsion points by five times another rational point.