search: Harrison `sos.ml:1638` fails to close (Pythagorean-style 4 ineq + 2 eq)

Split off from #44.

Repro

example (a b c x y : ℝ) (_hb : 0 ≤ b) (_hc : 0 ≤ c) (_hx : 0 ≤ x)
    (_hy : 0 ≤ y) (_hxc : x^2 = c) (_hy2 : y^2 = a^2 * c + b) :
    0 ≤ y*x - a*c := by sos

Fails with search failed to find a certificate in ~35s at default config.

Why we expected it to work

Five variables, but only four inequality hypotheses and two equality hypotheses in canonical form — the same shape we already handle in :1647, :1650, :1629. Harrison's REAL_SOS closes it.

Likely cause

Plausibly related to #51 (which has the same equality-cofactor flavor) but with a more entangled cofactor structure (y² = a²·c + b mixes three of the five variables). Worth investigating jointly with #51.

Start with the reproducer in the issue and inspect the search logic around sos.ml:1638, comparing it with the working cases at lines 1647, 1650, and 1629. Read the related equality-cofactor issue #51 and the parent issue #44 for context. Done means the supplied example closes successfully without the certificate-search failure.