An evaluation image proves irreducibility where the substitution cannot reach (#746)

[Rafael-SOWNet]

MathS.Polynomials.Factor in several variables is Kronecker's substitution, whose one-variable
image has degree Π (d_i + 1) - 1 — a product. That leaves the one-variable factoriser's
reach after very few variables: x2 + y2 + z2 + w2 + 1 needs an image of degree 80 against a
ceiling of 32, and the answer was null.

	before	now
Factor("x2 + y2 + z2 + w2 + 1", "x")	null	w ^ 2 + x ^ 2 + y ^ 2 + z ^ 2 + 1
Factor("x2 + y2 + z2 + 1", "x")	x ^ 2 + y ^ 2 + z ^ 2 + 1	unchanged
Factor("x7 - y7", "x")	null	null — it is reducible; this says nothing about it
Factor("(x + y) * (x - y)", "x")	(x + y) * (x - y)	unchanged
Factor("y * (x + 1)", "x")	y * (x + 1)	unchanged

Measured on a build of each side.

Why an evaluation image settles anything

Evaluating is a ring homomorphism, so f = g·h gives f(x, a) = g(x, a)·h(x, a). Degrees in
the main variable add, so if the image kept the total degree then neither part can have lost
any. An image that is irreducible and of full degree is therefore a proof that its source is
irreducible — and since #1059, "it does not factor" is an answer rather than a refusal.

An evaluation image has degree d_main however many other variables there are, which is exactly
why it reaches where the substitution does not.

What it does not claim, and how that is held down

One direction only. A reducible image says nothing at all — x2 + y is irreducible and its
image at y = -4 is (x-2)(x+2) — so several points are tried and a decline is never a claim
of reducibility.

The true half is the one nothing downstream can check: a factorisation is verified by
division, and "there is no factorisation" is not. So the tests are mostly about the half that
must never be wrong — 17 of the 23 assert that a certificate is not issued, and every case
in them is written as a product, or is a difference of like powers, so it is reducible by
construction whatever a factoriser would say about it.

The count in the positive test is what stops all of that passing vacuously: a certificate that
always declined would satisfy every AssertFalse in the file. The two halves hold each other up,
and the test remark says so.

The content precondition is checked, not assumed. A factor free of the main variable is
invisible to an image in that variable, so y · (x + 1) would be certified on an image of
2x + 2 whose primitive part is x + 1. The content in the main variable is computed and
anything but a constant declines.

Where this sits

Asked second, after the substitution refuses — the substitution is the one that can actually
factor, and this only ever says there is nothing to find.

It is the first step of Hensel lifting with an evaluation homomorphism — choosing a point
whose image keeps the degree — used for the one conclusion that needs no lifting. Lifting a
reducible image back to a factorisation of its source is the rest of that algorithm, is
unchanged here, and remains the outstanding piece of #746 tier 1.

🤖 Generated with Claude Code

https://claude.ai/code/session_01Bjumi5K7fg8yx6UK1mZTQd