Research proof index

The quadratic twist becomes isomorphic to E after base change to L. (Over a field, isomorphisms of Weierstrass curves are exactly the admissible changes of variables WeierstrassCurve.VariableChange, acting via •.) The point-level consequences of this isomorphism, which is what most applications need, are recorded separately in `quadraticTwistPoint...

The twist by a unit discriminant keeps multiplicative reduction. If E has multiplicative reduction and D = t² - 4n is a unit of R (residue ≠ 0), then the base change of the R-model twist (E.integralModel R).quadraticTwistOf t n again has multiplicative reduction: its c₄ = D² · c₄ is a unit (so the model is minimal and the reduction multi...

Packaging nodePoly_quadraticTwistOf_map_splits_of_residue: if the base change of the twisted integral model has multiplicative reduction and the residues of (t', n') satisfy the trace and norm relations, then the reduction is split multiplicative.

The integral model of the base change is the base change of the integral model. Both sides are lifts of E.baseChange l along the injective map 𝒪[l] → l (injectivity from IsFractionRing), and lifts along an injective map are unique: compare coefficientwise via integralModel_a₁_eq on both sides and the commuting square algebraMap_integerMap. (O...

If the root of the reduced node polynomial P̄ (assumed irreducible) satisfies a monic quadratic relation X² - t·X + n over the residue field, then comparing with the defining relation of P̄ (aeval_root_nodePoly_map) and using the linear independence of 1 and the root (AdjoinRoot.eq_zero_of_mul_root_add_eq_zero) yields the relations `φc₄·t + φ(...

Twisting flips the square class (residue characteristic ≠ 2). Combining the split criterion nodePoly_map_splits_iff_isSquare with the coefficient scaling of the quadratic twist (c₄_quadraticTwistOf, c₆_quadraticTwistOf), the node polynomial of W.quadraticTwistOf t n splits over a field k of characteristic ≠ 2 exactly when D · (-c₄ c₆) is...