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.
Multiplication is commutative
Statement
For all : .
Facts & Assumptions
Given: multiplication (Multiplication of natural numbers).
for all (Zero and one under multiplication).
The successor-left law (Distributivity and the successor law for multiplication).
The induction principle (The principle of mathematical induction).
Proof
Base : and by [L1], so .
Inductive hypothesis: .
Step: , using the multiplication recursion, the hypothesis, then the successor-left law [L2].
By induction [L3], for all , hence for all .
Depends on
Used by
- Exponentiation of natural numbers, mⁿ, and its agreement with the integer power in ℝ Definition
- lceil m/n rceil for naturals m and n ≥ 1: the least q ∈ ℕ with m ≤ n q Definition
- The factorial n! and the falling factorial n^underlinek, defined by recursion in ℕ Definition
- FALSE: for all sets A and B with B having at least two elements, A × B is strictly larger than A False statement
- A finite sum is unchanged by a permutation of its index range: ∑_k<n a_π(k) = ∑_k<n aₖ for every bijection π : n → n Lemma
- Integer multiplication is well defined Lemma
- Laws of finite sums and products in ℕ, and ι(∑_k<n aₖ) = ∑_k<n ι(aₖ) Lemma
- Order is compatible with multiplication Lemma
- A finite set with n elements has exactly binomn2 two-element subsets, and 2binomn2 = n(n-1) Theorem
- binomnk k! (n-k)! = n! for k ≤ n; hence binomnk k! = n^underlinek, the quotient n!/(k!(n-k)!) is a natural number, and binomnk = binomnn-k Theorem
- For all m and n there is a list of mn pairwise distinct reals with no strictly increasing sublist of length m+1 and no strictly decreasing sublist of length n+1 Theorem
- If | A| > k| B| then every f : A → B has a fibre with more than k elements, and for nonempty B some fibre has at least lceil | A| / | B|rceil elements Theorem
- ℕ × ℕ ≈ ℕ Theorem
- The integers form a commutative ring Theorem
- The integers form a totally ordered ring Theorem
- The multinomial coefficient equals n!/∏_i<m kᵢ!, and (x₀+…+xₘ₋₁)ⁿ = ∑ ιbinomnk∏_i<m xᵢ^kᵢ in ℝ Theorem
- The product rule: | A × B| = | A| | B|, and |∏_i<m Aᵢ| = ∏_i<m| Aᵢ| Theorem
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 23 results over 12 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
- T. Tao, Analysis I, 3rd ed., §2.1-2.3 (Peano axioms, recursion, arithmetic) (standard reference, not scraped)
- Peano axioms (Wikipedia) (standard reference, not scraped)
- W. Aitken, MATH 378 Ch. 1: The Peano Axioms (CSU San Marcos) (standard reference, not scraped)