Alphabeta Math
CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Bernoulli fails for x<−1: x=−4, n=3

Statement refuted

Refuted claim: the inequality (1+x)n≥1+nx of Bernoulli's inequality (1+x)n≥1+nx holds for every real x and every natural n, with powers as in Integer powers am.

Witness: x:=−4, n:=3. Then (1+x)3=(−3)3=−27 while 1+3x=−11, so (1+x)3<1+3x and the inequality fails. Two boundary remarks sharpen the failure: at n=1 the two sides agree for every x, so a failure needs n≥2; and at x=−3, n=3 the two sides happen to agree (−8=−8), so a witness must be chosen rather than assumed. The hypothesis x≥−1 of Bernoulli's inequality (1+x)n≥1+nx is therefore load-bearing.

Facts & Assumptions

Given: The real number x:=−4 and the natural number n:=3, with 3 and 4 also denoting the canonical naturals in R.

[L1]

Definition of powers (Integer powers am): a0=1 and aj+1=aja for every real a and every natural j.

[L2]

Multiplicative sign and positivity rules: (−u)v=−(uv) and (−u)(−v)=uv for all reals u,v (Sign rules for products: (−a)b=−(ab) and (−a)(−b)=ab); 1>0 (The multiplicative identity is positive); and a product of two positive reals is positive (Sign rules for products and monotonicity of multiplication).

[L3]

Adding a constant preserves the strict order: x<y implies x+c<y+c for all reals x,y,c (Order is preserved by adding a constant and by adding inequalities).

[L4]

Bernoulli's inequality (Bernoulli's inequality (1+x)n≥1+nx): for every real x≥−1 and every natural n, (1+x)n≥1+nx.

Counterexample

technique · direct
1.1L1L2algebra

At the witness, 1+x=1+(−4)=−3 and (−3)3=(−3)2⋅(−3)=9⋅(−3)=−(9⋅3)=−27 by the recursion clause of [L1] and the sign rules of [L2]; so (1+x)3=−27.

1.2L2algebra

Also 3x=3⋅(−4)=−(3⋅4)=−12 by [L2], and 1+3x=1+(−12)=−11 by field arithmetic; so the right-hand side of the claimed inequality is −11 at the witness.

1.3L1L2algebra

Boundary evaluations: at n=0 both sides are 1; at n=1 the recursion clause gives (1+x)1=(1+x)0(1+x)=1+x=1+1⋅x for every x; at x=−3, n=3 one gets (1+x)3=(−2)3=−8 and 1+3x=1+(−9)=−8, so the two sides agree there too, at a point with x<−1; and at x=−1 with n≥2 the left side is 0 while 1+nx=1−n<0.

2.1step 1.1step 1.2L2L3algebra

The comparison, using the evaluations of step 1.1 and step 1.2: 0<16, because 1>0 gives 0<1, repeatedly adding constants by [L3] gives 0<4, and 4⋅4=16>0 is a product of positives by [L2]; adding c=−27 to 0<16 by [L3] gives −27<16+(−27)=−11.

3.1step 1.1step 1.2step 1.3step 2.1L4∎

Hence (1+x)3=−27<−11=1+3x at x=−4, n=3, so the conclusion of the inequality fails there; since −4<−1, the hypothesis x≥−1 of [L4] cannot be dropped, and the evaluations of step 1.3 show that equality holds at n=0, at n=1, and at the example x=−3, n=3; these evaluations do not classify all cases with x<−1.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

20 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources