Polynomial certificate for order-seven isogeny doubling

The cleared Vélu abscissa commutes with tangent doubling by a homogeneous polynomial identity of degree 28. We verify the identity at 29 distinct rational values and close it with the degree bound. The pointwise ring certificates live in serially imported shards, keeping the memory required by each Lean process bounded during a cold build.

theorem MazurTorsion.Kubert.OrderSevenDoublingCertificate.polynomial_identity (d : ℚ) : veluXHomogeneousPolynomial d (sourceDoubleXPolynomial d) (sourceCompletedCubicPolynomial d) = doubleXHomogeneousPolynomial (orderSevenQuotient d) (veluXPolynomial d) (kernelPolynomial d ^ 2)

The degree-28 homogeneous abscissa certificate for doubling through the explicit order-seven Vélu map.