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.
FALSE: for every
Statement
FALSE. The statement
for every .
The claim is what a text whose natural numbers begin at would state truly. In this library contains (The natural numbers (von Neumann)), and the statement acquires a counterexample at its very first index.
Facts & Assumptions
Given: The canonical natural (The canonical natural of a field) and the real finite sum of Finite sums and finite products, by recursion; contains (The natural numbers (von Neumann)).
for every real , including ; and for (Integer powers , Multiplication by zero: , Field).
The true statement: for (, and for , clause 2), proved from the binomial theorem at , (The binomial theorem in : ).
Refutation
Evaluate the left-hand side at . The sum runs over , so by [L1] it is the single term .
That term is : by [L3], by [L2], and . So the sum equals , not , and the displayed statement is false at .
Where the hypothesis is spent in the true version. [L4] obtains the identity by evaluating the binomial theorem at , : the left-hand side becomes , which is only for , while by [L3]. That single evaluation is the entire difference between the true statement and the false one.
Remarks
-
The convention is not the culprit. It is what makes the binomial theorem itself true at and at , with no exceptional case; the price is that one of its corollaries carries a hypothesis. Changing the convention would move the exception, not remove it.
-
The concrete picture. In Pascal's triangle computed to row , with Pascal's rule checked at every interior entry the alternating sums of rows to are all and the alternating sum of row is . A reader who computes from row onwards sees only the true pattern.
Depends on
- $\sum_{k<n+1}\binom{n}{k} = 2^{n}$, and $\sum_{k<n+1}(-1)^{k}\iota\!\binom{n}{k} = 0$ for $n \ge 1$
- The binomial theorem in $\mathbb{R}$: $(x+y)^{n} = \sum_{k<n+1} \iota\!\binom{n}{k}\, x^{k} y^{\,n-k}$
- The set $[A]^{k}$ of $k$-element subsets and the binomial coefficient $\binom{n}{k} := \lvert [n]^{k}\rvert$
- Integer powers $a^m$
- The canonical natural $\iota(n) = n \cdot 1_F$ of a field
- Finite sums and finite products, by recursion
- The natural numbers $\mathbb{N}$ (von Neumann)
- Laws of finite sums and finite products
- Multiplication by zero: $0 \cdot a = 0$
- Field
Used by
Nothing in the library uses this result yet.
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 86 results over 30 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.
Sources
- Binomial coefficient (Wikipedia) (standard reference, not scraped)
- Binomial theorem (Wikipedia) (standard reference, not scraped)
- Pascal's triangle (Wikipedia) (standard reference, not scraped)