Main derivation
S01 · definition
Before
p=f\cdot g\ \text{(proposed)}After
p=f\cdot g\iff\text{every coefficient of }p\text{ equals that of the expanded }f\cdot gConditions: none
Rule: mko_factorization · Uses: G1
Leaf basis: mko_factorization + poly_eq_coeff
By the MKO, a proposed factorization is a polynomial identity: after expanding the right side and collecting like terms, the coefficient of every power must equal that of the left side (poly_eq_coeff). So verifying a factorization means comparing coefficients, not substituting a few numbers.
S02 · equivalent
Before
(x+a)(x+b)
After
x^2+(a+b)x+ab
Conditions: a,b\in\mathbb{Q}
Rule: L_binom · Uses: S01
Leaf basis: distributive + mul_comm + like_terms
By Lemma L_binom, the product of two monic degree-one factors has x-coefficient a+b and constant term ab. This is the MKO's binomial-product formula; the proof is S02.1 and S02.2.
S03 · equivalent
Before
3x^2+3x-18
After
3(x^2+x-6)
Conditions: none
Rule: distributive · Uses: G2, distributive
Leaf basis: distributive + poly_eq_coeff + numeric_evaluation
The three coefficients 3, 3 and −18 are all multiples of 3, so take out the common factor 3 by distributivity: 3(x²+x−6)=3x²+3x−18. Check the coefficients: 3·1=3, 3·1=3, 3·(−6)=−18.
S04 · implies
Before
a=3,\ b=-2
After
a+b=3+(-2)=1,\ ab=3\cdot(-2)=-6
Conditions: none
Rule: numeric_evaluation · Uses: S02, S03
Leaf basis: numeric_evaluation
To match x²+x−6 with the form of S02 we need a+b=1 and ab=−6. Try a=3, b=−2: 3+(−2)=1 and 3·(−2)=−6, so both conditions hold. How the pair was found does not matter; what matters is that it passes the expansion check of S05.
S05 · equivalent
Before
(x+3)(x-2)
After
x^2+(3+(-2))x+3\cdot(-2)=x^2+x-6
Conditions: none
Rule: L_binom · Uses: S02, S04
Leaf basis: L_binom + forall_elim + numeric_evaluation
Apply Lemma L_binom with a=3 and b=−2: (x+3)(x−2)=x²+(3+(−2))x+3·(−2)=x²+x−6. The coefficients [−6,1,1] agree one by one with those of x²+x−6.
S06 · equivalent
Before
3x^2+3x-18
After
3(x+3)(x-2)
Conditions: none
Rule: eq_replace · Uses: S03, S05
Leaf basis: eq_replace + poly_eq_coeff + distributive
In 3(x²+x−6) from S03, replace x²+x−6 by (x+3)(x−2) from S05 to get p=3(x+3)(x−2). Overall check: 3(x+3)(x−2)=3(x²+x−6)=3x²+3x−18, with coefficients [−18,3,3] equal to those of p (N6).
S07 · equivalent
Before
(x-d)(x+d)
After
x^2-d^2
Conditions: d\in\mathbb{Q}
Rule: L_diffsq · Uses: S02
Leaf basis: L_binom + numeric_evaluation
By Lemma L_diffsq, the difference of squares x²−d² factors as (x−d)(x+d). The proof, a special case of L_binom, is S07.1.
S08 · equivalent
Before
2x^2-50
After
2(x^2-25)
Conditions: none
Rule: distributive · Uses: G2, distributive
Leaf basis: distributive + numeric_evaluation
The coefficients 2 and −50 are multiples of 2, so take out the common factor 2: 2(x²−25)=2x²−50.
S09 · equivalent
Before
x^2-25
After
(x-5)(x+5)
Conditions: 25=5^2
Rule: L_diffsq · Uses: S07
Leaf basis: L_diffsq + forall_elim + numeric_evaluation
25=5², so x²−25 is a difference of squares, and L_diffsq with d=5 gives (x−5)(x+5).
S10 · equivalent
Before
2x^2-50
After
2(x-5)(x+5)
Conditions: none
Rule: eq_replace · Uses: S08, S09
Leaf basis: eq_replace + poly_eq_coeff + distributive
Replace x²−25 in S08 by (x−5)(x+5) to get q=2(x−5)(x+5). Overall check: expanding gives 2(x²−25)=2x²−50, with coefficients [−50,0,2] equal to those of q (N9); the x-coefficient 0 must match as well.
S11 · implies
Before
x^2+25\ \text{vs.}\ (x-5)(x+5)After
(x-5)(x+5)=x^2-25\neq x^2+25
Conditions: none
Rule: poly_eq_coeff · Uses: G2, S09, poly_eq_coeff
Leaf basis: poly_eq_coeff + numeric_evaluation
By S09, (x−5)(x+5)=x²−25, whose constant coefficient is −25; the constant coefficient of s=x²+25 is 25. Since 25≠−25, they are different polynomials. Applying the difference-of-squares formula to a sum of squares is wrong.
S12 · implies
Before
x^2+25=(ux+v)(wx+t),\ u\neq0,\ w\neq0
After
\text{impossible in}\ \mathbb{Q}[x]Conditions: u\neq 0; w\neq 0
Rule: L_no_linear_factor · Uses: G2, eval_hom, square_nonneg
Leaf basis: L_no_linear_factor + contradiction
By Lemma L_no_linear_factor, x²+25 cannot be written as a product of two degree-one factors in ℚ[x]; this rules out every such factorization, not just the candidate (x−5)(x+5). The proof is S12.1 to S12.3: a degree-one factor would give a rational root, but c²+25 is always positive.
S13 · implies
Before
x^3\ \text{and}\ x\ \text{at}\ x=-1,0,1After
\text{equal values, but}\ x^3\neq x\ \text{in}\ \mathbb{Q}[x]Conditions: none
Rule: poly_eq_coeff · Uses: G2, poly_eq_coeff, eval_hom
Leaf basis: poly_eq_coeff + numeric_evaluation
(−1)³=−1, 0³=0 and 1³=1, so x³ and x agree at these three points; indeed x³−x=(x−1)x(x+1) vanishes exactly there. But the x³-coefficient is 1 for x³ and 0 for x, so they are different polynomials, and at x=2, 8≠2. Both have degree at most 3, so deciding an identity by values would need at least 4 distinct points; agreement at three points does not establish an identity.
S14 · implies
Before
p,\ q,\ s,\ x^3\ \text{vs}\ xAfter
p=3(x+3)(x-2),\ q=2(x-5)(x+5),\ s\neq(x-5)(x+5),\ s\ \text{has no degree-one factor},\ x^3\neq xConditions: none
Rule: and_intro_elim · Uses: S06, S10, S11, S12, S13
Leaf basis: and_intro_elim
Summary: p=3(x+3)(x−2) and q=2(x−5)(x+5) both pass the coefficient-by-coefficient comparison; x²+25 is not (x−5)(x+5) and has no factorization into two degree-one factors; x³ and x agree at three points and are still different polynomials.
Substeps and lemmas
S02.1 · equivalent
Before
(x+a)(x+b)
After
x\cdot x+x\cdot b+a\cdot x+a\cdot b
Conditions: none
Rule: distributive · Uses: distributive
Leaf basis: distributive
Distribute (x+a) over (x+b): (x+a)(x+b)=x(x+b)+a(x+b), then distribute each part to get the four terms x·x, x·b, a·x and a·b.
S02.2 · equivalent
Before
x\cdot x+x\cdot b+a\cdot x+a\cdot b
After
x^2+(a+b)x+ab
Conditions: none
Rule: like_terms · Uses: S02.1, like_terms, mul_comm
Leaf basis: like_terms + mul_comm + add_comm
x·x=x²; by commutativity x·b=bx, which is a like term with ax, and they combine to (a+b)x; the constant term is ab. S02.1 and S02.2 together prove Lemma L_binom.
S07.1 · equivalent
Before
(x+(-d))(x+d)
After
x^2+(-d+d)x+(-d)d=x^2-d^2
Conditions: none
Rule: L_binom · Uses: S02
Leaf basis: L_binom + add_inverse + neg_mul
Take a=−d and b=d in L_binom: the x-coefficient is −d+d=0 and the constant term is (−d)·d=−d², so (x−d)(x+d)=x²−d². This proves Lemma L_diffsq.
S12.1 · implies
Before
x^2+25=(ux+v)(wx+t),\ u\neq 0
After
c=-\tfrac{v}{u}\in\mathbb{Q},\quad c^2+25=(uc+v)(wc+t)=0\cdot(wc+t)=0Conditions: u\neq 0
Rule: eval_hom · Uses: eval_hom, mul_inverse_nonzero
Leaf basis: eval_hom + mul_inverse_nonzero + mul_zero
Suppose such a factorization exists. Since u≠0, c=−v/u is rational and uc+v=−v+v=0. Equal polynomials have equal values at c, and evaluation respects products (eval_hom), so c²+25=(uc+v)(wc+t)=0·(wc+t)=0.
S12.2 · implies
Before
c\in\mathbb{Q}\subseteq\mathbb{R}After
c^2+25\geq 25>0
Conditions: none
Rule: square_nonneg · Uses: S12.1, square_nonneg, order_basics
Leaf basis: square_nonneg + order_basics
c is a real number, so c²≥0 by square_nonneg; adding 25 to both sides gives c²+25≥25>0, so c²+25≠0.
S12.3 · implies
Before
c^2+25=0\ \land\ c^2+25>0
After
\neg\exists\,u,v,w,t:\ x^2+25=(ux+v)(wx+t)
Conditions: none
Rule: contradiction · Uses: S12.1, S12.2
Leaf basis: contradiction + quantifier_negation
S12.1 gives c²+25=0 and S12.2 gives c²+25>0, a contradiction. So the supposed factorization does not exist. S12.1 to S12.3 together prove Lemma L_no_linear_factor. The same argument works with real c, so x²+25 has no degree-one factor even in ℝ[x]; in general factorability depends on the coefficient field, as with x²−2 (see the error controls).
Error controls and negative controls
A sum of squares is not a difference of squares
The first error named in the MKO is to apply the difference-of-squares formula to a sum of squares. (x−5)(x+5) expands to x²−25, not x²+25 (S11); moreover x²+25 has no degree-one factor at all (S12), because c²+25 is positive for every real c.
Agreement at finitely many points is not an identity
The second error named in the MKO is to pass off finite numerical agreement as an identity without degree-bound evidence. x³ and x agree at −1, 0 and 1 but are different polynomials (S13). Every factorization here is verified by coefficient comparison (S06, S10); the grid checks N1, N6, N7 and N9 are designed with a degree bound and serve only as support.
The coefficient field and the common factor
Factorability depends on the coefficient field (MKO para2): x²−2 is (x−√2)(x+√2) over ℝ but has no degree-one factor over ℚ (this rests on √2 being irrational, not proved here). Also, a common factor once taken out must be kept: 3x²+3x−18 is not (x+3)(x−2), whose leading coefficient is 1. Factoring is not equation solving either; finding roots with the zero-product property also requires specifying the number system.
- x²+25=(x−5)(x+5) →
reject — The right side expands to x²−25, and the constant term −25≠25. - x³ and x agree at x=−1, 0 and 1, so x³=x is a polynomial identity →
reject — The x³-coefficients are 1≠0; at x=2, 8≠2. - 3x²+3x−18=(x+3)(x−2) →
reject — (x+3)(x−2)=x²+x−6, with leading coefficient 1≠3 and constant term −6≠−18; the common factor 3 was dropped. - x²+x−6=(x−3)(x+2) →
reject — (x−3)(x+2)=x²−x−6, whose x-coefficient −1≠1.