Kummer-class independence for common cover primes

When a prime divides both cover exponents, the successive norm-degree argument used for coprime covers loses exactly the common-prime information. This module begins the required replacement by treating the exceptional prime 2 directly. In the quadratic presentation of the degree-one trace curve, it proves that the product of the two torus coordinates remains nonsquare.

The odd common-prime classes and the roots-of-unity eigencharacter descent are deliberately not assumed here; they remain the next noncoprime wall.

theorem BGS.Markoff.splitTraceCoordinateProduct_quadraticPresentation_not_isSquare {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) (hnondegenerate : sigma ≠ 1) (h2 : 2 ≠ 0) : ¬IsSquare ((algebraMap (RatFunc K) (AdjoinRoot (adjoinSquarePolynomial (splitTraceRadicand sigma)))) (RatFunc.X * splitTraceRadicand sigma))

The sole two-primary residue class left invisible by the four boundary valuations is nevertheless nontrivial: on the degree-one trace curve, the product of the two torus coordinates is not a square.