Euler's line: the circumcentre, the centroid and the orthocentre of a non-degenerate triangle are collinear

The certificate uses the Rabinowitsch trick: a fresh variable Zinv0 and the generator `collinear(A,B,C) * Zinv0 - 1`. Specialising Zinv0 := 1/collinear(A,B,C) is legitimate exactly when A, B, C are not collinear, and that is the ONLY place the side condition enters. Because the multiplier this route divides out is the SQUARE of the condition polynomial, the saturation cofactor is not the familiar minus-the-conclusion of the other saturated certificates but exactly -conclusion*(1 + collinear(A,B,C)*Zinv0) -- the N = 2 case of 1 = z^N d^N - g * sum_{i=1..N} C(N,i) g^{i-1}, asserted term for term by `the_squared_multiplier_produces_the_expected_rabinowitsch_cofactor`. Four tamper controls in the cited suite bear on this fact and every one runs against EVERY saturated certificate: deleting the degenerate counterexample is rejected; replacing it with a generic configuration is rejected; replacing it with A = B = (0,0), C = (1,0), O = (1/2,0), H = (0,0) -- which genuinely violates `abc-not-collinear` and yet leaves O, G, H collinear -- is also rejected; and an unused saturation is rejected.

The distinction ADR-0455 draws matters here more than on the six older facts, because the route that reached this theorem CANNOT establish minimality the way `geometry_order_audit` does for those: the multiplier a linear elimination divides out is an artifact of the decomposition it chose, so the route could in principle consume a condition the theorem does not need. It does not, and the proof is the counterexample rather than a search. The only proper subset of a one-element condition set is the empty one, and A = B = (0,0), C = (1,0), O = (1/2,0), H = (0,1) satisfies all four hypotheses while falsifying the conclusion -- so the conclusion is not in the plain hypothesis ideal, decided, with no budget, no monomial order and no algorithm anywhere in the argument. No larger budget, faster order or better algorithm can report this theorem as unconditional.

This control was written while the theorem was on the FRONTIER -- to keep it unproved rather than unchecked -- and is kept now that it is proved because it checks something the certificate cannot. The certificate establishes a polynomial identity; nothing inside a polynomial identity can tell you that `equidistant` means equidistant. It also is the diagnosis the linear route acts on, in miniature: the exact construction it performs IS Cramer's rule on the two 2x2 systems, and its determinant is a multiple of the very collinearity polynomial named as the non-degeneracy condition.