The first step of the end game is to run NCProcess2 on the last spreadsheet which was produced in §17.3. The aim of this run of NCProcess2 is to shrink the spreadsheet as aggressively as possible without destroying important information. The spreadsheet produced by NCProcess2 is the same as the last spreadsheet which was produced 4in §17.3.
Note that it is necessary that all of the equations
in the spreadsheet have solutions,
since they are implied by the original equations.
The equations involving only knowns play a key role.
In particular, they say precisely that, there must exist
a projection
such that
The converse is also true and can be verified with the assistance
of the above spreadsheet.
To do this, we assume that
the matrices
,
,
and
are given
and that (17.4) holds, and wish
to define
,
,
,
,
,
,
,
,
and
such that each of the
equations in the above spreadsheet hold. If we can do this,
then each of the equations from the starting polynomial equations
given in §17.2 will hold
and we will have shown that
a minimal factorization of
the
system exists.
With the assignments made above, every equation in the spreadsheet
above holds.
Thus, by backsolving through the spreadsheet,
we have constructed the factors of the
original system
.
This proves
Theorem ([BGKvD])
The system
can be factored if and only if there exists a projection
such that
and
.
Note that the known equations can be neatly expressed in terms of
and
.
Indeed, it is easy to check with a little algebra that these are
equivalent to
(17.1). It is a question of taste, not algebra,
as to which form one chooses.
For a more complicated example of an end game, see §20.4.