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

[← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-counterexample/)

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-counterexample-01 · production-20261019-adopted-96



## 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

S01 · definitionBefore

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

After

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

Conditions: none

Rule: mko_counterexample_def · Uses: G1, G2, mko_counterexample_def

Leaf basis: mko_counterexample_def

By the MKO, c is a valid counterexample to φ_U exactly when both hold: c lies in the domain U, and P(c) is false. The order of checking is domain eligibility first, then failure of the predicate.



S02 · equivalentBefore

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

After

m(10)=121=11\cdot 11

Conditions: none

Rule: numeric_evaluation · Uses: G2

Leaf basis: numeric_evaluation

Exact computation: 10²+10+11=100+10+11=121, and 11·11=121.



S03 · impliesBefore

m(10)=121=11\cdot 11

After

\neg P(10)

Conditions: 1<11<121; 11\mid 121

Rule: prime_def · Uses: S02, prime_def

Leaf basis: prime_def + divides_def + numeric_evaluation

121≥2, and a=11 satisfies 1<11<121 and 11∣121 (121=11·11). By the definition of prime, 121 is composite, so P(10) is false. The perfect square 121 is composite too; there is no exception.



S04 · impliesBefore

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

After

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

Conditions: none

Rule: mko_counterexample_def · Uses: S01, S03, G1

Leaf basis: set_builder + mko_counterexample_def + and_intro_elim

Eligibility first: 10 is an integer with 0≤10≤12, so 10∈U by set-builder notation. Then failure: S03 gives ¬P(10). Both conditions hold, so 10 is a valid counterexample to φ_U.



S05 · impliesBefore

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

After

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

Conditions: none

Rule: mko_quantifier_neg · Uses: S04, exists_intro, mko_quantifier_neg

Leaf basis: exists_intro + mko_quantifier_neg

∃-introduction gives ∃n∈U ¬P(n); by the negation law for restricted quantifiers (mko-quantifier) this is equivalent to ¬∀n∈U P(n). One valid counterexample suffices to refute φ_U; the full list of failures is not needed for that.



S06 · impliesBefore

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

After

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

Conditions: none

Rule: mko_counterexample_def · Uses: S01, G1, G2, G3

Leaf basis: set_builder + mko_counterexample_def + order_basics

The formula can be evaluated outside the domain: (−11)²+(−11)+11=121−11+11=121, which is composite. But eligibility comes before failure: −11<0 fails 0≤n≤12, so −11∉U. By the definition in S01, −11 is not a counterexample to φ_U; its failing value is irrelevant to φ_U.



S07 · theorem_applicationBefore

n\in V

After

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

Conditions: n\in\mathbb{Z}

Rule: L_no_small_factor · Uses: G2, L_no_small_factor

Leaf basis: division_algorithm + rem_divides + divides_combo + case_analysis

To decide φ_V we cannot rely on 'the search found nothing'; every element of V needs a reason. The first tool is Lemma L_no_small_factor: for every integer n, none of 2, 3, 5, 7 divides m(n). Elements of V are integers, so the lemma applies. It is proved in sub-steps S07.1 to S07.5.



S08 · impliesBefore

0\le n\le 9

After

11\le m(n)\le 101

Conditions: n\ge 0

Rule: order_basics · Uses: G1, G2, order_basics

Leaf basis: order_basics + square_nonneg + numeric_evaluation

For 0≤n≤9: n≥0 gives n²≥0 and n²+n≥0, so m(n)≥11; from n≤9 and n≥0 we get n²=n·n≤9·n≤81, so m(n)≤81+9+11=101.



S09 · theorem_applicationBefore

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

After

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

Conditions: m(n)\ge 2

Rule: L_trial · Uses: S07, S08, L_trial

Leaf basis: prime_def + order_basics + numeric_evaluation

Take an arbitrary n∈V. If a prime p satisfies p²≤m(n)≤101, then p≤10 (since 11²=121>101), so p∈{2,3,5,7}; S07 says none of these divides m(n). Also m(n)≥11≥2 (S08). By Lemma L_trial, m(n) is prime, that is P(n).



S10 · impliesBefore

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

After

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

Conditions: none

Rule: forall_intro · Uses: S09, forall_intro

Leaf basis: forall_intro

S07 to S09 proved P(n) for an arbitrary n∈V, with no assumption on n beyond 0≤n≤9. By ∀-introduction, φ_V is true. This is an argument valid for every element of the finite domain V, not 'a search found no counterexample'; N11 recomputes isprime for n=0 to 9 one by one as an independent complete check.



S11 · impliesBefore

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

After

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

Conditions: 1<11<143

Rule: prime_def · Uses: G1, G2, prime_def

Leaf basis: prime_def + set_builder + numeric_evaluation

11²+11+11=121+22=143=11·13 with 1<11<143, so 143 is composite; 0≤11≤12, so 11∈U. 11 is a second valid counterexample to φ_U.



S12 · theorem_applicationBefore

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

After

P(12)

Conditions: 167\ge 2

Rule: L_trial · Uses: L_no_small_factor, L_trial, G2

Leaf basis: rem_divides + numeric_evaluation + order_basics

m(12)=144+12+11=167. The primes with p²≤167 are those with p≤12: 2, 3, 5, 7, 11 (since 13²=169>167). By L_no_small_factor, 2, 3, 5, 7 do not divide 167; and 167=11·15+2 leaves remainder 2≠0, so 11∤167. By Lemma L_trial, 167 is prime and P(12) holds.



S13 · impliesBefore

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

After

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

Conditions: none

Rule: set_extensionality · Uses: S03, S10, S11, S12, G1

Leaf basis: set_extensionality + case_analysis + set_builder

The elements of U are the integers 0 to 12, split into V (0 to 9) and the three elements 10, 11, 12, which covers every case. P holds throughout V (S10) and at 12 (S12), and fails at 10 and 11 (S03, S11). So the failure set is exactly {10,11}: both inclusions follow from the case-by-case check. This is a complete verification of a finite domain.



S14 · impliesBefore

F_U=\{10,11\}

After

\min F_U=10

Conditions: F_U\neq\varnothing

Rule: order_basics · Uses: S13

Leaf basis: order_basics + numeric_evaluation

By MKO assumption a2, the least counterexample is the numerically smallest element of the finite failure set. F_U={10,11} is nonempty and 10<11, so the least counterexample is 10. The value comes from the complete F_U, not from the first failure met in a sample.



S15 · impliesBefore

10\in F_U,\ V\subseteq U

After

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

Conditions: none

Rule: set_operations_def · Uses: S10, S13, G1, G3

Leaf basis: set_operations_def + set_builder

Restrict to V: 10>9, so 10∉V and it loses eligibility as a counterexample to φ_V; so does 11. The failure set of V is F_V={n∈V ∣ ¬P(n)}=F_U∩V=∅, so φ_V has no counterexample, and its least counterexample is explicitly reported as nonexistent. Note that φ_V is true because of the argument in S10, not because 10 lost eligibility; losing a witness proves no universal statement by itself.



S16 · impliesBefore

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

After

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

Conditions: none

Rule: and_intro_elim · Uses: S05, S06, S10, S13, S14, S15

Leaf basis: and_intro_elim

Summary: φ_U is false (S05, valid counterexample 10); F_U={10,11} with least counterexample 10 (S13, S14); −11 makes the formula fail but is not in U, so it is not a counterexample (S06); φ_V is true (S10), F_V=∅, and there is no least counterexample (S15).







## Substeps and lemmas

S07.1 · impliesBefore

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

After

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

Conditions: p\ge 1

Rule: distributive · Uses: division_algorithm, distributive, divides_combo

Leaf basis: division_algorithm + distributive + add_assoc + mul_comm + divides_combo

By the division algorithm write n=pq+r with 0≤r<p. Expanding: (pq+r)²+(pq+r)+11=p²q²+2pqr+r²+pq+r+11=p(pq²+2qr+q)+(r²+r+11)=p(pq²+2qr+q)+m(r) (N4 checks this polynomial identity on a grid). Since p divides p(pq²+2qr+q), the sum and difference property gives: if p∣m(n), subtracting yields p∣m(r); if p∣m(r), adding yields p∣m(n). This proves the auxiliary Lemma L_residue.



S07.2 · impliesBefore

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

After

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

Conditions: none

Rule: L_residue · Uses: L_residue, rem_divides, case_analysis

Leaf basis: rem_divides + case_analysis + numeric_evaluation + division_algorithm

p=2: the remainder r is 0 or 1. m(0)=11=2·5+1 and m(1)=13=2·6+1 both leave remainder 1≠0, so 2∤m(0) and 2∤m(1). By L_residue, 2∤m(n) for every integer n.



S07.3 · impliesBefore

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

After

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

Conditions: none

Rule: L_residue · Uses: L_residue, rem_divides, case_analysis

Leaf basis: rem_divides + case_analysis + numeric_evaluation + division_algorithm

p=3: for r=0, 1, 2, m(r)=11, 13, 17; 11=3·3+2, 13=3·4+1, 17=3·5+2, with remainders 2, 1, 2, none of them 0, so 3 divides none of the three values. By L_residue, 3∤m(n) for every integer n.



S07.4 · impliesBefore

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

After

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

Conditions: none

Rule: L_residue · Uses: L_residue, rem_divides, case_analysis

Leaf basis: rem_divides + case_analysis + numeric_evaluation + division_algorithm

p=5: for r=0 to 4, m(r)=11, 13, 17, 23, 31, whose remainders on division by 5 are 1, 3, 2, 3, 1, none of them 0. By L_residue, 5∤m(n) for every integer n.



S07.5 · impliesBefore

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

After

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

Conditions: none

Rule: L_residue · Uses: L_residue, rem_divides, case_analysis

Leaf basis: rem_divides + case_analysis + numeric_evaluation + division_algorithm

p=7: for r=0 to 6, m(r)=11, 13, 17, 23, 31, 41, 53, whose remainders on division by 7 are 4, 6, 3, 2, 3, 6, 4, none of them 0. By L_residue, 7∤m(n) for every integer n. S07.2 to S07.5 together prove Lemma L_no_small_factor.



S09.1 · impliesBefore

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

After

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

Conditions: a>0

Rule: prime_def · Uses: prime_def, order_basics

Leaf basis: prime_def + divides_def + order_basics

Suppose m≥2 is not prime. By definition there is an integer a with 1<a<m and a∣m; let b=m/a, an integer, with b>1 because a<m and b<m because a>1. Swap the two if a>b, so we may assume 2≤a≤b. Multiplying by the positive a gives a²≤ab=m.



S09.2 · impliesBefore

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

After

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

Conditions: none

Rule: prime_divisor_exists · Uses: S09.1, prime_divisor_exists, divides_combo

Leaf basis: prime_divisor_exists + divides_combo + order_basics

a≥2, so a has a prime divisor p, with p≤a. From p∣a and a∣m we get p∣m; from 0<p≤a we get p²≤a²≤m. Hence: if m≥2 is not prime, some prime p with p²≤m divides m.



S09.3 · equivalentBefore

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

After

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

Conditions: m\ge 2

Rule: contrapositive · Uses: S09.2, contrapositive

Leaf basis: contrapositive + quantifier_negation

Take the contrapositive of S09.2: if no prime p with p²≤m divides m (and m≥2), then m is prime. Negating 'there is such a p' by quantifier negation gives 'every prime with p²≤m fails to divide m'. S09.1 to S09.3 prove Lemma L_trial.







## 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 firstOne 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 proofAnother 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 universalMKO 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)](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-counterexample-01.json)