# Polynomial factorization over the rationals: verifying common factors, binomial products and differences of squares by comparing coefficients [← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-factorization/) This is an owner-adopted natural-language teaching guide. Finite/arithmetic checks are not universal proofs; no Lean was run, and review scope is recorded per revision. Original source status labels are retained as historical data. Formulas retain exact TeX; no new semantic AST is invented. derivation-mko-factorization-01 · production-20261019-adopted-96 ## Goal and scope In ℚ[x]: (1) factor p(x)=3x²+3x−18 as 3(x+3)(x−2); (2) factor q(x)=2x²−50 as 2(x−5)(x+5); verify each factorization by expanding and comparing every coefficient. (3) Prove that x²+25≠(x−5)(x+5) and that x²+25 is not a product of two degree-one factors. (4) Explain why x³ and x take equal values at x=−1, 0, 1 and still are different polynomials. Within the MKO's scope: one formal variable x, rational coefficients, finite coefficient data. It illustrates common factors, binomial products and differences of squares, with coefficient comparison as the test for an identity. It gives no complete factorization algorithm for all polynomials (as the MKO states); the choice of a and b is a trial confirmed by the expansion that follows. The difference between factoring x²−2 over ℚ and over ℝ is only remarked on and not proved here; the canonical MKO and its English edition are not changed. ## Givens and symbols - distributive - add_comm - mul_comm - zero_product - square_nonneg - numeric_evaluation - G1 — Fix a formal variable x with coefficients in ℚ, represented by finite coefficient data; trailing zeros are removed from factors and products (MKO assumptions a1, a2). - G2 — p(x)=3x²+3x−18, q(x)=2x²−50 and s(x)=x²+25; the monomials x³ and x for comparison. - \mathbb{Q}[x] — all univariate polynomials with rational coefficients - p=f\cdot g — a proposed factorization: a polynomial identity - a,\ b,\ d — rational constants in the binomial product and difference of squares - p(c) — evaluation at x=c ## Rules and sources - distributive · prerequisite — Distributivity: u(v+w)=uv+uw; with commutativity also (v+w)u=vu+wu. - add_comm · prerequisite — Commutativity of addition: u+v=v+u. - mul_comm · prerequisite — Commutativity of multiplication: uv=vu (in commutative number systems such as ℤ, ℚ, ℝ, ℂ). - zero_product · prerequisite — Zero-product property: in ℤ, ℚ, ℝ, ℂ (or any integral domain), uv=0 ⇔ u=0 or v=0. - square_nonneg · prerequisite — Squares are nonnegative: for every real u, u²≥0, and u²=0 ⇔ u=0. - numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable. - forall_elim · prerequisite — ∀-elimination (instantiation): if ∀x∈D, P(x) holds and a∈D, then P(a) holds. - eq_replace · prerequisite — Replacement of equals: an expression inside a statement may be replaced by an equal expression without changing whether the statement is true. - add_inverse · prerequisite — Additive inverse: every u has −u with u+(−u)=0; u−v means u+(−v). - neg_mul · prerequisite — Signs and multiplication: (−u)v=−(uv) and (−u)(−v)=uv. - contradiction · prerequisite — Proof by contradiction: if assuming ¬P leads to a contradiction (a statement and its negation both hold), then P holds. - mul_inverse_nonzero · prerequisite — Inverse of a nonzero number: in ℚ, ℝ or ℂ, if u≠0 there is 1/u with u·(1/u)=1, and v/u means v·(1/u). 0 has no inverse, so v/0 is undefined. - mul_zero · prerequisite — Multiplying by zero: u·0=0. Reason: u·0=u·(0+0)=u·0+u·0; subtracting u·0 from both sides gives 0=u·0. - order_basics · prerequisite — Order of the reals: exactly one of uv holds; u0 give uwvw. - quantifier_negation · prerequisite — Negating quantifiers: ¬(∀x, P(x)) is equivalent to ∃x, ¬P(x), and ¬(∃x, P(x)) is equivalent to ∀x, ¬P(x). - and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q. - mko_factorization · cited — In Q[x], a proposed factorization p=f·g is a polynomial identity: after expansion and collection of like terms, every coefficient agrees. This entry illustrates binomial products, common factors, and differences of squares; it does not provide a complete factorization algorithm for all polynomials. · mko-factorization - poly_eq_coeff · prerequisite — Two polynomials in ℚ[x] are equal exactly when, for every k, their coefficients of x^k are equal (coefficients not listed count as 0). - like_terms · prerequisite — Combining like terms: c x^k+d x^k=(c+d)x^k (distributivity); terms of different powers are not combined. - eval_hom · prerequisite — For c∈ℚ (or c∈ℝ), evaluation f↦f(c) satisfies (f+g)(c)=f(c)+g(c) and (fg)(c)=f(c)g(c); equal polynomials have equal values at every c. - L_binom · lemma — For a,b∈ℚ, (x+a)(x+b)=x²+(a+b)x+ab in ℚ[x]. - L_diffsq · lemma — For d∈ℚ, (x−d)(x+d)=x²−d² in ℚ[x]. - L_no_linear_factor · lemma — There are no rationals u, v, w, t with u≠0 and w≠0 such that x²+25=(ux+v)(wx+t); that is, x²+25 is not a product of two degree-one factors in ℚ[x]. ## Main derivation S01 · definitionBefore 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 g Conditions: 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 · equivalentBefore (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 · equivalentBefore 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 · impliesBefore 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 · equivalentBefore (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 · equivalentBefore 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 · equivalentBefore (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 · equivalentBefore 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 · equivalentBefore 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 · equivalentBefore 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 · impliesBefore 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 · impliesBefore 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 · impliesBefore x^3\ \text{and}\ x\ \text{at}\ x=-1,0,1 After \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 · impliesBefore p,\ q,\ s,\ x^3\ \text{vs}\ x After 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 x Conditions: 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 · equivalentBefore (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 · equivalentBefore 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 · equivalentBefore (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 · impliesBefore 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)=0 Conditions: 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 · impliesBefore 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 · impliesBefore 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). ## Reverse audits - S14 · sufficient_goal_reduction · S06, S10, S11, S12, S13, and_intro_elim — Goal G: the four conclusions. Sufficient condition H: the separate conclusions of S06, S10, S11, S12 and S13; H⇒G is just conjunction. H is proved forwards by coefficient computation and contradiction; G is never used as a premise. - S13 · premise_audit · poly_eq_coeff, eval_hom, numeric_evaluation — The inequality is proved by coefficients, not by substitution; N13 is a finite check at three points and N14 shows a fourth point differs. The fact that polynomials of degree at most d agreeing at d+1 points are identical is not proved here and is used only to explain why three points are too few. - S12.3 · premise_audit · S12.1, S12.2, contradiction — The contradiction comes from two conclusions about the same c; the assumption for contradiction is discharged here. - S12.2 · premise_audit · square_nonneg, order_basics — It holds for every real c, not just at finitely many points; the minimum 25 is reached at c=0 (N12). - S12.1 · premise_audit · eval_hom, mul_inverse_nonzero, mul_zero — u≠0 is needed to form c=−v/u; this reasoning takes place inside the scope of the assumption to be refuted. - S12 · premise_audit · L_no_linear_factor, eval_hom, square_nonneg — The conclusion concerns two degree-one factors only; writing x²+25 as 1·(x²+25), with a constant factor, is not a new factorization (MKO assumption a2). - S11 · premise_audit · S09, poly_eq_coeff, numeric_evaluation — One differing coefficient suffices for inequality (N10, N11); this rejects only this candidate, and whether any other factorization exists is settled in S12. - S10 · inverse_equivalence · eq_replace, poly_eq_coeff — Replacement of equals, two-way; all three coefficients are compared. - S09 · inverse_equivalence · L_diffsq, numeric_evaluation — The constant must be written as the square of a rational (N8); the identity is two-way. - S08 · inverse_equivalence · distributive, numeric_evaluation — Expanding returns the original: 2·1=2 and 2·(−25)=−50. - S07.1 · inverse_equivalence · L_binom, add_inverse, neg_mul — Substitution into an identity and simplification; every move replaces equals by equals. - S07 · inverse_equivalence · L_diffsq — The identity is two-way (N7). Note that it applies to a difference only: x²+d² is not covered. - S06 · inverse_equivalence · eq_replace, poly_eq_coeff — Replacement of equals works both ways; the factor 3 must be kept, or the leading coefficient would become 1. - S05 · inverse_equivalence · L_binom, poly_eq_coeff — The lemma is an identity and stays two-way after substituting particular a and b. - S04 · premise_audit · S02, numeric_evaluation — Only this candidate pair is checked (N4, N5); it is not claimed to be unique or produced by an algorithm. - S03 · inverse_equivalence · distributive, poly_eq_coeff, numeric_evaluation — Expanding 3(x²+x−6) returns the original, with all three coefficients equal (N2, N3), so the step is two-way. - S02.2 · inverse_equivalence · like_terms, mul_comm, add_comm — Combining like terms and splitting the coefficient back are inverse moves, both identities. - S02.1 · inverse_equivalence · distributive — Distributivity is an identity; read backwards it is taking out a common factor. - S02 · inverse_equivalence · L_binom — Both sides are the same polynomial and may replace each other either way; the lemma holds for all rational a, b (N1 checks it with a degree bound). - S01 · premise_audit · G1, mko_factorization, poly_eq_coeff — This step only states the test; every factorization below is verified by it. ## Error controls and negative controls A sum of squares is not a difference of squaresThe 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 identityThe 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 factorFactorability 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. ## Result and limitations In ℚ[x], 3x²+3x−18=3(x+3)(x−2) and 2x²−50=2(x−5)(x+5), each verified by expanding and comparing every coefficient. x²+25≠(x−5)(x+5) (constant terms 25≠−25), and x²+25 is not a product of two degree-one factors (otherwise c²+25=0 would have a rational solution). x³ and x agree at −1, 0 and 1, but x³≠x. - The claim that x²−2 has no degree-one factor over ℚ rests on the irrationality of √2; it is only remarked on here, not proved. - The pair a, b in S04 is a candidate found by trial; this guide gives no general factorization algorithm (the MKO explicitly makes no such claim). - N13 is a finite check at three points, used precisely to show that finite agreement is not enough; N1, N5 to N10 and N15 are grid checks designed with a degree bound, supporting the coefficient comparisons. ## Verification and source binding 17 declared checks for this guide; only the listed expressions are covered. - source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f - adopted source SHA-256: 96eb7a6a6d15bd4bc31f1e82c3a0f24b1950d37ba0e48a4f3336de4395e33750 - original source SHA-256: 96eb7a6a6d15bd4bc31f1e82c3a0f24b1950d37ba0e48a4f3336de4395e33750 - Lean: NOT_RUN · independent AI: NOT_MEASURED [Same-source full JSON (formulas, ASTs, controls and revision log)](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-factorization-01.json)