Counterexamples and domain eligibility: primality of n²+n+11, the failure set and the least counterexample

Goal and scope

Let U={n∈ℤ ∣ 0≤n≤12}, V={n∈ℤ ∣ 0≤n≤9}, m(n)=n²+n+11 and P(n): 'm(n) is prime'. Decide φ_U: ∀n∈U P(n); find the failure set F_U and the least counterexample; decide whether the candidate −11 is eligible; and decide φ_V: ∀n∈V P(n).

Works inside the MKO's scope: explicit finite integer domains and decidable predicates. Shows the two conditions of a counterexample (in the domain, predicate fails), how eligibility changes under restriction, the complete failure set and the least counterexample, and a proof of a finite universal by an argument valid for every element. Makes no universal claim about n²+n+11 over ℕ or ℤ; takes 'every integer a≥2 has a prime divisor' as a premise; does not change the canonical MKO or its English edition.

Givens and symbols

• divides_def
• division_algorithm
• order_basics
• numeric_evaluation
• prime_def

• G1 — U={n∈ℤ ∣ 0≤n≤12} and V={n∈ℤ ∣ 0≤n≤9}; both are explicit finite integer domains, and V⊆U.
• G2 — m(n)=n²+n+11; P(n): 'm(n) is prime', decidable exactly for every integer. φ_U: ∀n∈U P(n); φ_V: ∀n∈V P(n).
• G3 — Candidates whose eligibility is to be decided: c=−11 (for φ_U) and c=10 (for φ_V).

• U,\ V — domains: the integers with 0≤n≤12 and with 0≤n≤9
• m(n) — n²+n+11
• P(n) — the predicate 'm(n) is prime'
• F_U,\ F_V — the failure sets {n∈U ∣ ¬P(n)} and {n∈V ∣ ¬P(n)}
• p\mid m,\ p\nmid m — p divides m; p does not divide m

Rules and sources

• divides_def · prerequisite — Divisibility: for integers a, b, a∣b means there is an integer k with b=ak.
• division_algorithm · prerequisite — Division algorithm: for an integer a and a positive integer b there are unique integers q, r with a=bq+r and 0≤r<b.
• order_basics · prerequisite — Order of the reals: exactly one of u<v, u=v, u>v holds; u<v and v<w give u<w; u<v gives u+w<v+w; u<v and w>0 give uw<vw; u<v and w<0 give uw>vw.
• numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
• set_builder · prerequisite — Set-builder notation: x∈{y∈A ∣ P(y)} if and only if x∈A and P(x).
• and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
• exists_intro · prerequisite — ∃-introduction: if some a∈D satisfies P(a), then ∃x∈D, P(x).
• case_analysis · prerequisite — Proof by cases: if P∨Q holds and both P⇒R and Q⇒R are proved, then R holds. The cases must cover every possibility.
• distributive · prerequisite — Distributivity: u(v+w)=uv+uw; with commutativity also (v+w)u=vu+wu.
• add_assoc · prerequisite — Associativity of addition: (u+v)+w=u+(v+w).
• mul_comm · prerequisite — Commutativity of multiplication: uv=vu (in commutative number systems such as ℤ, ℚ, ℝ, ℂ).
• square_nonneg · prerequisite — Squares are nonnegative: for every real u, u²≥0, and u²=0 ⇔ u=0.
• contrapositive · prerequisite — Contrapositive: P⇒Q is equivalent to ¬Q⇒¬P. The converse Q⇒P is in general not equivalent to P⇒Q.
• quantifier_negation · prerequisite — Negating quantifiers: ¬(∀x, P(x)) is equivalent to ∃x, ¬P(x), and ¬(∃x, P(x)) is equivalent to ∀x, ¬P(x).
• forall_intro · prerequisite — ∀-introduction (generalization): if a statement is proved for an arbitrary element x, with no extra assumption on x, it holds for every x in the domain.
• set_extensionality · prerequisite — Set equality: A=B if and only if A⊆B and B⊆A, i.e. they have the same elements.
• set_operations_def · prerequisite — Set operations: x∈A∪B ⇔ x∈A or x∈B; x∈A∩B ⇔ x∈A and x∈B; x∈A∖B ⇔ x∈A and x∉B; in a universe U, Aᶜ=U∖A.
• mko_counterexample_def · cited — For ∀x∈U P(x), c is a valid counterexample exactly when c∈U and P(c) is false. One valid counterexample refutes the universal statement. Failure to find one is not itself a proof unless the domain is finite and every element has been checked completely. · mko-counterexample
• mko_quantifier_neg · cited — For an explicit domain under classical truth semantics, ¬∀x∈U P(x) is equivalent to ∃x∈U ¬P(x), and ¬∃x∈U P(x) is equivalent to ∀x∈U ¬P(x). · mko-quantifier
• prime_def · prerequisite — An integer m≥2 is prime when its only positive divisors are 1 and m; m≥2 is not prime (composite) exactly when some integer a has 1<a<m and a∣m.
• prime_divisor_exists · prerequisite — Every integer a≥2 has a prime divisor p (p∣a), and a positive divisor of a positive integer a is at most a. (This follows from well-ordering: the least divisor of a above 1 is prime; it is a premise here.)
• rem_divides · prerequisite — For an integer a and a positive integer b, b∣a exactly when the remainder r in the division a=bq+r (0≤r<b) is 0 (by uniqueness in the division algorithm).
• divides_combo · prerequisite — If p∣u and p∣v then p∣u+v and p∣u−v; if p∣a and a∣m then p∣m.
• L_residue · lemma — For an integer p≥1 and an integer n, writing n=pq+r with 0≤r<p gives m(n)=p(pq²+2qr+q)+m(r); hence p∣m(n) ⇔ p∣m(r).
• L_no_small_factor · lemma — For every integer n, none of 2, 3, 5, 7 divides m(n)=n²+n+11.
• L_trial · lemma — If an integer m≥2 is divisible by no prime p with p²≤m, then m is prime.

Main derivation

c\ \text{is a valid counterexample to}\ \forall n\in U\,P(n)

c\in U\ \land\ \neg P(c)

m(10)=10^2+10+11

m(10)=121=11\cdot 11

m(10)=121=11\cdot 11

\neg P(10)

0\le 10\le 12,\ \neg P(10)

10\in U\land\neg P(10)

10\in U\land\neg P(10)

\neg\forall n\in U\,P(n)

c=-11:\ m(-11)=121

-11\notin U,\ \text{so}\ -11\ \text{is not a counterexample to}\ \varphi_U

n\in V

2\nmid m(n),\ 3\nmid m(n),\ 5\nmid m(n),\ 7\nmid m(n)

0\le n\le 9

11\le m(n)\le 101

11\le m(n)\le 101,\quad 2,3,5,7\nmid m(n)

P(n)\ \text{for an arbitrary}\ n\in V

P(n)\ \text{for an arbitrary}\ n\in V

\forall n\in V\,P(n)

m(11)=11^2+11+11

m(11)=143=11\cdot 13,\ 11\in U,\ \neg P(11)

m(12)=12^2+12+11=167

P(12)

U=V\cup\{10,11,12\}

F_U=\{n\in U\mid\neg P(n)\}=\{10,11\}

F_U=\{10,11\}

\min F_U=10

10\in F_U,\ V\subseteq U

10\notin V,\ F_V=F_U\cap V=\varnothing

\text{S05, S06, S10, S13, S14, S15}

\neg\varphi_U,\ F_U=\{10,11\},\ \min F_U=10,\ -11\ \text{ineligible},\ \varphi_V\ \text{true}

Substeps and lemmas

n=pq+r,\ 0\le r<p

m(n)=p(pq^2+2qr+q)+m(r),\quad p\mid m(n)\Leftrightarrow p\mid m(r)

p=2,\ r\in\{0,1\}

m(0)=11=2\cdot 5+1,\ m(1)=13=2\cdot 6+1;\ 2\nmid m(n)

p=3,\ r\in\{0,1,2\}

m(r)\in\{11,13,17\},\ \text{remainders}\ 2,1,2;\ 3\nmid m(n)

p=5,\ r\in\{0,1,2,3,4\}

m(r)\in\{11,13,17,23,31\},\ \text{remainders}\ 1,3,2,3,1;\ 5\nmid m(n)

p=7,\ r\in\{0,1,2,3,4,5,6\}

m(r)\in\{11,13,17,23,31,41,53\},\ \text{remainders}\ 4,6,3,2,3,6,4;\ 7\nmid m(n)

m\ge 2,\ m\ \text{not prime}

m=ab,\ 2\le a\le b,\ a^2\le m

m=ab,\ 2\le a,\ a^2\le m

\exists\ \text{prime}\ p:\ p\mid m\land p^2\le m

m\ \text{not prime}\Rightarrow\exists\ \text{prime}\ p:\ p\mid m\land p^2\le m

(\forall\ \text{prime}\ p:\ p^2\le m\Rightarrow p\nmid m)\Rightarrow m\ \text{prime}

Reverse audits

• S16 · sufficient_goal_reduction · S05, S06, S10, S13, S14, S15, and_intro_elim — Goal G: the four verdicts. Sufficient condition H: the conclusions of S05, S06, S10, S13, S14 and S15; H⇒G is just conjunction. Each part of H is proved forwards earlier, and G is never used as a premise.
• S15 · premise_audit · S10, S13, set_operations_def — F_V=∅ needs S10 (no failure in V); 10∉V alone would not give F_V=∅.
• S14 · premise_audit · S13, order_basics — It needs F_U to be fully determined (S13); otherwise a smaller failure could not be ruled out.
• S13 · premise_audit · S03, S10, S11, S12, set_extensionality, case_analysis — The case split must cover all 13 elements of U; missing one would leave F_U undetermined.
• S12 · premise_audit · L_no_small_factor, L_trial, rem_divides — All primes up to 12 must be listed; 11 lies outside L_no_small_factor and is decided separately by its remainder (N15, N16).
• S11 · premise_audit · prime_def, set_builder, numeric_evaluation — Both conditions are checked (N12, N13).
• S10 · premise_audit · S09, forall_intro — n must be an arbitrary element of V; had the proof used a property of a specific n, it could not be generalized.
• S09.3 · inverse_equivalence · contrapositive, quantifier_negation — A statement and its contrapositive are equivalent, both ways; the quantifier negation used for the existential is an equivalence too.
• S09.2 · premise_audit · prime_divisor_exists, divides_combo, order_basics — The existence of a prime divisor is a premise of this guide (provable from well-ordering) and is not reproved here.
• S09.1 · premise_audit · prime_def, divides_def, order_basics — a>0 is needed to keep the inequality direction; the range of b follows from m=ab and 1<a<m.
• S09 · premise_audit · S07, S08, L_trial — It needs every prime with p²≤101, namely the primes up to 10: 2, 3, 5, 7 (N10 checks 11²>101); missing any would leave the argument incomplete.
• S08 · premise_audit · order_basics, square_nonneg — Multiplying by a nonnegative number keeps the inequality direction, which needs n≥0; the bound 101 can be recomputed (N9). No converse is claimed.
• S07.5 · premise_audit · L_residue, rem_divides, case_analysis — The seven remainders cover every integer; all seven are computed (N8). The universal conclusion comes from the argument that finitely many remainder cases cover all integers, not from sampling values of n.
• S07.4 · premise_audit · L_residue, rem_divides, case_analysis — The five remainders cover every integer; all five remainders are computed (N7).
• S07.3 · premise_audit · L_residue, rem_divides, case_analysis — The three remainders cover every integer; all three remainders are computed (N6).
• S07.2 · premise_audit · L_residue, rem_divides, case_analysis — The two remainders cover every integer (division algorithm); the remainder in each case is computed exactly (N5).
• S07.1 · premise_audit · division_algorithm, distributive, divides_combo — It needs the division-algorithm decomposition and the expansion identity; the two directions of the resulting ⇔ are justified by subtracting and by adding.
• S07 · premise_audit · L_no_small_factor — It needs only that n is an integer; the lemma does not say m(n) is prime, it only rules out four small prime factors.
• S06 · premise_audit · set_builder, mko_counterexample_def, numeric_evaluation — The verdict needs only the first condition to fail (N3 just recomputes the formula); it is not claimed that φ_U is therefore true, since S05 already showed it false.
• S05 · premise_audit · exists_intro, mko_quantifier_neg — The witness must be in U; refuting a universal needs one witness. No converse is claimed.
• S04 · premise_audit · set_builder, S03, mko_counterexample_def — Both conditions are needed together; ¬P(10) without 10∈U would not be enough.
• S03 · premise_audit · prime_def, divides_def — One proper divisor, 11, is enough; no converse is claimed.
• S02 · inverse_equivalence · numeric_evaluation — Both sides are the same integer and can be recomputed (N1, N2).
• S01 · premise_audit · mko_counterexample_def, G1, G2 — This step only states the definition and derives no new fact; neither condition may be dropped.

Error controls and negative controls

Check domain eligibility first

One misconception named by the MKO is refuting a restricted universal with a value outside the domain. Substituting −11 gives 121, which is composite, but −11∉U, so it is not a counterexample to φ_U (S06). The order is always: check c∈U first, then whether P(c) fails.

Not finding a counterexample is not a proof

Another misconception named by the MKO is treating an unsuccessful search as a general proof. Trying n=0 to 9 gives primes every time, yet n=10 fails; claiming 'true for all n' after searching up to 9 would be wrong. The proof of φ_V is the argument in S07 to S10, valid for every element of V; over an infinite domain no finite search is a proof.

Losing a witness does not prove the restricted universal

MKO paragraph two: after restricting to a subset, an old counterexample may leave the subset and lose eligibility, but that does not make the new universal true. For example W={11,12}⊆U: 10∉W loses eligibility, yet 11∈W still makes P fail, so ∀n∈W P(n) is still false. φ_V is true because of the proof in S10, not because 10∉V.

• m(−11)=121 is composite, so −11 is a counterexample to ∀n∈U P(n) → reject — −11<0, so −11∉U; a failing value outside the domain is not a counterexample.
• n=0 to 9 all make n²+n+11 prime, so it holds for every natural number n → reject — At n=10, n²+n+11=121=11·11, which is not prime.
• 10∉V, so ∀n∈V P(n) is proved → reject — Losing one witness proves no universal; with W={11,12}, 10 is also outside W, yet ∀n∈W P(n) is still false because of 11. φ_V needs the argument of S07 to S10.
• The least counterexample to φ_V is 10 → reject — 10∉V; F_V=∅, so φ_V has no counterexample and no least counterexample exists.

Result and limitations

φ_U (∀n∈U, n²+n+11 is prime, with U the integers 0 to 12) is false: the failure set is F_U={10,11} (121=11·11, 143=11·13), and the least counterexample is 10. The candidate −11 gives 121 but −11∉U, so it is not a counterexample. φ_V (V the integers 0 to 9) is true: for every n∈V, 11≤m(n)≤101 and none of 2, 3, 5, 7 divides m(n), so m(n) is prime; F_V=∅ and there is no least counterexample.

• N5 to N8 are finite checks over all remainders r for each p; the universal conclusion L_no_small_factor rests on L_residue (S07.1) and on the remainder cases covering every integer, not on these checks alone.
• 'Every integer a≥2 has a prime divisor' is a premise here and is not proved. N11 and N17 are independent recomputations with isprime; the argument does not depend on them.

Verification and source binding

18 declared checks for this guide; only the listed expressions are covered.

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: 50a0b8ce1009ddb04ac5c306440773799a1f5d16fecb299d252315f534a48568
• original source SHA-256: 50a0b8ce1009ddb04ac5c306440773799a1f5d16fecb299d252315f534a48568
• Lean: NOT_RUN · independent AI: NOT_MEASURED

Same-source full JSON (formulas, ASTs, controls and revision log)