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.
Strong (complete) induction
Statement
Let be a property of naturals such that for every , if holds for all then . Then holds for all . (At the hypothesis is vacuous, so is forced.)
Facts & Assumptions
Given: A property satisfying the strong-induction hypothesis : for every , .
Well-ordering: every nonempty subset of has a least element (The well-ordering principle).
Exactly one of , , holds (Trichotomy of the order on ).
Proof
Suppose fails somewhere; let , a nonempty subset of .
By well-ordering [L1], has a least element , so for every ; hence every lies outside , since would give , which [L2] does not allow alongside ; that is, holds for all .
By the hypothesis applied at , holds, so .
But by construction, a contradiction; hence is empty and holds for all .
Depends on
Used by
- Converse of Lagrange for finite abelian groups: every divisor occurs as a subgroup order Corollary
- The 2-adic absolute value gives an ultrametric on ℚ, in which every triangle is isosceles and every point of a ball is a centre Example
- A normal sequence of entourages yields a uniformly continuous pseudometric with controlled dyadic balls Lemma
- Every nonzero nonunit polynomial over a field factors into irreducible polynomials Lemma
- Every subset of an at most countable set is at most countable Lemma
- For positive integers a and b: a ∣ b if and only if vₚ(a) ≤ vₚ(b) for every prime p Lemma
- If every diagonal value of an incidence function is a unit, recursive interval formulas construct both a left and a right convolution inverse Lemma
- A maximal-order cyclic subgroup splits off a finite abelian p-group Theorem
- Cauchy's theorem for finite abelian groups Theorem
- Division by a monic polynomial over a commutative ring Theorem
- Every finite abelian p-group is a direct product of cyclic p-groups Theorem
- Every integer n ≥ 1 is a finite product of primes: there are r ∈ ℕ and a list p : r → ℤ of primes with n = ∏_i<r pᵢ, the case n = 1 being the empty product Theorem
- Every nontrivial finite abelian group is an internal direct product of indecomposable subgroups Theorem
- ℕ × ℕ ≈ ℕ Theorem
- On a finite chain, the Möbius function is 1 on the diagonal, -1 on covers and 0 on longer intervals Theorem
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 29 results over 15 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
- Mathematical induction (Wikipedia) (standard reference, not scraped)
- Well-ordering principle (Wikipedia) (standard reference, not scraped)
- Peano axioms (Wikipedia) (standard reference, not scraped)