Naive height contraction in elliptic halving descent (source code)

= Naive height contraction in elliptic halving descent
{title2=$P=2Q+R\Longrightarrow h_x(Q)\leq\tfrac12h_x(P)+C_R$}

For a fixed rational point $R$ on an <elliptic curve> over a <number field>, the addition formula gives $h_x(P-R)\leq2h_x(P)+O_R(1)$. The duplication map has degree four, so $h_x(2Q)=4h_x(Q)+O(1)$. Combining them gives the displayed contraction. A finite set of representatives modulo twice the point group makes the constants uniform. Points above a fixed height threshold descend by a definite amount; <Northcott theorem> makes the terminal bounded-height set finite. This converts the <Weak Mordell-Weil theorem> into the full finite-generation theorem.