The unsorry worklist: theorems that are already proven but not yet in mathlib, vetted for absence and stated in Lean, waiting for an agent or a human to prove them. Claim one, open a PR, let the gates decide (see Running an agent and ADR-012).
324 open · 425 proved · 752 total prove-goals.
| Goal | Status | Diff | Upstream | Source | Reference |
|---|---|---|---|---|---|
abstract-regular-polyhedron-realizable-iff — The Track-1 existence-biconditional: for p, q ≥ 3, the pair (p,q) is a Platonic Schläfli pair {(3,3),(3,4),(4,3),(3,5),(5,3)} iff it is realizable by an abstract regular polyhedron (∃ V E F > 0 with p·F=2E, q·V=2E, V+F=E+2). |
open | 4 | — | The capstone of Freek #50’s combinatorial classification (ADR-031, Track 1) — the labelled combinatorial/Euler form, explicitly NOT the geometric #50. | ⟹ is the existence direction (platonic-pairs-realizable); ⟸ is the proved classification (abstract-regular-polyhedron-classification). Composing them gives the biconditional. mathlib has neither. |
alt-sum-range-choose-sq-eq-zero-odd — For odd n, the alternating sum of (-1)^k times the square of n-choose-k vanishes. |
open | 3 | — | #400 Identity Engine (ADR-043) — binomial family; promoted from candidate backlog (#610). | For odd n, the alternating sum of (-1)^k times the square of n-choose-k vanishes. Not a named mathlib lemma in this form. |
alt-sum-range-sq-eq-signed-pronic — Twice the alternating sum of the first n+1 squares equals (-1)^n times the n-th pronic number n(n+1). |
open | 2 | — | #400 Identity Engine (ADR-043) — closed-form sum family; promoted from candidate backlog. | Twice the alternating sum of the first n+1 squares equals (-1)^n times the n-th pronic number n(n+1). Not a named mathlib lemma in this form. |
alt-sum-range-two-k-add-one-eq-signed-n — The alternating sum of the odd numbers (2k+1) over k below n equals (-1)^(n+1) times n. |
open | 2 | — | #400 Identity Engine (ADR-043) — binomial family; promoted from candidate backlog (#610). | The alternating sum of the odd numbers (2k+1) over k below n equals (-1)^(n+1) times n. Not a named mathlib lemma in this form. |
alternating-sum-k-mul-choose-eq-zero — For n at least 2 the alternating sum of k·C(n,k) over k is zero. |
open | 4 | — | #400 Identity Engine (ADR-043) — binomial family; promoted from candidate backlog (#610). | For n at least 2 the alternating sum of k·C(n,k) over k is zero. Not a named mathlib lemma in this form. |
alternating-sum-shifted-choose-eq-one — The alternating sum of the shifted binomial coefficients C(n+1,k+1) equals 1. |
open | 4 | — | #400 Identity Engine (ADR-043) — binomial family; promoted from candidate backlog (#610). | The alternating sum of the shifted binomial coefficients C(n+1,k+1) equals 1. Not a named mathlib lemma in this form. |
am-gm-three-cube — For nonneg reals, 27abc ≤ (a+b+c)³ — AM-GM for three terms (polynomial form). |
open | 3 | — | Classic elementary real inequality (#400 plan Phase 3 — library growth). | For nonneg reals, 27abc ≤ (a+b+c)³ — AM-GM for three terms (polynomial form). Not a named mathlib lemma in this concrete polynomial/abs form. |
am-hm-two-var — For positive reals a,b, 4/(a+b) ≤ 1/a + 1/b — the two-variable AM–HM inequality. |
open | 2 | — | Classic elementary inequality / number-theory fact (#400 plan Phase 3 — library growth). | For positive reals a,b, 4/(a+b) ≤ 1/a + 1/b — the two-variable AM–HM inequality. Not a named mathlib lemma in this concrete form. |
cassini-nat-fib-int — Over the integers, fib n times fib(n+2) minus fib(n+1) squared equals (-1)^(n+1) (a Cassini-form identity for Nat.fib). |
open | 4 | — | #400 Identity Engine (ADR-043) — Fibonacci/Lucas family; promoted from candidate backlog (#610). | Over the integers, fib n times fib(n+2) minus fib(n+1) squared equals (-1)^(n+1) (a Cassini-form identity for Nat.fib). Not a named mathlib lemma in this form. |
catalan-r2-int-fib — Catalan’s identity at offset 2: fib(n)² − fib(n−2)·fib(n+2) = (−1)^n. |
open | 2 | — | #400 Identity Engine (ADR-043) — Fibonacci/Lucas family; promoted from candidate backlog. | Catalan’s identity at offset 2: fib(n)² − fib(n−2)·fib(n+2) = (−1)^n. Not a named mathlib lemma in this form. |
catalan-r2-shift-nat-fib-int — Over the integers, the square of fib(n+2) minus fib(n) times fib(n+4) equals (-1)^n, a Catalan identity at offset two shifted to stay in the naturals. |
open | 3 | — | #400 Identity Engine (ADR-043) — Fibonacci/Lucas family; promoted from candidate backlog (#610). | Over the integers, the square of fib(n+2) minus fib(n) times fib(n+4) equals (-1)^n, a Catalan identity at offset two shifted to stay in the naturals. Not a named mathlib lemma in this form. |
catalan-r3-shift-nat-fib-int — Over the integers, the square of fib(n+3) minus fib(n) times fib(n+6) equals four times (-1)^n, a Catalan identity at offset three. |
open | 3 | — | #400 Identity Engine (ADR-043) — Fibonacci/Lucas family; promoted from candidate backlog (#610). | Over the integers, the square of fib(n+3) minus fib(n) times fib(n+6) equals four times (-1)^n, a Catalan identity at offset three. Not a named mathlib lemma in this form. |
cauchy-schwarz-three-var-product — The three-variable Cauchy-Schwarz inequality in product form. |
open | 2 | — | #400 Identity Engine (ADR-043) — inequality (SOS) family; promoted from candidate backlog. | The three-variable Cauchy-Schwarz inequality in product form. Not a named mathlib lemma in this form. |
consecutive-fib-product-diff-nat-int — Over the integers, fib n times fib(n+3) minus fib(n+1) times fib(n+2) equals (-1)^(n+1). |
open | 4 | — | #400 Identity Engine (ADR-043) — Fibonacci/Lucas family; promoted from candidate backlog (#610). | Over the integers, fib n times fib(n+3) minus fib(n+1) times fib(n+2) equals (-1)^(n+1). Not a named mathlib lemma in this form. |
cyclic-cube-sum-ge-asym-quad-cubic — For nonnegative reals the sum of cubes dominates the cyclic sum a^2 b + b^2 c + c^2 a. |
open | 2 | — | #400 Identity Engine (ADR-043) — inequality (SOS) family; promoted from candidate backlog. | For nonnegative reals the sum of cubes dominates the cyclic sum a^2 b + b^2 c + c^2 a. Not a named mathlib lemma in this form. |
cyclotomic-five-divides-pow-five-sub-one — The 5th cyclotomic polynomial n⁴+n³+n²+n+1 divides n⁵-1. |
open | 2 | — | #400 Identity Engine (ADR-043) — algebraic identity family; promoted from candidate backlog (#610). | The 5th cyclotomic polynomial n⁴+n³+n²+n+1 divides n⁵-1. Not a named mathlib lemma in this form. |
cyclotomic-three-divides-pow-six-sub-one — The polynomial n²+n+1 divides n⁶-1. |
open | 2 | — | #400 Identity Engine (ADR-043) — algebraic identity family; promoted from candidate backlog (#610). | The polynomial n²+n+1 divides n⁶-1. Not a named mathlib lemma in this form. |
diff-tetrahedral-eq-triangular — The difference of two consecutive tetrahedral numbers equals the intervening triangular number. |
open | 2 | — | #400 Identity Engine (ADR-043) — figurate-number family; promoted from candidate backlog (#610). | The difference of two consecutive tetrahedral numbers equals the intervening triangular number. Not a named mathlib lemma in this form. |
dvd-120-pow-eleven-sub-pow-three — 120 divides n^11 minus n^3 for every integer n. |
open | 3 | — | #400 Identity Engine (ADR-043) — divisibility family; promoted from candidate backlog (#610). | 120 divides n^11 minus n^3 for every integer n. Not a named mathlib lemma in this form. |
dvd-1302-pow-thirtyone-sub-self — The integer 1302 = 2·3·7·31 divides n^31 - n for every integer n. |
open | 3 | — | #400 Identity Engine (ADR-043) — divisibility family; promoted from candidate backlog (#610). | The integer 1302 = 2·3·7·31 divides n^31 - n for every integer n. Not a named mathlib lemma in this form. |
dvd-133-pow-nineteen-sub-self — The integer 133 = 7·19 divides n^19 - n for every integer n. |
open | 2 | — | #400 Identity Engine (ADR-043) — divisibility family; promoted from candidate backlog (#610). | The integer 133 = 7·19 divides n^19 - n for every integer n. Not a named mathlib lemma in this form. |
dvd-1365-pow-fifteen-sub-pow-three — The integer 1365 = 3·5·7·13 divides n^15 - n^3 for every integer n. |
open | 3 | — | #400 Identity Engine (ADR-043) — divisibility family; promoted from candidate backlog (#610). | The integer 1365 = 3·5·7·13 divides n^15 - n^3 for every integer n. Not a named mathlib lemma in this form. |
dvd-138-pow-twentythree-sub-self — 138 divides n^23 - n for every integer n. |
open | 3 | — | #400 Identity Engine (ADR-043) — divisibility family; promoted from candidate backlog. | 138 divides n^23 - n for every integer n. Not a named mathlib lemma in this form. |
dvd-170-pow-seventeen-sub-self — For every integer n, 170 divides n raised to the 17th power minus n. |
open | 3 | — | #400 Identity Engine (ADR-043) — divisibility family; promoted from candidate backlog (#610). | For every integer n, 170 divides n raised to the 17th power minus n. Not a named mathlib lemma in this form. |
dvd-1806-pow-fortythree-sub-self — For every integer n, 1806 divides n raised to the 43rd power minus n. |
open | 3 | — | #400 Identity Engine (ADR-043) — divisibility family; promoted from candidate backlog (#610). | For every integer n, 1806 divides n raised to the 43rd power minus n. Not a named mathlib lemma in this form. |
dvd-210-pow-fifteen-sub-pow-three — The integer 210 = 2·3·5·7 divides n^15 - n^3 for every integer n. |
open | 2 | — | #400 Identity Engine (ADR-043) — divisibility family; promoted from candidate backlog (#610). | The integer 210 = 2·3·5·7 divides n^15 - n^3 for every integer n. Not a named mathlib lemma in this form. |
dvd-240-pow-nine-sub-pow-five — 240 divides n^9 minus n^5 for every integer n. |
open | 3 | — | #400 Identity Engine (ADR-043) — divisibility family; promoted from candidate backlog (#610). | 240 divides n^9 minus n^5 for every integer n. Not a named mathlib lemma in this form. |
dvd-252-pow-eight-sub-sq — 252 divides n^8 minus n^2 for every integer n. |
open | 3 | — | #400 Identity Engine (ADR-043) — divisibility family; promoted from candidate backlog (#610). | 252 divides n^8 minus n^2 for every integer n. Not a named mathlib lemma in this form. |
dvd-255-pow-seventeen-sub-self — For every integer n, 255 divides n raised to the 17th power minus n. |
open | 3 | — | #400 Identity Engine (ADR-043) — divisibility family; promoted from candidate backlog (#610). | For every integer n, 255 divides n raised to the 17th power minus n. Not a named mathlib lemma in this form. |
dvd-266-pow-nineteen-sub-self — The integer 266 = 2·7·19 divides n^19 - n for every integer n. |
open | 2 | — | #400 Identity Engine (ADR-043) — divisibility family; promoted from candidate backlog (#610). | The integer 266 = 2·7·19 divides n^19 - n for every integer n. Not a named mathlib lemma in this form. |
dvd-273-pow-fourteen-sub-sq — The integer 273 = 3·7·13 divides n^14 - n^2 for every integer n. |
open | 2 | — | #400 Identity Engine (ADR-043) — divisibility family; promoted from candidate backlog (#610). | The integer 273 = 3·7·13 divides n^14 - n^2 for every integer n. Not a named mathlib lemma in this form. |
dvd-273-pow-thirteen-sub-self — The integer 273 = 3·7·13 divides n^13 - n for every integer n. |
open | 2 | — | #400 Identity Engine (ADR-043) — divisibility family; promoted from candidate backlog (#610). | The integer 273 = 3·7·13 divides n^13 - n for every integer n. Not a named mathlib lemma in this form. |
dvd-2730-pow-thirteen-sub-self — 2730 divides n^13 - n for every integer n. |
open | 4 | — | #400 Identity Engine (ADR-043) — divisibility family. | 2730 divides n^13 - n for every integer n. Not a named mathlib lemma in this form. |
dvd-330-pow-twentythree-sub-pow-three — For every integer n, 330 divides n to the 23rd power minus n to the 3rd power. |
open | 3 | — | #400 Identity Engine (ADR-043) — divisibility family; promoted from candidate backlog. | For every integer n, 330 divides n to the 23rd power minus n to the 3rd power. Not a named mathlib lemma in this form. |
dvd-360-pow-fifteen-sub-pow-three — The integer 360 = 2^3·3^2·5 divides n^15 - n^3 for every integer n. |
open | 3 | — | #400 Identity Engine (ADR-043) — divisibility family; promoted from candidate backlog (#610). | The integer 360 = 2^3·3^2·5 divides n^15 - n^3 for every integer n. Not a named mathlib lemma in this form. |
dvd-455-pow-fifteen-sub-pow-three — The integer 455 = 5·7·13 divides n^15 - n^3 for every integer n. |
open | 2 | — | #400 Identity Engine (ADR-043) — divisibility family; promoted from candidate backlog (#610). | The integer 455 = 5·7·13 divides n^15 - n^3 for every integer n. Not a named mathlib lemma in this form. |
dvd-504-pow-nine-sub-pow-three — 504 divides n^9 minus n^3 for every integer n. |
open | 3 | — | #400 Identity Engine (ADR-043) — divisibility family; promoted from candidate backlog (#610). | 504 divides n^9 minus n^3 for every integer n. Not a named mathlib lemma in this form. |
dvd-5040-seven-consecutive-product — 5040 (=7!) divides n·(n^2-1)·(n^2-4)·(n^2-9), the product of seven consecutive integers centred at n. |
open | 4 | — | #400 Identity Engine (ADR-043) — divisibility family; promoted from candidate backlog (#610). | 5040 (=7!) divides n·(n^2-1)·(n^2-4)·(n^2-9), the product of seven consecutive integers centred at n. Not a named mathlib lemma in this form. |
dvd-510-pow-fortynine-sub-pow-seventeen — 510 divides n^49 - n^17 for every integer n. |
open | 2 | — | #400 Identity Engine (ADR-043) — divisibility family; promoted from candidate backlog. | 510 divides n^49 - n^17 for every integer n. Not a named mathlib lemma in this form. |
dvd-510-pow-nineteen-sub-pow-three — For every integer n, 510 divides n to the 19th power minus n to the 3rd power. |
open | 2 | — | #400 Identity Engine (ADR-043) — divisibility family; promoted from candidate backlog. | For every integer n, 510 divides n to the 19th power minus n to the 3rd power. Not a named mathlib lemma in this form. |
dvd-510-pow-thirtythree-sub-pow-seventeen — For every integer n, 510 divides n to the 33rd power minus n to the 17th power. |
open | 3 | — | #400 Identity Engine (ADR-043) — divisibility family; promoted from candidate backlog (#610). | For every integer n, 510 divides n to the 33rd power minus n to the 17th power. Not a named mathlib lemma in this form. |
dvd-510-pow-twentyone-sub-pow-five — For every integer n, 510 divides n to the 21st power minus n to the 5th power. |
open | 3 | — | #400 Identity Engine (ADR-043) — divisibility family; promoted from candidate backlog (#610). | For every integer n, 510 divides n to the 21st power minus n to the 5th power. Not a named mathlib lemma in this form. |
dvd-546-pow-fourteen-sub-sq — The integer 546 = 2·3·7·13 divides n^14 - n^2 for every integer n. |
open | 2 | — | #400 Identity Engine (ADR-043) — divisibility family; promoted from candidate backlog (#610). | The integer 546 = 2·3·7·13 divides n^14 - n^2 for every integer n. Not a named mathlib lemma in this form. |
dvd-630-pow-fourteen-sub-sq — The integer 630 = 2·3^2·5·7 divides n^14 - n^2 for every integer n. |
open | 3 | — | #400 Identity Engine (ADR-043) — divisibility family; promoted from candidate backlog (#610). | The integer 630 = 2·3^2·5·7 divides n^14 - n^2 for every integer n. Not a named mathlib lemma in this form. |
dvd-66-pow-thirtyone-sub-pow-eleven — 66 divides n^31 - n^11 for every integer n. |
open | 3 | — | #400 Identity Engine (ADR-043) — divisibility family; promoted from candidate backlog. | 66 divides n^31 - n^11 for every integer n. Not a named mathlib lemma in this form. |
dvd-6765-pow-fortyone-sub-self — For every integer n, 6765 divides n raised to the 41st power minus n. |
open | 3 | — | #400 Identity Engine (ADR-043) — divisibility family; promoted from candidate backlog (#610). | For every integer n, 6765 divides n raised to the 41st power minus n. Not a named mathlib lemma in this form. |
dvd-840-pow-fifteen-sub-pow-three — The integer 840 = 2^3·3·5·7 divides n^15 - n^3 for every integer n. |
open | 3 | — | #400 Identity Engine (ADR-043) — divisibility family; promoted from candidate backlog (#610). | The integer 840 = 2^3·3·5·7 divides n^15 - n^3 for every integer n. Not a named mathlib lemma in this form. |
dvd-870-pow-twentynine-sub-self — 870 divides n^29 - n for every integer n. |
open | 3 | — | #400 Identity Engine (ADR-043) — divisibility family; promoted from candidate backlog. | 870 divides n^29 - n for every integer n. Not a named mathlib lemma in this form. |
dvd-903-pow-fortythree-sub-self — For every integer n, 903 divides n raised to the 43rd power minus n. |
open | 3 | — | #400 Identity Engine (ADR-043) — divisibility family; promoted from candidate backlog (#610). | For every integer n, 903 divides n raised to the 43rd power minus n. Not a named mathlib lemma in this form. |
dvd-910-pow-thirteen-sub-self — The integer 910 = 2·5·7·13 divides n^13 - n for every integer n. |
open | 2 | — | #400 Identity Engine (ADR-043) — divisibility family; promoted from candidate backlog (#610). | The integer 910 = 2·5·7·13 divides n^13 - n for every integer n. Not a named mathlib lemma in this form. |
dvd-910-pow-twentyfive-sub-pow-thirteen — For every integer n, 910 divides n to the 25th power minus n to the 13th power. |
open | 3 | — | #400 Identity Engine (ADR-043) — divisibility family; promoted from candidate backlog. | For every integer n, 910 divides n to the 25th power minus n to the 13th power. Not a named mathlib lemma in this form. |
dvd-fortyeight-coprime-six-pow-four-sub-one — For every integer n divisible by neither 2 nor 3, 48 divides n^4 minus 1. |
open | 4 | — | #400 Identity Engine (ADR-043) — divisibility family; promoted from candidate backlog (#610). | For every integer n divisible by neither 2 nor 3, 48 divides n^4 minus 1. Not a named mathlib lemma in this form. |
dvd-sixteen-odd-pow-four-sub-one — For every odd integer n, 16 divides n^4 minus 1. |
open | 3 | — | #400 Identity Engine (ADR-043) — divisibility family; promoted from candidate backlog (#610). | For every odd integer n, 16 divides n^4 minus 1. Not a named mathlib lemma in this form. |
dvd-thirtytwo-odd-pow-eight-sub-one — For every odd integer n, 32 divides n^8 minus 1. |
open | 3 | — | #400 Identity Engine (ADR-043) — divisibility family; promoted from candidate backlog (#610). | For every odd integer n, 32 divides n^8 minus 1. Not a named mathlib lemma in this form. |
eisenstein-norm-multiplicative — The set of Loeschian numbers x²+xy+y² (Eisenstein integer norms) is closed under multiplication. |
open | 2 | — | #400 Identity Engine (ADR-043) — algebraic identity family; promoted from candidate backlog. | The set of Loeschian numbers x²+xy+y² (Eisenstein integer norms) is closed under multiplication. Not a named mathlib lemma in this form. |
fib-add-five-eq-five-mul-fib-succ-add-three-mul-fib — fib(n+5) equals five times fib(n+1) plus three times fib n. |
open | 2 | — | #400 Identity Engine (ADR-043) — Fibonacci/Lucas family; promoted from candidate backlog (#610). | fib(n+5) equals five times fib(n+1) plus three times fib n. Not a named mathlib lemma in this form. |
fib-add-four-eq-three-mul-fib-add-two-sub-fib — fib(n+4) equals three times fib(n+2) minus fib n. |
open | 2 | — | #400 Identity Engine (ADR-043) — Fibonacci/Lucas family; promoted from candidate backlog (#610). | fib(n+4) equals three times fib(n+2) minus fib n. Not a named mathlib lemma in this form. |
fib-add-four-recurrence-nat — fib(n+4) + fib(n) = 3·fib(n+2), the second-order Fibonacci recurrence. |
open | 2 | — | #400 Identity Engine (ADR-043) — Fibonacci/Lucas family; promoted from candidate backlog (#610). | fib(n+4) + fib(n) = 3·fib(n+2), the second-order Fibonacci recurrence. Not a named mathlib lemma in this form. |
fib-add-six-eq-eight-mul-fib-succ-add-five-mul-fib — fib(n+6) equals eight times fib(n+1) plus five times fib n. |
open | 2 | — | #400 Identity Engine (ADR-043) — Fibonacci/Lucas family; promoted from candidate backlog (#610). | fib(n+6) equals eight times fib(n+1) plus five times fib n. Not a named mathlib lemma in this form. |
fib-add-three-eq-two-mul-fib-succ-add-fib — fib(n+3) equals twice fib(n+1) plus fib n. |
open | 2 | — | #400 Identity Engine (ADR-043) — Fibonacci/Lucas family; promoted from candidate backlog (#610). | fib(n+3) equals twice fib(n+1) plus fib n. Not a named mathlib lemma in this form. |
fib-add-two-sq-sub-fib-sq-eq-fib-two-mul-add-two — The difference of the squares fib(n+2)^2 - fib(n)^2 equals fib(2n+2). |
open | 3 | — | #400 Identity Engine (ADR-043) — Fibonacci/Lucas family; promoted from candidate backlog (#610). | The difference of the squares fib(n+2)^2 - fib(n)^2 equals fib(2n+2). Not a named mathlib lemma in this form. |
fib-consecutive-vieta-form-value — Consecutive Fibonacci numbers (Fₙ, Fₙ₊₁) satisfy the Markov/Vieta form x²−xy−y²=(−1)ⁿ. |
open | 2 | — | #400 Identity Engine (ADR-043) — Pell-equation family; promoted from candidate backlog. | Consecutive Fibonacci numbers (Fₙ, Fₙ₊₁) satisfy the Markov/Vieta form x²−xy−y²=(−1)ⁿ. Not a named mathlib lemma in this form. |
fib-prod-cross-shift-nat-int — Over the integers, fib(n+1) times fib(n+2) minus fib(n) times fib(n+3) equals (-1)^n. |
open | 3 | — | #400 Identity Engine (ADR-043) — Fibonacci/Lucas family; promoted from candidate backlog (#610). | Over the integers, fib(n+1) times fib(n+2) minus fib(n) times fib(n+3) equals (-1)^n. Not a named mathlib lemma in this form. |
fib-two-mul-eq-fib-mul-two-mul-fib-succ-sub-fib — The Fibonacci doubling identity in additive form: F(2n) + F(n)^2 equals F(n)·2F(n+1). |
open | 3 | — | #400 Identity Engine (ADR-043) — partition/generating-function family; promoted from candidate backlog (#610). | The Fibonacci doubling identity in additive form: F(2n) + F(n)^2 equals F(n)·2F(n+1). Not a named mathlib lemma in this form. |
fib-two-mul-sq-diff-int — fib(2n) = fib(n+1)² − fib(n−1)², a difference-of-squares doubling formula. |
open | 3 | — | #400 Identity Engine (ADR-043) — Fibonacci/Lucas family; promoted from candidate backlog (#610). | fib(2n) = fib(n+1)² − fib(n−1)², a difference-of-squares doubling formula. Not a named mathlib lemma in this form. |
five-var-qm-am — The square of a five-term sum is at most five times the sum of the five squares (QM-AM, five variables). |
open | 3 | — | #400 Identity Engine (ADR-043) — inequality (SOS) family; promoted from candidate backlog (#610). | The square of a five-term sum is at most five times the sum of the five squares (QM-AM, five variables). Not a named mathlib lemma in this form. |
fourth-power-mod-fortyone-mem — The fourth-power residues modulo the prime 41 are exactly {0,1,4,10,16,18,23,25,31,37,40}. |
open | 2 | — | #400 Identity Engine (ADR-043) — power-residue family; promoted from candidate backlog. | The fourth-power residues modulo the prime 41 are exactly {0,1,4,10,16,18,23,25,31,37,40}. Not a named mathlib lemma in this form. |
hexagonal-eq-triangular-odd-index — The n-th hexagonal number n(2n-1) equals the (2n-1)-th triangular number. |
open | 1 | — | #400 Identity Engine (ADR-043) — figurate-number family; promoted from candidate backlog (#610). | The n-th hexagonal number n(2n-1) equals the (2n-1)-th triangular number. Not a named mathlib lemma in this form. |
lcm-self-succ — The lcm of n and n+1 is their product n(n+1). |
open | 2 | — | #400 Identity Engine (ADR-043) — gcd-coprime family. | The lcm of n and n+1 is their product n(n+1). Not a named mathlib lemma in this form. |
lucas-succ-add-lucas-pred-eq-five-mul-fib — The sum of the Lucas numbers at n+2 and n equals five times fib(n+1) (stated with a +1 index shift to keep terms in Nat). |
open | 2 | — | #400 Identity Engine (ADR-043) — Fibonacci/Lucas family; promoted from candidate backlog. | The sum of the Lucas numbers at n+2 and n equals five times fib(n+1) (stated with a +1 index shift to keep terms in Nat). Not a named mathlib lemma in this form. |
n4-plus-one-factor-over-sqrt-shift — The Sophie-Germain-type factorisation gives that 2n²-2n+1 divides 4n⁴+1. |
open | 2 | — | #400 Identity Engine (ADR-043) — algebraic identity family; promoted from candidate backlog (#610). | The Sophie-Germain-type factorisation gives that 2n²-2n+1 divides 4n⁴+1. Not a named mathlib lemma in this form. |
nat-sq-lt-two-pow-s2 — nat-sq-lt-two-pow-s2 |
open | 1 | — | — | — |
nesbitt-inequality-s1 — nesbitt-inequality-s1 |
open | 1 | — | — | — |
nicomachus-sum-cubes-eq-sum-id-sq — The sum of the first n cubes equals the square of the sum of the first n naturals (Nicomachus’s theorem). |
open | 3 | — | #400 Identity Engine (ADR-043) — algebraic identity family; promoted from candidate backlog (#610). | The sum of the first n cubes equals the square of the sum of the first n naturals (Nicomachus’s theorem). Not a named mathlib lemma in this form. |
one-hundred-twenty-dvd-five-consecutive — 120 = 5! divides the product of any five consecutive integers. |
open | 3 | — | #400 Identity Engine (ADR-043) — divisibility family; extends twenty-four-dvd-four-consecutive. | The product of k consecutive integers is divisible by k!; here k=5, k!=120. Extends the accepted twenty-four-dvd-four-consecutive (4!∣4-consecutive). Not a named mathlib lemma in this form. |
platonic-pairs-realizable — Each of the five Platonic Schläfli pairs {(3,3),(3,4),(4,3),(3,5),(5,3)} is realizable by an abstract regular polyhedron: there exist V, E, F (>0) satisfying the two handshakes p·F=2E, q·V=2E and Euler V+F=E+2. |
open | 3 | — | The existence (⟸) direction of Freek #50’s combinatorial classification (ADR-031, Track 1). Complements the proved classification (⟹) abstract-regular-polyhedron-classification; together they are the Track-1 existence-biconditional. |
witnesses — tetra (3,3)→(4,6,4), octa (3,4)→(6,12,8), cube (4,3)→(8,12,6), icosa (3,5)→(12,30,20), dodeca (5,3)→(20,30,12). mathlib has no abstract-regular-polyhedron realizability lemma. |
pow-five-add-pow-five-ge-quartic-mul — For nonnegative a,b, a⁵+b⁵ ≥ a⁴b+ab⁴. |
open | 3 | — | #400 Identity Engine (ADR-043) — inequalities family. | For nonnegative a,b, a⁵+b⁵ ≥ a⁴b+ab⁴. Not a named mathlib lemma in this form. |
prime-pow-eight-mod-480 — For every prime p greater than 5, p^8 is congruent to 1 modulo 480. |
open | 4 | — | #400 Identity Engine (ADR-043) — divisibility family; promoted from candidate backlog (#610). | For every prime p greater than 5, p^8 is congruent to 1 modulo 480. Not a named mathlib lemma in this form. |
prime-pow-six-mod-504 — For every prime p greater than 7, p^6 is congruent to 1 modulo 504. |
open | 4 | — | #400 Identity Engine (ADR-043) — divisibility family; promoted from candidate backlog (#610). | For every prime p greater than 7, p^6 is congruent to 1 modulo 504. Not a named mathlib lemma in this form. |
prod-icc-k-mul-add-two-div-succ-sq-telescope — For n at least 1, the product of k(k+2)/(k+1)^2 for k from 1 to n equals (n+2)/(2(n+1)). |
open | 3 | — | #400 Identity Engine (ADR-043) — telescoping family; promoted from candidate backlog (#610). | For n at least 1, the product of k(k+2)/(k+1)^2 for k from 1 to n equals (n+2)/(2(n+1)). Not a named mathlib lemma in this form. |
prod-icc-k-mul-add-two-div-succ-sq-telescope-half — The product of k(k+2)/(k+1)^2 for k from 1 to n telescopes to (n+2)/(2(n+1)). |
open | 2 | — | #400 Identity Engine (ADR-043) — telescoping family; promoted from candidate backlog. | The product of k(k+2)/(k+1)^2 for k from 1 to n telescopes to (n+2)/(2(n+1)). Not a named mathlib lemma in this form. |
prod-icc-k-sq-div-pred-mul-succ-telescope — The product of k^2/((k-1)(k+1)) for k from 2 to n telescopes to 2n/(n+1). |
open | 2 | — | #400 Identity Engine (ADR-043) — telescoping family; promoted from candidate backlog. | The product of k^2/((k-1)(k+1)) for k from 2 to n telescopes to 2n/(n+1). Not a named mathlib lemma in this form. |
prod-icc-one-add-recip-eq-succ — The product of (2k+1)/(2k−1) for k from 1 to n equals 2n+1. |
open | 2 | — | #400 Identity Engine (ADR-043) — telescoping family; promoted from candidate backlog (#610). | The product of (2k+1)/(2k−1) for k from 1 to n equals 2n+1. Not a named mathlib lemma in this form. |
prod-icc-one-add-recip-k-sq-add-two-k-telescope — For n at least 1, the product of (1 + 1/(k^2+2k)) for k from 1 to n equals 2(n+1)/(n+2). |
open | 3 | — | #400 Identity Engine (ADR-043) — telescoping family; promoted from candidate backlog (#610). | For n at least 1, the product of (1 + 1/(k^2+2k)) for k from 1 to n equals 2(n+1)/(n+2). Not a named mathlib lemma in this form. |
prod-icc-one-add-recip-k-sq-sub-one-telescope — For n at least 2, the product of (1 + 1/(k^2-1)) for k from 2 to n equals 2n/(n+1). |
open | 3 | — | #400 Identity Engine (ADR-043) — telescoping family; promoted from candidate backlog (#610). | For n at least 2, the product of (1 + 1/(k^2-1)) for k from 2 to n equals 2n/(n+1). Not a named mathlib lemma in this form. |
prod-icc-one-add-recip-pronic — The product of (1 + 1/(k²+2k)) for k from 1 to n equals 2(n+1)/(n+2). |
open | 3 | — | #400 Identity Engine (ADR-043) — telescoping family; promoted from candidate backlog (#610). | The product of (1 + 1/(k²+2k)) for k from 1 to n equals 2(n+1)/(n+2). Not a named mathlib lemma in this form. |
prod-icc-one-sub-recip-sq-eq-frac — The product of (k²−1)/k² for k from 2 to n equals (n+1)/(2n). |
open | 2 | — | #400 Identity Engine (ADR-043) — telescoping family; promoted from candidate backlog (#610). | The product of (k²−1)/k² for k from 2 to n equals (n+1)/(2n). Not a named mathlib lemma in this form. |
prod-icc-one-sub-two-div-pronic — The product of (1 − 2/(k(k+1))) for k from 2 to n equals (n+2)/(3n). |
open | 3 | — | #400 Identity Engine (ADR-043) — telescoping family; promoted from candidate backlog (#610). | The product of (1 − 2/(k(k+1))) for k from 2 to n equals (n+2)/(3n). Not a named mathlib lemma in this form. |
prod-icc-succ-add-three-div-self-eq-binom-shift — The product of (k+3)/k for k from 1 to n telescopes to (n+1)(n+2)(n+3)/6. |
open | 2 | — | #400 Identity Engine (ADR-043) — telescoping family; promoted from candidate backlog. | The product of (k+3)/k for k from 1 to n telescopes to (n+1)(n+2)(n+3)/6. Not a named mathlib lemma in this form. |
prod-icc-succ-sq-div-k-mul-add-two-telescope — The product of (k+1)^2/(k(k+2)) for k from 1 to n telescopes to 2(n+1)/(n+2). |
open | 2 | — | #400 Identity Engine (ADR-043) — telescoping family; promoted from candidate backlog. | The product of (k+1)^2/(k(k+2)) for k from 1 to n telescopes to 2(n+1)/(n+2). Not a named mathlib lemma in this form. |
prod-one-sub-inv-sq-telescope — For n ≥ 2, ∏_{k=2}^{n} (1 − 1/k²) = (n+1)/(2n) over ℚ — the telescoping product of (1 − 1/k²). |
open | 4 | — | Classic telescoping product (Wallis-adjacent finite product) | ∏(1−1/k²) = (n+1)/(2n), via the factorisation 1 − 1/k² = (k−1)(k+1)/k². Distinct from the reciprocal-pronic / reciprocal-triangular SUM telescopes already in the pool (this is a multiplicative, rational telescope). |
prod-range-one-sub-recip-succ-sq — The product of (1 − 1/(k+1)²) for k from 1 to n equals (n+2)/(2(n+1)). |
open | 2 | — | #400 Identity Engine (ADR-043) — telescoping family; promoted from candidate backlog (#610). | The product of (1 − 1/(k+1)²) for k from 1 to n equals (n+2)/(2(n+1)). Not a named mathlib lemma in this form. |
quartic-n4-plus-four-composite — n⁴+4 factors explicitly as (n²-2n+2)(n²+2n+2), exhibiting both Sophie-Germain factors. |
open | 2 | — | #400 Identity Engine (ADR-043) — algebraic identity family; promoted from candidate backlog (#610). | n⁴+4 factors explicitly as (n²-2n+2)(n²+2n+2), exhibiting both Sophie-Germain factors. Not a named mathlib lemma in this form. |
quartic-n4-plus-four-not-prime — For n at least 2 the value n^4+4 is composite (special case of the Sophie Germain identity). |
open | 3 | — | #400 Identity Engine (ADR-043) — algebraic identity family; promoted from candidate backlog (#610). | For n at least 2 the value n^4+4 is composite (special case of the Sophie Germain identity). Not a named mathlib lemma in this form. |
quartic-plus-four-not-prime — For n≥2 the number n⁴+4 is composite (special Sophie Germain case b=1). |
open | 4 | — | #400 Identity Engine (ADR-043) — algebraic family. | For n≥2 the number n⁴+4 is composite (special Sophie Germain case b=1). Not a named mathlib lemma in this form. |
quartic-sum-ge-abc-times-sum — The sum of fourth powers of three reals dominates abc times their sum a+b+c. |
open | 2 | — | #400 Identity Engine (ADR-043) — inequality (SOS) family; promoted from candidate backlog. | The sum of fourth powers of three reals dominates abc times their sum a+b+c. Not a named mathlib lemma in this form. |
quartic-x4-plus-x2-plus-one-dvd-by-minus-factor — The Aurifeuillian quartic x^4+x^2+1 is divisible by the quadratic factor x^2-x+1. |
open | 2 | — | #400 Identity Engine (ADR-043) — algebraic identity family; promoted from candidate backlog (#610). | The Aurifeuillian quartic x^4+x^2+1 is divisible by the quadratic factor x^2-x+1. Not a named mathlib lemma in this form. |
realization-determines-counts — The face/edge/vertex counts of an abstract regular polyhedron are determined by (p,q): two realizations with the same (p,q) have equal V,E,F. |
open | 5 | — | Freek #50 combinatorial classification, Track-1 completion (ADR-031; #400 plan Phase 1). | The face/edge/vertex counts of an abstract regular polyhedron are determined by (p,q): two realizations with the same (p,q) have equal V,E,F. Not in mathlib (no abstract-regular-polyhedron theory). |
realization-edge-in-set — Any abstract regular polyhedron has E ∈ {6,12,30} (the only edge counts among the five Platonic solids). |
open | 4 | — | Freek #50 combinatorial classification, Track-1 completion (ADR-031; #400 plan Phase 1). | Any abstract regular polyhedron has E ∈ {6,12,30} (the only edge counts among the five Platonic solids). Not in mathlib (no abstract-regular-polyhedron theory). |
realization-edge-relation — For an abstract regular polyhedron, the handshakes + Euler give 2E(p+q) = pq(E+2). |
open | 2 | — | Freek #50 combinatorial classification, Track-1 completion (ADR-031; #400 plan Phase 1). | For an abstract regular polyhedron, the handshakes + Euler give 2E(p+q) = pq(E+2). Not in mathlib (no abstract-regular-polyhedron theory). |
sextic-x6-plus-x3-plus-one-composite-shift — The ninth cyclotomic polynomial n⁶+n³+1 divides n⁹-1. |
open | 2 | — | #400 Identity Engine (ADR-043) — algebraic identity family; promoted from candidate backlog (#610). | The ninth cyclotomic polynomial n⁶+n³+1 divides n⁹-1. Not a named mathlib lemma in this form. |
six-dvd-pow-three-add-five-mul — For every integer n, 6 ∣ n³ + 5n. |
open | 2 | — | #400 Identity Engine (ADR-043) — divisibility family. Classic elementary number theory. | 6 ∣ n³ + 5n, since n³ + 5n = (n³ − n) + 6n and 6 ∣ n³ − n. Not a named mathlib lemma in this form. |
sophie-germain-plus-factor-dvd — The second Sophie-Germain quadratic factor a^2+2ab+2b^2 divides a^4+4b^4. |
open | 2 | — | #400 Identity Engine (ADR-043) — algebraic identity family; promoted from candidate backlog (#610). | The second Sophie-Germain quadratic factor a^2+2ab+2b^2 divides a^4+4b^4. Not a named mathlib lemma in this form. |
sos-weighted-three-one-two — A weighted AM-GM cubic: 3a^2b is at most 2a^3 plus 2b^3 for nonnegative reals. |
open | 3 | — | #400 Identity Engine (ADR-043) — inequality (SOS) family; promoted from candidate backlog (#610). | A weighted AM-GM cubic: 3a^2b is at most 2a^3 plus 2b^3 for nonnegative reals. Not a named mathlib lemma in this form. |
sq-add-sq-eq-three-mul-sq-s4 — sq-add-sq-eq-three-mul-sq-s4 |
open | 1 | — | — | — |
sq-mod-five-ne-two-three — No natural number’s square leaves remainder 2 or 3 when divided by 5. |
open | 2 | — | #400 Identity Engine (ADR-043) — power-residue family; promoted from candidate backlog (#610). | No natural number’s square leaves remainder 2 or 3 when divided by 5. Not a named mathlib lemma in this form. |
sq-mod-ten-ne-two-three-seven-eight — No perfect square ends in the decimal digit 2, 3, 7, or 8. |
open | 2 | — | #400 Identity Engine (ADR-043) — power-residue family; promoted from candidate backlog (#610). | No perfect square ends in the decimal digit 2, 3, 7, or 8. Not a named mathlib lemma in this form. |
sum-centered-cube-eq-biquadratic — Twice the sum over k<n of k^3+(k+1)^3 equals n^2 times (n^2+1). |
open | 2 | — | #400 Identity Engine (ADR-043) — figurate-number family; promoted from candidate backlog (#610). | Twice the sum over k<n of k^3+(k+1)^3 equals n^2 times (n^2+1). Not a named mathlib lemma in this form. |
sum-centered-hexagonal-eq-cube — The sum of the first n centered hexagonal numbers equals n cubed. |
open | 2 | — | #400 Identity Engine (ADR-043) — figurate-number family; promoted from candidate backlog (#610). | The sum of the first n centered hexagonal numbers equals n cubed. Not a named mathlib lemma in this form. |
sum-centered-octahedral-closed-form — The running sum of three-times-centered-octahedral terms (2k+1)(2k^2+2k+3) equals n^2(n^2+2). |
open | 2 | — | #400 Identity Engine (ADR-043) — figurate-number family; promoted from candidate backlog. | The running sum of three-times-centered-octahedral terms (2k+1)(2k^2+2k+3) equals n^2(n^2+2). Not a named mathlib lemma in this form. |
sum-centered-square-numbers-closed-form — Three times the running sum of centered square numbers 2k(k+1)+1 equals n(2n^2+1). |
open | 2 | — | #400 Identity Engine (ADR-043) — figurate-number family; promoted from candidate backlog (#610). | Three times the running sum of centered square numbers 2k(k+1)+1 equals n(2n^2+1). Not a named mathlib lemma in this form. |
sum-centered-tetrahedral-closed-form — Twice the running sum of (2k+1)(k^2+k+3) equals n^2(n^2+5), a centered-tetrahedral closed form. |
open | 2 | — | #400 Identity Engine (ADR-043) — figurate-number family; promoted from candidate backlog. | Twice the running sum of (2k+1)(k^2+k+3) equals n^2(n^2+5), a centered-tetrahedral closed form. Not a named mathlib lemma in this form. |
sum-centered-triangular-closed-form — The sum of the first n centered triangular numbers equals n times (n^2+1). |
open | 2 | — | #400 Identity Engine (ADR-043) — figurate-number family; promoted from candidate backlog. | The sum of the first n centered triangular numbers equals n times (n^2+1). Not a named mathlib lemma in this form. |
sum-centered-triangular-running-closed-form — The running sum of twice-centered-triangular terms 3k^2+3k+2 equals n(n^2+1). |
open | 2 | — | #400 Identity Engine (ADR-043) — figurate-number family; promoted from candidate backlog (#610). | The running sum of twice-centered-triangular terms 3k^2+3k+2 equals n(n^2+1). Not a named mathlib lemma in this form. |
sum-cube-add-id-closed-form — Four times the sum of (k^3 + k) equals n(n+1)(n^2+n+2). |
open | 2 | — | #400 Identity Engine (ADR-043) — figurate-number family; promoted from candidate backlog (#610). | Four times the sum of (k^3 + k) equals n(n+1)(n^2+n+2). Not a named mathlib lemma in this form. |
sum-decagonal-closed-form — Six times the sum of the first n decagonal numbers equals n(n+1)(8n-5). |
open | 3 | — | #400 Identity Engine (ADR-043) — figurate-number family; promoted from candidate backlog (#610). | Six times the sum of the first n decagonal numbers equals n(n+1)(8n-5). Not a named mathlib lemma in this form. |
sum-decagonal-numbers-closed-form — Six times the running sum of the first n decagonal numbers k(4k-3) equals n(n+1)(8n-5). |
open | 2 | — | #400 Identity Engine (ADR-043) — figurate-number family; promoted from candidate backlog. | Six times the running sum of the first n decagonal numbers k(4k-3) equals n(n+1)(8n-5). Not a named mathlib lemma in this form. |
sum-decagonal-second-kind-closed-form — Three times the running sum of the second-kind decagonal terms k(5k+1) equals n(n+1)(5n+4). |
open | 2 | — | #400 Identity Engine (ADR-043) — figurate-number family; promoted from candidate backlog (#610). | Three times the running sum of the second-kind decagonal terms k(5k+1) equals n(n+1)(5n+4). Not a named mathlib lemma in this form. |
sum-even-cubes-eq-twice-square — The sum of the first n even cubes equals 2n^2(n+1)^2. |
open | 2 | — | #400 Identity Engine (ADR-043) — figurate-number family; promoted from candidate backlog (#610). | The sum of the first n even cubes equals 2n^2(n+1)^2. Not a named mathlib lemma in this form. |
sum-even-index-triangular-closed-form — Six times the sum of the even-index triangular numbers T_{2k}=k(2k+1) equals n(n+1)(4n+5). |
open | 2 | — | #400 Identity Engine (ADR-043) — figurate-number family; promoted from candidate backlog (#610). | Six times the sum of the even-index triangular numbers T_{2k}=k(2k+1) equals n(n+1)(4n+5). Not a named mathlib lemma in this form. |
sum-even-squares-faulhaber — Three times the sum of the first n even squares equals 2n(n+1)(2n+1). |
open | 2 | — | #400 Identity Engine (ADR-043) — figurate-number family; promoted from candidate backlog (#610). | Three times the sum of the first n even squares equals 2n(n+1)(2n+1). Not a named mathlib lemma in this form. |
sum-five-consecutive-product-closed-form — Six times the sum of five consecutive integer products equals the six-term product n through n+5, the 5-simplex closed form. |
open | 2 | — | #400 Identity Engine (ADR-043) — figurate-number family; promoted from candidate backlog (#610). | Six times the sum of five consecutive integer products equals the six-term product n through n+5, the 5-simplex closed form. Not a named mathlib lemma in this form. |
sum-four-consecutive-eq-hyper-tetrahedral — Five times the sum of products of four consecutive integers equals n(n+1)(n+2)(n+3)(n+4). |
open | 3 | — | #400 Identity Engine (ADR-043) — figurate-number family; promoted from candidate backlog. | Five times the sum of products of four consecutive integers equals n(n+1)(n+2)(n+3)(n+4). Not a named mathlib lemma in this form. |
sum-fourth-powers-eq — Thirty times the sum of fourth powers k^4 over range n equals the Faulhaber quartic closed form. |
open | 4 | — | #400 Identity Engine (ADR-043) — figurate family. | Thirty times the sum of fourth powers k^4 over range n equals the Faulhaber quartic closed form. Not a named mathlib lemma in this form. |
sum-fourth-powers-three-var-ge-sym-square-products — The sum of fourth powers of three reals dominates the symmetric sum of pairwise products of their squares. |
open | 2 | — | #400 Identity Engine (ADR-043) — algebraic identity family; promoted from candidate backlog (#610). | The sum of fourth powers of three reals dominates the symmetric sum of pairwise products of their squares. Not a named mathlib lemma in this form. |
sum-heptagonal-closed-form — Six times the sum of the first n heptagonal-gnomon terms equals 2n(n+1)(5n-2). |
open | 3 | — | #400 Identity Engine (ADR-043) — figurate-number family; promoted from candidate backlog (#610). | Six times the sum of the first n heptagonal-gnomon terms equals 2n(n+1)(5n-2). Not a named mathlib lemma in this form. |
sum-heptagonal-numbers-closed-form — Three times the sum of the first n heptagonal numbers (twice each, as k(5k-3)) equals n(n+1)(5n-2). |
open | 2 | — | #400 Identity Engine (ADR-043) — figurate-number family; promoted from candidate backlog (#610). | Three times the sum of the first n heptagonal numbers (twice each, as k(5k-3)) equals n(n+1)(5n-2). Not a named mathlib lemma in this form. |
sum-hexagonal-eq — Six times the sum of hexagonal-type terms k(2k-1) over range n equals (n-1)n(4n-5). |
open | 3 | — | #400 Identity Engine (ADR-043) — figurate family. | Six times the sum of hexagonal-type terms k(2k-1) over range n equals (n-1)n(4n-5). Not a named mathlib lemma in this form. |
sum-hexagonal-numbers-closed-form — Six times the sum of the first n hexagonal numbers equals n(n+1)(4n-1). |
open | 3 | — | #400 Identity Engine (ADR-043) — figurate-number family; promoted from candidate backlog (#610). | Six times the sum of the first n hexagonal numbers equals n(n+1)(4n-1). Not a named mathlib lemma in this form. |
sum-icc-choose-hockey-stick-s1 — sum-icc-choose-hockey-stick-s1 |
open | 1 | — | — | — |
sum-icc-choose-hockey-stick-s2 — sum-icc-choose-hockey-stick-s2 |
open | 1 | — | — | — |
sum-icc-choose-hockey-stick-s3 — sum-icc-choose-hockey-stick-s3 |
open | 1 | — | — | — |
sum-icc-cube-diff-recip-telescope — For n at least 1, the sum of (3k^2+3k+1)/(k^3(k+1)^3) for k from 1 to n equals 1 minus 1/(n+1)^3. |
open | 3 | — | #400 Identity Engine (ADR-043) — telescoping family; promoted from candidate backlog (#610). | For n at least 1, the sum of (3k^2+3k+1)/(k^3(k+1)^3) for k from 1 to n equals 1 minus 1/(n+1)^3. Not a named mathlib lemma in this form. |
sum-icc-eight-k-div-odd-sq-pair-telescope — The sum of 8k/((2k-1)^2(2k+1)^2) for k from 1 to n telescopes to 1 minus 1/(2n+1)^2. |
open | 2 | — | #400 Identity Engine (ADR-043) — telescoping family; promoted from candidate backlog. | The sum of 8k/((2k-1)^2(2k+1)^2) for k from 1 to n telescopes to 1 minus 1/(2n+1)^2. Not a named mathlib lemma in this form. |
sum-icc-five-k-sub-two-mul-three-pow-pred-closed — Four times the sum of (5k-2)3^(k-1) for k from 1 to n equals (10n-9)3^n + 9. |
open | 2 | — | #400 Identity Engine (ADR-043) — closed-form sum family; promoted from candidate backlog. | Four times the sum of (5k-2)3^(k-1) for k from 1 to n equals (10n-9)3^n + 9. Not a named mathlib lemma in this form. |
sum-icc-four-div-four-k-sub-one-four-k-add-three-telescope — The sum of 4/((4k-1)(4k+3)) for k from 1 to n telescopes to 1/3 minus 1/(4n+3). |
open | 2 | — | #400 Identity Engine (ADR-043) — telescoping family; promoted from candidate backlog (#610). | The sum of 4/((4k-1)(4k+3)) for k from 1 to n telescopes to 1/3 minus 1/(4n+3). Not a named mathlib lemma in this form. |
sum-icc-four-div-three-consec-odd-telescope — The sum of 4/((2k-1)(2k+1)(2k+3)) for k from 1 to n telescopes to 1/3 minus 1/((2n+1)(2n+3)). |
open | 2 | — | #400 Identity Engine (ADR-043) — telescoping family; promoted from candidate backlog. | The sum of 4/((2k-1)(2k+1)(2k+3)) for k from 1 to n telescopes to 1/3 minus 1/((2n+1)(2n+3)). Not a named mathlib lemma in this form. |
sum-icc-id-mul-two-pow-pred — The sum of k·2^(k−1) for k from 1 to n equals (n−1)·2^n + 1. |
open | 2 | — | #400 Identity Engine (ADR-043) — closed-form sum family; promoted from candidate backlog. | The sum of k·2^(k−1) for k from 1 to n equals (n−1)·2^n + 1. Not a named mathlib lemma in this form. |
sum-icc-k-div-three-shifted-consecutive-telescope — The sum of k/((k+1)(k+2)(k+3)) for k from 1 to n telescopes to 1/4 + 1/(2(n+2)) - 3/(2(n+3)). |
open | 3 | — | #400 Identity Engine (ADR-043) — telescoping family; promoted from candidate backlog. | The sum of k/((k+1)(k+2)(k+3)) for k from 1 to n telescopes to 1/4 + 1/(2(n+2)) - 3/(2(n+3)). Not a named mathlib lemma in this form. |
sum-icc-k-mul-three-k-add-one-eq — The sum of k(3k+1) for k from 1 to n, twice the negative-index generalized pentagonal numbers, equals n(n+1)². |
open | 3 | — | #400 Identity Engine (ADR-043) — partition/generating-function family; promoted from candidate backlog (#610). | The sum of k(3k+1) for k from 1 to n, twice the negative-index generalized pentagonal numbers, equals n(n+1)². Not a named mathlib lemma in this form. |
sum-icc-k-mul-three-k-sub-one-eq — The sum of k(3k-1) for k from 1 to n, twice the generalized pentagonal numbers, equals n²(n+1). |
open | 3 | — | #400 Identity Engine (ADR-043) — partition/generating-function family; promoted from candidate backlog (#610). | The sum of k(3k-1) for k from 1 to n, twice the generalized pentagonal numbers, equals n²(n+1). Not a named mathlib lemma in this form. |
sum-icc-k-mul-two-k-sub-one-closed-form — Six times the sum of k(2k-1) for k from 1 to n equals n(n+1)(4n-1). |
open | 2 | — | #400 Identity Engine (ADR-043) — closed-form sum family; promoted from candidate backlog (#610). | Six times the sum of k(2k-1) for k from 1 to n equals n(n+1)(4n-1). Not a named mathlib lemma in this form. |
sum-icc-k-sq-add-one-mul-factorial-eq-prod — The sum of (k^2+1)·k! for k from 1 to n equals n·(n+1)!. |
open | 3 | — | #400 Identity Engine (ADR-043) — telescoping family; promoted from candidate backlog (#610). | The sum of (k^2+1)·k! for k from 1 to n equals n·(n+1)!. Not a named mathlib lemma in this form. |
sum-icc-k-sq-add-one-mul-factorial-eq-pronic-factorial — The sum over k from 1 to n of (k^2+1)k! telescopes to n(n+1)!. |
open | 2 | — | #400 Identity Engine (ADR-043) — closed-form sum family; promoted from candidate backlog. | The sum over k from 1 to n of (k^2+1)k! telescopes to n(n+1)!. Not a named mathlib lemma in this form. |
sum-icc-k-sub-one-div-factorial-eq-one-sub — For n at least 1, the sum of (k-1)/k! for k from 1 to n equals 1 minus 1/n!. |
open | 3 | — | #400 Identity Engine (ADR-043) — telescoping family; promoted from candidate backlog (#610). | For n at least 1, the sum of (k-1)/k! for k from 1 to n equals 1 minus 1/n!. Not a named mathlib lemma in this form. |
sum-icc-recip-four-consecutive-product-telescope — The sum of 1/(k(k+1)(k+2)(k+3)) for k from 1 to n telescopes to 1/18 minus 1/(3(n+1)(n+2)(n+3)). |
open | 2 | — | #400 Identity Engine (ADR-043) — telescoping family; promoted from candidate backlog. | The sum of 1/(k(k+1)(k+2)(k+3)) for k from 1 to n telescopes to 1/18 minus 1/(3(n+1)(n+2)(n+3)). Not a named mathlib lemma in this form. |
sum-icc-recip-k-sq-sub-one-telescope — For n at least 2, the sum of 1/(k^2-1) for k from 2 to n equals 3/4 minus (2n+1)/(2n(n+1)). |
open | 3 | — | #400 Identity Engine (ADR-043) — telescoping family; promoted from candidate backlog (#610). | For n at least 2, the sum of 1/(k^2-1) for k from 2 to n equals 3/4 minus (2n+1)/(2n(n+1)). Not a named mathlib lemma in this form. |
sum-icc-recip-km1-k-kp1-telescope — For n at least 2, the sum of 1/((k-1)k(k+1)) for k from 2 to n equals 1/4 minus 1/(2n(n+1)). |
open | 3 | — | #400 Identity Engine (ADR-043) — telescoping family; promoted from candidate backlog (#610). | For n at least 2, the sum of 1/((k-1)k(k+1)) for k from 2 to n equals 1/4 minus 1/(2n(n+1)). Not a named mathlib lemma in this form. |
sum-icc-recip-step-four-pair-eq-n-div — The sum of 1/((4k-3)(4k+1)) for k from 1 to n telescopes to n/(4n+1). |
open | 2 | — | #400 Identity Engine (ADR-043) — closed-form sum family; promoted from candidate backlog. | The sum of 1/((4k-3)(4k+1)) for k from 1 to n telescopes to n/(4n+1). Not a named mathlib lemma in this form. |
sum-icc-three-div-three-k-sub-one-three-k-add-two-telescope — The sum of 3/((3k-1)(3k+2)) for k from 1 to n telescopes to 1/2 minus 1/(3n+2). |
open | 2 | — | #400 Identity Engine (ADR-043) — telescoping family; promoted from candidate backlog (#610). | The sum of 3/((3k-1)(3k+2)) for k from 1 to n telescopes to 1/2 minus 1/(3n+2). Not a named mathlib lemma in this form. |
sum-icc-three-k-add-two-div-triple-consecutive-telescope — The sum of (3k+2)/(k(k+1)(k+2)) for k from 1 to n telescopes to 2 minus 1/(n+1) minus 2/(n+2). |
open | 2 | — | #400 Identity Engine (ADR-043) — telescoping family; promoted from candidate backlog. | The sum of (3k+2)/(k(k+1)(k+2)) for k from 1 to n telescopes to 2 minus 1/(n+1) minus 2/(n+2). Not a named mathlib lemma in this form. |
sum-icc-three-k-sub-one-mul-two-pow-pred-closed — The sum of (3k-1)2^(k-1) for k from 1 to n equals (3n-4)2^n + 4. |
open | 2 | — | #400 Identity Engine (ADR-043) — closed-form sum family; promoted from candidate backlog. | The sum of (3k-1)2^(k-1) for k from 1 to n equals (3n-4)2^n + 4. Not a named mathlib lemma in this form. |
sum-icc-two-div-k-mul-k-add-two-telescope — The sum of 2/(k(k+2)) for k from 1 to n telescopes to 3/2 minus 1/(n+1) minus 1/(n+2). |
open | 2 | — | #400 Identity Engine (ADR-043) — telescoping family; promoted from candidate backlog (#610). | The sum of 2/(k(k+2)) for k from 1 to n telescopes to 3/2 minus 1/(n+1) minus 1/(n+2). Not a named mathlib lemma in this form. |
sum-icc-two-k-add-one-div-k-sq-succ-sq-telescope — The sum of (2k+1)/(k^2(k+1)^2) for k from 1 to n telescopes to 1 minus 1/(n+1)^2. |
open | 3 | — | #400 Identity Engine (ADR-043) — telescoping family; promoted from candidate backlog (#610). | The sum of (2k+1)/(k^2(k+1)^2) for k from 1 to n telescopes to 1 minus 1/(n+1)^2. Not a named mathlib lemma in this form. |
sum-id-mul-triangular-closed-form — Twenty-four times the sum of k times the k-th triangular number equals (n-1)n(n+1)(3n-2). |
open | 3 | — | #400 Identity Engine (ADR-043) — figurate-number family; promoted from candidate backlog (#610). | Twenty-four times the sum of k times the k-th triangular number equals (n-1)n(n+1)(3n-2). Not a named mathlib lemma in this form. |
sum-k-add-one-mul-two-pow — The sum over k<n of (k+1)·2^k equals (n−1)·2^n + 1. |
open | 2 | — | #400 Identity Engine (ADR-043) — closed-form-sums family. | The sum over k<n of (k+1)·2^k equals (n−1)·2^n + 1. Not a named mathlib lemma in this form. |
sum-k-mul-k-add-two-closed-form — Six times the sum of k(k+2) over k up to n equals n(n+1)(2n+7). |
open | 2 | — | #400 Identity Engine (ADR-043) — figurate-number family; promoted from candidate backlog (#610). | Six times the sum of k(k+2) over k up to n equals n(n+1)(2n+7). Not a named mathlib lemma in this form. |
sum-k-mul-succ-mul-two-k-succ — Twice the sum of k(k+1)(2k+1) over k up to n equals n(n+1)^2(n+2). |
open | 3 | — | #400 Identity Engine (ADR-043) — figurate-number family; promoted from candidate backlog (#610). | Twice the sum of k(k+1)(2k+1) over k up to n equals n(n+1)^2(n+2). Not a named mathlib lemma in this form. |
sum-k-mul-succ-sq-closed-form — Twelve times the sum of k(k+1)^2 equals n(n+1)(n+2)(3n+5). |
open | 2 | — | #400 Identity Engine (ADR-043) — figurate-number family; promoted from candidate backlog (#610). | Twelve times the sum of k(k+1)^2 equals n(n+1)(n+2)(3n+5). Not a named mathlib lemma in this form. |
sum-k-sq-mul-succ-closed-form — Twelve times the sum of k^2(k+1) over k up to n equals n(n+1)(n+2)(3n+1). |
open | 2 | — | #400 Identity Engine (ADR-043) — figurate-number family; promoted from candidate backlog (#610). | Twelve times the sum of k^2(k+1) over k up to n equals n(n+1)(n+2)(3n+1). Not a named mathlib lemma in this form. |
sum-k-sq-mul-two-pow — The sum over k<n of k²·2^k equals (n²−4n+6)·2^n − 6. |
open | 3 | — | #400 Identity Engine (ADR-043) — closed-form-sums family. | The sum over k<n of k²·2^k equals (n²−4n+6)·2^n − 6. Not a named mathlib lemma in this form. |
sum-nonagonal-closed-form — Three times the sum of the first n nonagonal-gnomon terms equals n(n+1)(7n-4). |
open | 3 | — | #400 Identity Engine (ADR-043) — figurate-number family; promoted from candidate backlog (#610). | Three times the sum of the first n nonagonal-gnomon terms equals n(n+1)(7n-4). Not a named mathlib lemma in this form. |
sum-nonagonal-numbers-closed-form — Three times the running sum of the first n nonagonal numbers (as k(7k-5)) equals n(n+1)(7n-4). |
open | 2 | — | #400 Identity Engine (ADR-043) — figurate-number family; promoted from candidate backlog (#610). | Three times the running sum of the first n nonagonal numbers (as k(7k-5)) equals n(n+1)(7n-4). Not a named mathlib lemma in this form. |
sum-oblong-eq — Three times the sum of the first n oblong (pronic) numbers k(k+1) equals (n-1)n(n+1). |
open | 2 | — | #400 Identity Engine (ADR-043) — figurate family. | Three times the sum of the first n oblong (pronic) numbers k(k+1) equals (n-1)n(n+1). Not a named mathlib lemma in this form. |
sum-octagonal-eq — Twice the sum of octagonal-type terms k(3k-2) over range n equals (n-1)n(2n-3). |
open | 3 | — | #400 Identity Engine (ADR-043) — figurate family. | Twice the sum of octagonal-type terms k(3k-2) over range n equals (n-1)n(2n-3). Not a named mathlib lemma in this form. |
sum-octagonal-numbers-closed-form — Twice the running sum of the first n octagonal numbers k(3k-2) equals n(n+1)(2n-1). |
open | 2 | — | #400 Identity Engine (ADR-043) — figurate-number family; promoted from candidate backlog. | Twice the running sum of the first n octagonal numbers k(3k-2) equals n(n+1)(2n-1). Not a named mathlib lemma in this form. |
sum-octagonal-running-closed-form — Twice the running sum of the first n octagonal numbers k(3k-2) equals n(n+1)(2n-1). |
open | 3 | — | #400 Identity Engine (ADR-043) — figurate-number family; promoted from candidate backlog (#610). | Twice the running sum of the first n octagonal numbers k(3k-2) equals n(n+1)(2n-1). Not a named mathlib lemma in this form. |
sum-octahedral-centered-squares — Three times the sum of the first n centered-square numbers is n times (2n^2+1), the octahedral closed form. |
open | 2 | — | #400 Identity Engine (ADR-043) — figurate-number family; promoted from candidate backlog. | Three times the sum of the first n centered-square numbers is n times (2n^2+1), the octahedral closed form. Not a named mathlib lemma in this form. |
sum-octahedral-numbers-closed-form — Six times the sum of the first n octahedral numbers equals 3n(n+1)(n^2+n+1). |
open | 2 | — | #400 Identity Engine (ADR-043) — figurate-number family; promoted from candidate backlog (#610). | Six times the sum of the first n octahedral numbers equals 3n(n+1)(n^2+n+1). Not a named mathlib lemma in this form. |
sum-odd-gnomon-squares-closed-form — Twice the sum of (3k-2)^2 over k up to n equals n(6n^2-3n-1). |
open | 3 | — | #400 Identity Engine (ADR-043) — figurate-number family; promoted from candidate backlog (#610). | Twice the sum of (3k-2)^2 over k up to n equals n(6n^2-3n-1). Not a named mathlib lemma in this form. |
sum-odd-squares-eq — Three times the sum of the first n odd squares (2k+1)^2 equals n(2n-1)(2n+1). |
open | 3 | — | #400 Identity Engine (ADR-043) — figurate family. | Three times the sum of the first n odd squares (2k+1)^2 equals n(2n-1)(2n+1). Not a named mathlib lemma in this form. |
sum-odd-squares-faulhaber — Three times the sum of the first n odd squares equals n(2n-1)(2n+1). |
open | 2 | — | #400 Identity Engine (ADR-043) — figurate-number family; promoted from candidate backlog (#610). | Three times the sum of the first n odd squares equals n(2n-1)(2n+1). Not a named mathlib lemma in this form. |
sum-one-div-four-k-plus-one-mul-four-k-plus-five — The sum over k<n of 1/((4k+1)(4k+5)) equals n/(4n+1). |
open | 3 | — | #400 Identity Engine (ADR-043) — telescoping family. | The sum over k<n of 1/((4k+1)(4k+5)) equals n/(4n+1). Not a named mathlib lemma in this form. |
sum-one-div-succ-mul-add-four-telescope — The sum over k<n of 3/((k+1)(k+4)) telescopes to 11/6 − 1/(n+1) − 1/(n+2) − 1/(n+3). |
open | 4 | — | #400 Identity Engine (ADR-043) — telescoping family. | The sum over k<n of 3/((k+1)(k+4)) telescopes to 11/6 − 1/(n+1) − 1/(n+2) − 1/(n+3). Not a named mathlib lemma in this form. |
sum-one-div-three-k-plus-one-mul-three-k-plus-four — The sum over k<n of 1/((3k+1)(3k+4)) equals n/(3n+1). |
open | 3 | — | #400 Identity Engine (ADR-043) — telescoping family. | The sum over k<n of 1/((3k+1)(3k+4)) equals n/(3n+1). Not a named mathlib lemma in this form. |
sum-pentagonal-eq — The sum of generalized pentagonal-type terms k(3k-1) over range n equals (n-1)^2·n. |
open | 3 | — | #400 Identity Engine (ADR-043) — figurate family. | The sum of generalized pentagonal-type terms k(3k-1) over range n equals (n-1)^2·n. Not a named mathlib lemma in this form. |
sum-pentagonal-pyramidal-closed-form — Twelve times the sum of k^2(k+1) (twice the pentagonal-pyramidal terms) equals n(n+1)(3n+1)(n+2). |
open | 3 | — | #400 Identity Engine (ADR-043) — figurate-number family; promoted from candidate backlog (#610). | Twelve times the sum of k^2(k+1) (twice the pentagonal-pyramidal terms) equals n(n+1)(3n+1)(n+2). Not a named mathlib lemma in this form. |
sum-pentagonal-running-eq-pyramidal — Twice the running sum of the first n pentagonal numbers k(3k-1)/2 equals the pentagonal-pyramidal number n^2(n+1). |
open | 3 | — | #400 Identity Engine (ADR-043) — figurate-number family; promoted from candidate backlog (#610). | Twice the running sum of the first n pentagonal numbers k(3k-1)/2 equals the pentagonal-pyramidal number n^2(n+1). Not a named mathlib lemma in this form. |
sum-pentatope-triple-product — Four times the sum of three consecutive integer products equals n(n+1)(n+2)(n+3), the pentatope closed form. |
open | 2 | — | #400 Identity Engine (ADR-043) — figurate-number family; promoted from candidate backlog (#610). | Four times the sum of three consecutive integer products equals n(n+1)(n+2)(n+3), the pentatope closed form. Not a named mathlib lemma in this form. |
sum-product-consecutive-odds-closed-form — Three times the sum of products of consecutive odd numbers (2k-1)(2k+1) equals n(4n^2+6n-1). |
open | 2 | — | #400 Identity Engine (ADR-043) — figurate-number family; promoted from candidate backlog (#610). | Three times the sum of products of consecutive odd numbers (2k-1)(2k+1) equals n(4n^2+6n-1). Not a named mathlib lemma in this form. |
sum-pronic-eq-thrice-tetrahedral — Three times the sum of the first n pronic numbers k(k+1) equals (n-1)n(n+1). |
open | 2 | — | #400 Identity Engine (ADR-043) — figurate-number family; promoted from candidate backlog (#610). | Three times the sum of the first n pronic numbers k(k+1) equals (n-1)n(n+1). Not a named mathlib lemma in this form. |
sum-quadruple-product-closed-form — Five times the sum of four consecutive integer products equals the five-term product n through n+4. |
open | 2 | — | #400 Identity Engine (ADR-043) — figurate-number family; promoted from candidate backlog (#610). | Five times the sum of four consecutive integer products equals the five-term product n through n+4. Not a named mathlib lemma in this form. |
sum-quintic-gnomon-eq-fifth-power — The sum over k<n of the quintic gnomon equals n to the fifth. |
open | 2 | — | #400 Identity Engine (ADR-043) — figurate-number family; promoted from candidate backlog (#610). | The sum over k<n of the quintic gnomon equals n to the fifth. Not a named mathlib lemma in this form. |
sum-range-catalan-mul-catalan-eq-catalan-succ — The Catalan numbers satisfy the convolution recurrence: the self-convolution of the first n+1 Catalan numbers gives C(n+1). |
open | 3 | — | #400 Identity Engine (ADR-043) — partition/generating-function family; promoted from candidate backlog. | The Catalan numbers satisfy the convolution recurrence: the self-convolution of the first n+1 Catalan numbers gives C(n+1). Not a named mathlib lemma in this form. |
sum-range-choose-mul-choose-three-eq — Eight times the subset-of-a-subset sum of C(n,k)·C(k,3) equals C(n,3)·2^n. |
open | 4 | — | #400 Identity Engine (ADR-043) — binomial family; promoted from candidate backlog (#610). | Eight times the subset-of-a-subset sum of C(n,k)·C(k,3) equals C(n,3)·2^n. Not a named mathlib lemma in this form. |
sum-range-choose-mul-k-mul-comp-eq — Four times the sum of C(n,k)·k·(n-k) equals n(n-1)·2^n. |
open | 4 | — | #400 Identity Engine (ADR-043) — binomial family; promoted from candidate backlog (#610). | Four times the sum of C(n,k)·k·(n-k) equals n(n-1)·2^n. Not a named mathlib lemma in this form. |
sum-range-choose-mul-succ-choose-eq — The cross-row Vandermonde diagonal summing C(n,k) times C(n+1,k) equals C(2n+1,n). |
open | 3 | — | #400 Identity Engine (ADR-043) — binomial family; promoted from candidate backlog (#610). | The cross-row Vandermonde diagonal summing C(n,k) times C(n+1,k) equals C(2n+1,n). Not a named mathlib lemma in this form. |
sum-range-choose-mul-succ-choose-succ-eq-central-shift — The sum of n-choose-k times (n+1)-choose-(k+1) equals C(2n+1, n+1). |
open | 3 | — | #400 Identity Engine (ADR-043) — binomial family; promoted from candidate backlog (#610). | The sum of n-choose-k times (n+1)-choose-(k+1) equals C(2n+1, n+1). Not a named mathlib lemma in this form. |
sum-range-choose-sq-eq-central — ∑_{k=0}^{n} C(n,k)² = C(2n,n) — the central-binomial Vandermonde identity. |
open | 4 | — | Classic combinatorial / finite-sum identity (library-growth batch, #400 plan Phase 3). | ∑_{k=0}^{n} C(n,k)² = C(2n,n) — the central-binomial Vandermonde identity. Not a named mathlib lemma (Vandermonde/Pascal are present but not these specific closed forms). |
sum-range-comp-mul-choose-sq-eq — Over the integers the sum of (m-k) times C(m,k) squared, with m = n+1, equals m times C(2m,m) minus m times C(2m-1,m-1). |
open | 3 | — | #400 Identity Engine (ADR-043) — binomial family; promoted from candidate backlog (#610). | Over the integers the sum of (m-k) times C(m,k) squared, with m = n+1, equals m times C(2m,m) minus m times C(2m-1,m-1). Not a named mathlib lemma in this form. |
sum-range-compositions-count-eq-two-pow — Summing the number of compositions of n+1 into k parts (binom(n, k-1)) over all part counts gives 2^n, the total number of compositions. |
open | 3 | — | #400 Identity Engine (ADR-043) — partition/generating-function family; promoted from candidate backlog (#610). | Summing the number of compositions of n+1 into k parts (binom(n, k-1)) over all part counts gives 2^n, the total number of compositions. Not a named mathlib lemma in this form. |
sum-range-cube-diff-eq-cube — The sum of (3k²+3k+1) for k from 0 to n-1 equals n³. |
open | 2 | — | #400 Identity Engine (ADR-043) — telescoping family; promoted from candidate backlog. | The sum of (3k²+3k+1) for k from 0 to n-1 equals n³. Not a named mathlib lemma in this form. |
sum-range-cube-mul-three-pow-closed — Eight times the sum of k-cubed times three-to-the-k over k below n equals (4n^3-18n^2+36n-33)3^n+33. |
open | 3 | — | #400 Identity Engine (ADR-043) — binomial family; promoted from candidate backlog (#610). | Eight times the sum of k-cubed times three-to-the-k over k below n equals (4n^3-18n^2+36n-33)3^n+33. Not a named mathlib lemma in this form. |
sum-range-cube-mul-two-pow-closed — The sum of k-cubed times two-to-the-k over k below n has the closed form (n^3-6n^2+18n-26)2^n+26. |
open | 3 | — | #400 Identity Engine (ADR-043) — binomial family; promoted from candidate backlog (#610). | The sum of k-cubed times two-to-the-k over k below n has the closed form (n^3-6n^2+18n-26)2^n+26. Not a named mathlib lemma in this form. |
sum-range-cube-sym-choose-sq-eq-zero — The sum of (n-2k)^3·C(n,k)^2 over k vanishes by the antisymmetry k to n-k. |
open | 4 | — | #400 Identity Engine (ADR-043) — binomial family; promoted from candidate backlog (#610). | The sum of (n-2k)^3·C(n,k)^2 over k vanishes by the antisymmetry k to n-k. Not a named mathlib lemma in this form. |
sum-range-disp-mul-choose-eq-zero — Over the integers the mean-centered sum of (2k-n) times C(n,k) vanishes. |
open | 2 | — | #400 Identity Engine (ADR-043) — binomial family; promoted from candidate backlog (#610). | Over the integers the mean-centered sum of (2k-n) times C(n,k) vanishes. Not a named mathlib lemma in this form. |
sum-range-disp-mul-choose-sq-eq-zero — Over the integers the sum of (n-2k) times C(n,k) squared vanishes by the reflection symmetry k to n-k. |
open | 3 | — | #400 Identity Engine (ADR-043) — binomial family; promoted from candidate backlog (#610). | Over the integers the sum of (n-2k) times C(n,k) squared vanishes by the reflection symmetry k to n-k. Not a named mathlib lemma in this form. |
sum-range-even-cols-eq-two-pow — The sum of the even-indexed entries of row 2n of Pascal’s triangle equals 2^(2n-1). |
open | 4 | — | #400 Identity Engine (ADR-043) — binomial family; promoted from candidate backlog (#610). | The sum of the even-indexed entries of row 2n of Pascal’s triangle equals 2^(2n-1). Not a named mathlib lemma in this form. |
sum-range-fall-three-mul-choose — The sum over k of the third falling factorial of k times C(n,k), scaled by 8, equals n(n-1)(n-2) times 2^n. |
open | 4 | — | #400 Identity Engine (ADR-043) — binomial family; promoted from candidate backlog (#610). | The sum over k of the third falling factorial of k times C(n,k), scaled by 8, equals n(n-1)(n-2) times 2^n. Not a named mathlib lemma in this form. |
sum-range-fib-mul-two-pow-rev-eq — The generating-function-weighted sum of Fibonacci numbers ∑ F(k)·2^(n-k) plus F(n+3) equals 2^(n+1). |
open | 3 | — | #400 Identity Engine (ADR-043) — partition/generating-function family; promoted from candidate backlog (#610). | The generating-function-weighted sum of Fibonacci numbers ∑ F(k)·2^(n-k) plus F(n+3) equals 2^(n+1). Not a named mathlib lemma in this form. |
sum-range-fib-prod-shift-even-nat — The sum of fib(i)·fib(i+1) over the first 2n indices equals fib(2n)². |
open | 3 | — | #400 Identity Engine (ADR-043) — Fibonacci/Lucas family; promoted from candidate backlog (#610). | The sum of fib(i)·fib(i+1) over the first 2n indices equals fib(2n)². Not a named mathlib lemma in this form. |
sum-range-fib-sq-eq-fib-mul-fib-succ — The sum of the squares of the first n positive-index Fibonacci numbers equals the product of fib n and fib (n+1). |
open | 3 | — | #400 Identity Engine (ADR-043) — Fibonacci/Lucas family; promoted from candidate backlog (#610). | The sum of the squares of the first n positive-index Fibonacci numbers equals the product of fib n and fib (n+1). Not a named mathlib lemma in this form. |
sum-range-fib-sq-eq-prod — The sum of the squares of Fib(i) for i from 0 to n equals Fib(n)·Fib(n+1). |
open | 3 | — | #400 Identity Engine (ADR-043) — closed-form sum family; promoted from candidate backlog (#610). | The sum of the squares of Fib(i) for i from 0 to n equals Fib(n)·Fib(n+1). Not a named mathlib lemma in this form. |
sum-range-fib-sq-mul-two-eq — Twice the running sum of squared Fibonacci numbers relates the telescoping products F(n)F(n+1) and F(n+1)F(n+2) minus F(n+1)². |
open | 3 | — | #400 Identity Engine (ADR-043) — partition/generating-function family; promoted from candidate backlog (#610). | Twice the running sum of squared Fibonacci numbers relates the telescoping products F(n)F(n+1) and F(n+1)F(n+2) minus F(n+1)². Not a named mathlib lemma in this form. |
sum-range-fib-two-mul-succ-eq-fib-pred — The sum of the even-positive-index Fibonacci numbers fib 2, fib 4, …, fib (2n) equals fib(2n+1) minus one. |
open | 3 | — | #400 Identity Engine (ADR-043) — Fibonacci/Lucas family; promoted from candidate backlog (#610). | The sum of the even-positive-index Fibonacci numbers fib 2, fib 4, …, fib (2n) equals fib(2n+1) minus one. Not a named mathlib lemma in this form. |
sum-range-four-consecutive-product — Five times the sum of i(i+1)(i+2)(i+3) over i below n equals (n−1)n(n+1)(n+2)(n+3). |
open | 3 | — | #400 Identity Engine (ADR-043) — closed-form sum family; promoted from candidate backlog (#610). | Five times the sum of i(i+1)(i+2)(i+3) over i below n equals (n−1)n(n+1)(n+2)(n+3). Not a named mathlib lemma in this form. |
sum-range-four-cube-diff-eq — The sum of (4k³+6k²+4k+1) for k from 0 to n-1 equals n⁴. |
open | 2 | — | #400 Identity Engine (ADR-043) — telescoping family; promoted from candidate backlog (#610). | The sum of (4k³+6k²+4k+1) for k from 0 to n-1 equals n⁴. Not a named mathlib lemma in this form. |
sum-range-four-mul-add-one — The sum of 4k+1 over k below n equals n·(2n−1), the n-th centered-square-style count. |
open | 2 | — | #400 Identity Engine (ADR-043) — closed-form sum family; promoted from candidate backlog (#610). | The sum of 4k+1 over k below n equals n·(2n−1), the n-th centered-square-style count. Not a named mathlib lemma in this form. |
sum-range-half-even-row-choose-eq — Twice the sum of the first n+1 entries of the even row 2n of Pascal’s triangle equals 4 to the n plus the central coefficient C(2n,n). |
open | 3 | — | #400 Identity Engine (ADR-043) — binomial family; promoted from candidate backlog (#610). | Twice the sum of the first n+1 entries of the even row 2n of Pascal’s triangle equals 4 to the n plus the central coefficient C(2n,n). Not a named mathlib lemma in this form. |
sum-range-id-div-two-pow — The sum of i/2^i for i from 0 to n equals 2 − (n+2)/2^n. |
open | 3 | — | #400 Identity Engine (ADR-043) — closed-form sum family; promoted from candidate backlog (#610). | The sum of i/2^i for i from 0 to n equals 2 − (n+2)/2^n. Not a named mathlib lemma in this form. |
sum-range-id-div-two-pow-eq-two-sub — The sum of k over two-to-the-k for k below n equals two minus (2n+2)/2^n. |
open | 3 | — | #400 Identity Engine (ADR-043) — binomial family; promoted from candidate backlog (#610). | The sum of k over two-to-the-k for k below n equals two minus (2n+2)/2^n. Not a named mathlib lemma in this form. |
sum-range-id-mul-add-two — Six times the sum of i·(i+2) over i below n equals n·(n−1)·(2n+5). |
open | 3 | — | #400 Identity Engine (ADR-043) — closed-form sum family; promoted from candidate backlog (#610). | Six times the sum of i·(i+2) over i below n equals n·(n−1)·(2n+5). Not a named mathlib lemma in this form. |
sum-range-id-mul-choose-eq-half — Twice the sum over k of k times n-choose-k equals n times two-to-the-n. |
open | 3 | — | #400 Identity Engine (ADR-043) — binomial family; promoted from candidate backlog (#610). | Twice the sum over k of k times n-choose-k equals n times two-to-the-n. Not a named mathlib lemma in this form. |
sum-range-id-mul-four-pow-closed — Nine times the sum of k times four-to-the-k over k below n equals (3n-4)4^n+4. |
open | 2 | — | #400 Identity Engine (ADR-043) — binomial family; promoted from candidate backlog (#610). | Nine times the sum of k times four-to-the-k over k below n equals (3n-4)4^n+4. Not a named mathlib lemma in this form. |
sum-range-id-mul-neg-two-pow-closed — Nine times the sum of k times negative-two-to-the-k over k below n equals (2n-3)(-2)^n-2. |
open | 2 | — | #400 Identity Engine (ADR-043) — binomial family; promoted from candidate backlog. | Nine times the sum of k times negative-two-to-the-k over k below n equals (2n-3)(-2)^n-2. Not a named mathlib lemma in this form. |
sum-range-id-mul-succ-mul-two-pow-closed — The sum of k(k+1) times two-to-the-k over k below n equals (n^2-3n+4)2^n-4. |
open | 3 | — | #400 Identity Engine (ADR-043) — binomial family; promoted from candidate backlog (#610). | The sum of k(k+1) times two-to-the-k over k below n equals (n^2-3n+4)2^n-4. Not a named mathlib lemma in this form. |
sum-range-id-mul-three-pow — Four times the sum of i·3^i over i below n, plus 3^(n+1), equals 2n·3^n + 3. |
open | 3 | — | #400 Identity Engine (ADR-043) — closed-form sum family; promoted from candidate backlog (#610). | Four times the sum of i·3^i over i below n, plus 3^(n+1), equals 2n·3^n + 3. Not a named mathlib lemma in this form. |
sum-range-id-mul-three-pow-closed — Four times the sum of k times three-to-the-k over k below n equals (2n-3)3^n+3. |
open | 2 | — | #400 Identity Engine (ADR-043) — binomial family; promoted from candidate backlog (#610). | Four times the sum of k times three-to-the-k over k below n equals (2n-3)3^n+3. Not a named mathlib lemma in this form. |
sum-range-k-div-succ-factorial-eq — The rational sum of k/(k+1)! for k from 0 to n-1 equals 1 − 1/n!. |
open | 3 | — | #400 Identity Engine (ADR-043) — telescoping family; promoted from candidate backlog (#610). | The rational sum of k/(k+1)! for k from 0 to n-1 equals 1 − 1/n!. Not a named mathlib lemma in this form. |
sum-range-k-div-succ-factorial-telescope — The sum of k/(k+1)! over the first n terms equals 1 minus 1/n!. |
open | 3 | — | #400 Identity Engine (ADR-043) — telescoping family; promoted from candidate backlog (#610). | The sum of k/(k+1)! over the first n terms equals 1 minus 1/n!. Not a named mathlib lemma in this form. |
sum-range-k-mul-choose-mul-four-pow-closed — Five times the sum of k times n-choose-k times four-to-the-k equals four-n times five-to-the-n. |
open | 3 | — | #400 Identity Engine (ADR-043) — binomial family; promoted from candidate backlog (#610). | Five times the sum of k times n-choose-k times four-to-the-k equals four-n times five-to-the-n. Not a named mathlib lemma in this form. |
sum-range-k-mul-choose-mul-three-pow-closed — Four times the sum of k times n-choose-k times three-to-the-k equals three-n times four-to-the-n. |
open | 3 | — | #400 Identity Engine (ADR-043) — binomial family; promoted from candidate backlog (#610). | Four times the sum of k times n-choose-k times three-to-the-k equals three-n times four-to-the-n. Not a named mathlib lemma in this form. |
sum-range-k-mul-choose-mul-two-pow-eq-two-n-three-pow — Three times the sum of k times n-choose-k times two-to-the-k equals two-n times three-to-the-n. |
open | 3 | — | #400 Identity Engine (ADR-043) — binomial family; promoted from candidate backlog (#610). | Three times the sum of k times n-choose-k times two-to-the-k equals two-n times three-to-the-n. Not a named mathlib lemma in this form. |
sum-range-k-mul-choose-sq-eq-central — The sum of k·C(n,k)^2 equals n times the binomial coefficient C(2n-1,n-1). |
open | 4 | — | #400 Identity Engine (ADR-043) — binomial family; promoted from candidate backlog (#610). | The sum of k·C(n,k)^2 equals n times the binomial coefficient C(2n-1,n-1). Not a named mathlib lemma in this form. |
sum-range-k-mul-factorial-eq-factorial-succ-sub-one — The sum of k·k! for k up to n telescopes to (n+1)! - 1. |
open | 3 | — | #400 Identity Engine (ADR-043) — partition/generating-function family; promoted from candidate backlog (#610). | The sum of k·k! for k up to n telescopes to (n+1)! - 1. Not a named mathlib lemma in this form. |
sum-range-k-mul-factorial-succ — One plus the sum of k times k-factorial over k below n equals n-factorial. |
open | 3 | — | #400 Identity Engine (ADR-043) — algebraic identity family; promoted from candidate backlog (#610). | One plus the sum of k times k-factorial over k below n equals n-factorial. Not a named mathlib lemma in this form. |
sum-range-k-mul-two-pow-eq — The sum of k·2^k for k from 0 to n-1 equals (n−2)·2ⁿ + 2. |
open | 2 | — | #400 Identity Engine (ADR-043) — telescoping family; promoted from candidate backlog. | The sum of k·2^k for k from 0 to n-1 equals (n−2)·2ⁿ + 2. Not a named mathlib lemma in this form. |
sum-range-k-plus-one-mul-choose — Twice the sum of (k+1)·C(n,k) over k equals (n+2)·2^n. |
open | 3 | — | #400 Identity Engine (ADR-043) — binomial family; promoted from candidate backlog (#610). | Twice the sum of (k+1)·C(n,k) over k equals (n+2)·2^n. Not a named mathlib lemma in this form. |
sum-range-k-sq-mul-choose-eq — Four times the sum of k squared times C(n,k) over k equals n(n+1) times 2 to the n. |
open | 3 | — | #400 Identity Engine (ADR-043) — binomial family; promoted from candidate backlog (#610). | Four times the sum of k squared times C(n,k) over k equals n(n+1) times 2 to the n. Not a named mathlib lemma in this form. |
sum-range-k-sq-mul-five-pow-closed — The weighted sum of k squared times five to the k over the first n terms has a closed form scaled by 32. |
open | 2 | — | #400 Identity Engine (ADR-043) — closed-form sum family; promoted from candidate backlog. | The weighted sum of k squared times five to the k over the first n terms has a closed form scaled by 32. Not a named mathlib lemma in this form. |
sum-range-k-sq-mul-four-pow-closed — The weighted sum of k squared times four to the k over the first n terms has a closed form scaled by 27. |
open | 2 | — | #400 Identity Engine (ADR-043) — closed-form sum family; promoted from candidate backlog. | The weighted sum of k squared times four to the k over the first n terms has a closed form scaled by 27. Not a named mathlib lemma in this form. |
sum-range-k-sub-one-div-factorial-telescope — Reserved-shape variant: a factorial telescope whose summand (k-1)/(k+1)! collapses to a boundary term. |
open | 2 | — | #400 Identity Engine (ADR-043) — telescoping family; promoted from candidate backlog. | Reserved-shape variant: a factorial telescope whose summand (k-1)/(k+1)! collapses to a boundary term. Not a named mathlib lemma in this form. |
sum-range-lower-triangle-choose-eq-two-pow — The double sum of C(j,k) over the lower-triangular index region with j up to n equals 2 to the (n+1) minus 1. |
open | 3 | — | #400 Identity Engine (ADR-043) — binomial family; promoted from candidate backlog (#610). | The double sum of C(j,k) over the lower-triangular index region with j up to n equals 2 to the (n+1) minus 1. Not a named mathlib lemma in this form. |
sum-range-lucas-shift-nat — The sum of L(i+1)=fib(i)+fib(i+2) over the first n indices equals fib(n+1)+fib(n+3)−3. |
open | 3 | — | #400 Identity Engine (ADR-043) — Fibonacci/Lucas family; promoted from candidate backlog (#610). | The sum of L(i+1)=fib(i)+fib(i+2) over the first n indices equals fib(n+1)+fib(n+3)−3. Not a named mathlib lemma in this form. |
sum-range-multichoose-two-eq-choose-succ-two — Summing the size-j multiset counts from a two-element set over j up to m gives the triangular number C(m+2, 2). |
open | 2 | — | #400 Identity Engine (ADR-043) — partition/generating-function family; promoted from candidate backlog (#610). | Summing the size-j multiset counts from a two-element set over j up to m gives the triangular number C(m+2, 2). Not a named mathlib lemma in this form. |
sum-range-odd-cubes — ∑_{k=0}^{n-1} (2k+1)³ = n²(2n²−1) — the closed form for the sum of the first n odd cubes. |
open | 3 | — | Classic combinatorial / finite-sum identity (library-growth batch, #400 plan Phase 3). | ∑_{k=0}^{n-1} (2k+1)³ = n²(2n²−1) — the closed form for the sum of the first n odd cubes. Not a named mathlib lemma (Vandermonde/Pascal are present but not these specific closed forms). |
sum-range-odd-div-two-pow — The sum of (2i+1)/2^i for i from 0 to n equals 6 − (2n+5)/2^n. |
open | 3 | — | #400 Identity Engine (ADR-043) — closed-form sum family; promoted from candidate backlog (#610). | The sum of (2i+1)/2^i for i from 0 to n equals 6 − (2n+5)/2^n. Not a named mathlib lemma in this form. |
sum-range-odd-index-choose-eq-two-pow — The sum of the odd-indexed entries of the even row 2(n+1) of Pascal’s triangle equals 2 to the (2n+1). |
open | 3 | — | #400 Identity Engine (ADR-043) — binomial family; promoted from candidate backlog (#610). | The sum of the odd-indexed entries of the even row 2(n+1) of Pascal’s triangle equals 2 to the (2n+1). Not a named mathlib lemma in this form. |
sum-range-odd-mul-three-pow — The sum of (2i+1)·3^i over i below n, plus 3^n, equals n·3^n + 1. |
open | 3 | — | #400 Identity Engine (ADR-043) — closed-form sum family; promoted from candidate backlog (#610). | The sum of (2i+1)·3^i over i below n, plus 3^n, equals n·3^n + 1. Not a named mathlib lemma in this form. |
sum-range-odd-num-sq-succ-sq-telescope — The sum of (2k+3)/((k+1)²(k+2)²) for k from 0 to n-1 equals 1 − 1/(n+1)². |
open | 3 | — | #400 Identity Engine (ADR-043) — telescoping family; promoted from candidate backlog (#610). | The sum of (2k+3)/((k+1)²(k+2)²) for k from 0 to n-1 equals 1 − 1/(n+1)². Not a named mathlib lemma in this form. |
sum-range-pascal-diagonal-eq-choose — The hockey-stick along a Pascal diagonal: the sum of C(m+k,k) for k from 0 to n equals C(m+n+1,n). |
open | 3 | — | #400 Identity Engine (ADR-043) — binomial family; promoted from candidate backlog (#610). | The hockey-stick along a Pascal diagonal: the sum of C(m+k,k) for k from 0 to n equals C(m+n+1,n). Not a named mathlib lemma in this form. |
sum-range-recip-choose-two-eq-two-n-div-succ — The sum of the reciprocals of the binomial coefficients C(k+2,2) telescopes to 2n/(n+1). |
open | 3 | — | #400 Identity Engine (ADR-043) — partition/generating-function family; promoted from candidate backlog (#610). | The sum of the reciprocals of the binomial coefficients C(k+2,2) telescopes to 2n/(n+1). Not a named mathlib lemma in this form. |
sum-range-recip-consecutive — The telescoping sum ∑_{k<n} 1/((k+1)(k+2)) equals n/(n+1) over ℚ. |
open | 3 | — | #400 Identity Engine (ADR-043) — telescoping-sum family. | Partial fractions 1/((k+1)(k+2)) = 1/(k+1) − 1/(k+2) telescope to n/(n+1). Not a named mathlib lemma. |
sum-range-recip-five-step-product — The sum of 1/((5k+2)(5k+7)) for k from 0 to n-1 equals n/(2(5n+2)). |
open | 3 | — | #400 Identity Engine (ADR-043) — telescoping family; promoted from candidate backlog (#610). | The sum of 1/((5k+2)(5k+7)) for k from 0 to n-1 equals n/(2(5n+2)). Not a named mathlib lemma in this form. |
sum-range-recip-five-step-residue-one — The sum of 5/((5k+1)(5k+6)) for k from 0 to n-1 telescopes to 1 minus 1/(5n+1). |
open | 2 | — | #400 Identity Engine (ADR-043) — telescoping family; promoted from candidate backlog (#610). | The sum of 5/((5k+1)(5k+6)) for k from 0 to n-1 telescopes to 1 minus 1/(5n+1). Not a named mathlib lemma in this form. |
sum-range-recip-four-consec-product — The sum of 1/((k+1)(k+2)(k+3)(k+4)) over the first n terms equals 1/18 minus 1/(3(n+1)(n+2)(n+3)). |
open | 3 | — | #400 Identity Engine (ADR-043) — telescoping family; promoted from candidate backlog (#610). | The sum of 1/((k+1)(k+2)(k+3)(k+4)) over the first n terms equals 1/18 minus 1/(3(n+1)(n+2)(n+3)). Not a named mathlib lemma in this form. |
sum-range-recip-four-step-product — The sum of 1/((4k+1)(4k+5)) for k from 0 to n-1 equals n/(4n+1). |
open | 2 | — | #400 Identity Engine (ADR-043) — telescoping family; promoted from candidate backlog (#610). | The sum of 1/((4k+1)(4k+5)) for k from 0 to n-1 equals n/(4n+1). Not a named mathlib lemma in this form. |
sum-range-recip-four-step-residue-one — The sum of 4/((4k+1)(4k+5)) for k from 0 to n-1 telescopes to 1 minus 1/(4n+1). |
open | 2 | — | #400 Identity Engine (ADR-043) — telescoping family; promoted from candidate backlog (#610). | The sum of 4/((4k+1)(4k+5)) for k from 0 to n-1 telescopes to 1 minus 1/(4n+1). Not a named mathlib lemma in this form. |
sum-range-recip-odd-consecutive — The telescoping sum of 1/((2k+1)(2k+3)) over k below n equals n/(2n+1). |
open | 2 | — | #400 Identity Engine (ADR-043) — closed-form sum family; promoted from candidate backlog. | The telescoping sum of 1/((2k+1)(2k+3)) over k below n equals n/(2n+1). Not a named mathlib lemma in this form. |
sum-range-recip-odd-pair-consecutive — The sum of 1/((2k+1)(2k+3)) for k from 0 to n-1 equals n/(2n+1). |
open | 2 | — | #400 Identity Engine (ADR-043) — telescoping family; promoted from candidate backlog (#610). | The sum of 1/((2k+1)(2k+3)) for k from 0 to n-1 equals n/(2n+1). Not a named mathlib lemma in this form. |
sum-range-recip-odd-pair-step-two-eq-n-div — The sum over k<n of 1/((2k+1)(2k+3)) telescopes to n/(2n+1). |
open | 2 | — | #400 Identity Engine (ADR-043) — closed-form sum family; promoted from candidate backlog. | The sum over k<n of 1/((2k+1)(2k+3)) telescopes to n/(2n+1). Not a named mathlib lemma in this form. |
sum-range-recip-odd-product — The telescoping sum ∑_{k<n} 1/((2k+1)(2k+3)) equals n/(2n+1) over ℚ. |
open | 3 | — | #400 Identity Engine (ADR-043) — telescoping-sum family. | Partial fractions 1/((2k+1)(2k+3)) = ½(1/(2k+1) − 1/(2k+3)) telescope to n/(2n+1). Not a named mathlib lemma. |
sum-range-recip-shift-two-shift-five-telescope — The sum of 3/((k+2)(k+5)) for k from 0 to n-1 telescopes to 13/12 minus 1/(n+2)+1/(n+3)+1/(n+4). |
open | 3 | — | #400 Identity Engine (ADR-043) — telescoping family; promoted from candidate backlog (#610). | The sum of 3/((k+2)(k+5)) for k from 0 to n-1 telescopes to 13/12 minus 1/(n+2)+1/(n+3)+1/(n+4). Not a named mathlib lemma in this form. |
sum-range-recip-three-consec-odd-telescope — The sum of 1/((2k+1)(2k+3)(2k+5)) over the first n terms equals 1/12 minus 1/(4(2n+1)(2n+3)). |
open | 3 | — | #400 Identity Engine (ADR-043) — telescoping family; promoted from candidate backlog (#610). | The sum of 1/((2k+1)(2k+3)(2k+5)) over the first n terms equals 1/12 minus 1/(4(2n+1)(2n+3)). Not a named mathlib lemma in this form. |
sum-range-recip-three-consec-shifted — The sum of 1/((k+1)(k+2)(k+3)) over the first n terms equals n(n+3)/(4(n+1)(n+2)). |
open | 3 | — | #400 Identity Engine (ADR-043) — telescoping family; promoted from candidate backlog (#610). | The sum of 1/((k+1)(k+2)(k+3)) over the first n terms equals n(n+3)/(4(n+1)(n+2)). Not a named mathlib lemma in this form. |
sum-range-recip-three-consecutive — The telescoping sum of 1/((k+1)(k+2)(k+3)) over k below n equals 1/4 − 1/(2(n+1)(n+2)). |
open | 3 | — | #400 Identity Engine (ADR-043) — closed-form sum family; promoted from candidate backlog (#610). | The telescoping sum of 1/((k+1)(k+2)(k+3)) over k below n equals 1/4 − 1/(2(n+1)(n+2)). Not a named mathlib lemma in this form. |
sum-range-recip-three-step-residue-one — The sum of 3/((3k+1)(3k+4)) for k from 0 to n-1 telescopes to 1 minus 1/(3n+1). |
open | 2 | — | #400 Identity Engine (ADR-043) — telescoping family; promoted from candidate backlog (#610). | The sum of 3/((3k+1)(3k+4)) for k from 0 to n-1 telescopes to 1 minus 1/(3n+1). Not a named mathlib lemma in this form. |
sum-range-recip-triple-consecutive — The sum of 1/((k+1)(k+2)(k+3)) for k from 0 to n-1 equals 1/4 − 1/(2(n+1)(n+2)). |
open | 3 | — | #400 Identity Engine (ADR-043) — telescoping family; promoted from candidate backlog (#610). | The sum of 1/((k+1)(k+2)(k+3)) for k from 0 to n-1 equals 1/4 − 1/(2(n+1)(n+2)). Not a named mathlib lemma in this form. |
sum-range-recip-two-pow — The partial geometric sum of 1/2^i over i below n equals 2 − 2/2^n. |
open | 2 | — | #400 Identity Engine (ADR-043) — closed-form sum family; promoted from candidate backlog (#610). | The partial geometric sum of 1/2^i over i below n equals 2 − 2/2^n. Not a named mathlib lemma in this form. |
sum-range-shifted-choose-eq-two-pow-sub-one — The sum of the shifted binomial coefficients C(n+1,k+1) for k from 0 to n equals 2^(n+1) minus 1. |
open | 3 | — | #400 Identity Engine (ADR-043) — binomial family; promoted from candidate backlog (#610). | The sum of the shifted binomial coefficients C(n+1,k+1) for k from 0 to n equals 2^(n+1) minus 1. Not a named mathlib lemma in this form. |
sum-range-sq-add-one-mul-two-pow-closed — The sum of (k^2+1) times two-to-the-k over k below n equals (n^2-4n+7)2^n-7. |
open | 3 | — | #400 Identity Engine (ADR-043) — binomial family; promoted from candidate backlog (#610). | The sum of (k^2+1) times two-to-the-k over k below n equals (n^2-4n+7)2^n-7. Not a named mathlib lemma in this form. |
sum-range-sq-mul-four-pow-closed — Twenty-seven times the sum of k-squared times four-to-the-k over k below n equals (9n^2-24n+20)4^n-20. |
open | 3 | — | #400 Identity Engine (ADR-043) — binomial family; promoted from candidate backlog (#610). | Twenty-seven times the sum of k-squared times four-to-the-k over k below n equals (9n^2-24n+20)4^n-20. Not a named mathlib lemma in this form. |
sum-range-sq-mul-three-pow — Twice the sum of k^2·3^k over k below n, plus 3, equals 3^n·(n^2 − 3n + 3). |
open | 2 | — | #400 Identity Engine (ADR-043) — closed-form sum family; promoted from candidate backlog. | Twice the sum of k^2·3^k over k below n, plus 3, equals 3^n·(n^2 − 3n + 3). Not a named mathlib lemma in this form. |
sum-range-sq-mul-three-pow-closed — Twice the sum of k-squared times three-to-the-k over k below n equals (n^2-3n+3)3^n-3. |
open | 3 | — | #400 Identity Engine (ADR-043) — binomial family; promoted from candidate backlog (#610). | Twice the sum of k-squared times three-to-the-k over k below n equals (n^2-3n+3)3^n-3. Not a named mathlib lemma in this form. |
sum-range-sq-mul-two-pow — The sum of k^2·2^k over k below n, plus 6, equals 2^n·(n^2 − 4n + 6). |
open | 2 | — | #400 Identity Engine (ADR-043) — closed-form sum family; promoted from candidate backlog. | The sum of k^2·2^k over k below n, plus 6, equals 2^n·(n^2 − 4n + 6). Not a named mathlib lemma in this form. |
sum-range-stirling-first-row-eq-factorial — The sum of the unsigned Stirling numbers of the first kind across a full row equals n factorial, since every permutation of an n-set decomposes into some number of cycles. |
open | 3 | — | #400 Identity Engine (ADR-043) — partition/generating-function family; promoted from candidate backlog. | The sum of the unsigned Stirling numbers of the first kind across a full row equals n factorial, since every permutation of an n-set decomposes into some number of cycles. Not a named mathlib lemma in this form. |
sum-range-succ-div-factorial-add-two-telescope — The sum of (k+1)/(k+2)! over the first n terms equals 1 minus 1/(n+1)!. |
open | 3 | — | #400 Identity Engine (ADR-043) — telescoping family; promoted from candidate backlog (#610). | The sum of (k+1)/(k+2)! over the first n terms equals 1 minus 1/(n+1)!. Not a named mathlib lemma in this form. |
sum-range-succ-div-two-pow-eq-four-sub — The sum of (k+1) over two-to-the-k for k below n equals four minus (2n+4)/2^n. |
open | 3 | — | #400 Identity Engine (ADR-043) — binomial family; promoted from candidate backlog (#610). | The sum of (k+1) over two-to-the-k for k below n equals four minus (2n+4)/2^n. Not a named mathlib lemma in this form. |
sum-range-succ-k-mul-choose-mul-two-pow-closed — Three times the sum of (k+1) times n-choose-k times two-to-the-k equals (2n+3) times three-to-the-n. |
open | 3 | — | #400 Identity Engine (ADR-043) — binomial family; promoted from candidate backlog (#610). | Three times the sum of (k+1) times n-choose-k times two-to-the-k equals (2n+3) times three-to-the-n. Not a named mathlib lemma in this form. |
sum-range-succ-mul-choose-sq-eq — Twice the sum of (k+1) times C(n,k) squared equals (n+2) times the central coefficient C(2n,n). |
open | 3 | — | #400 Identity Engine (ADR-043) — binomial family; promoted from candidate backlog (#610). | Twice the sum of (k+1) times C(n,k) squared equals (n+2) times the central coefficient C(2n,n). Not a named mathlib lemma in this form. |
sum-range-succ-mul-factorial-eq — The sum over k from 0 to n-1 of (k+1)·(k+1)! equals (n+1)! − 1. |
open | 2 | — | #400 Identity Engine (ADR-043) — telescoping family; promoted from candidate backlog (#610). | The sum over k from 0 to n-1 of (k+1)·(k+1)! equals (n+1)! − 1. Not a named mathlib lemma in this form. |
sum-range-succ-mul-factorial-succ — The sum of (i+1)·(i+1)! over i below n, plus 1, telescopes to (n+1)!. |
open | 2 | — | #400 Identity Engine (ADR-043) — closed-form sum family; promoted from candidate backlog (#610). | The sum of (i+1)·(i+1)! over i below n, plus 1, telescopes to (n+1)!. Not a named mathlib lemma in this form. |
sum-range-succ-mul-two-pow-eq-closed — The derivative-of-geometric-series sum ∑ (k+1)·2^k from k=0 to n has closed form n·2^(n+1)+1. |
open | 2 | — | #400 Identity Engine (ADR-043) — partition/generating-function family; promoted from candidate backlog (#610). | The derivative-of-geometric-series sum ∑ (k+1)·2^k from k=0 to n has closed form n·2^(n+1)+1. Not a named mathlib lemma in this form. |
sum-range-succ-sq-mul-two-pow-closed — The sum of (k+1)-squared times two-to-the-k over k below n equals (n^2-2n+3)2^n-3. |
open | 3 | — | #400 Identity Engine (ADR-043) — binomial family; promoted from candidate backlog (#610). | The sum of (k+1)-squared times two-to-the-k over k below n equals (n^2-2n+3)2^n-3. Not a named mathlib lemma in this form. |
sum-range-three-k-add-two-mul-two-pow-closed — The sum of (3k+2) times two-to-the-k over k below n equals (3n-4)2^n+4. |
open | 2 | — | #400 Identity Engine (ADR-043) — binomial family; promoted from candidate backlog (#610). | The sum of (3k+2) times two-to-the-k over k below n equals (3n-4)2^n+4. Not a named mathlib lemma in this form. |
sum-range-three-mul-add-one — Twice the sum of 3k+1 over k below n equals n·(3n−1). |
open | 2 | — | #400 Identity Engine (ADR-043) — closed-form sum family; promoted from candidate backlog (#610). | Twice the sum of 3k+1 over k below n equals n·(3n−1). Not a named mathlib lemma in this form. |
sum-range-triangular-eq-tetrahedral — 6·∑_{k=0}^{n} k(k+1)/2 = n(n+1)(n+2) — sum of triangular numbers is tetrahedral. |
open | 3 | — | Classic combinatorial / finite-sum identity (library-growth batch, #400 plan Phase 3). | 6·∑_{k=0}^{n} k(k+1)/2 = n(n+1)(n+2) — sum of triangular numbers is tetrahedral. Not a named mathlib lemma (Vandermonde/Pascal are present but not these specific closed forms). |
sum-range-two-k-add-one-div-two-pow-closed — The sum of (2k+1)/2^k over the first n terms equals 6 minus (4n+6)/2^n. |
open | 3 | — | #400 Identity Engine (ADR-043) — telescoping family; promoted from candidate backlog (#610). | The sum of (2k+1)/2^k over the first n terms equals 6 minus (4n+6)/2^n. Not a named mathlib lemma in this form. |
sum-range-two-k-add-one-mul-two-pow-closed — The sum of (2k+1)·2^k for k up to n has the closed form (2n-1)·2^(n+1) + 3 over the integers. |
open | 3 | — | #400 Identity Engine (ADR-043) — partition/generating-function family; promoted from candidate backlog (#610). | The sum of (2k+1)·2^k for k up to n has the closed form (2n-1)·2^(n+1) + 3 over the integers. Not a named mathlib lemma in this form. |
sum-range-two-k-sub-n-mul-choose-sq-eq-zero — The weighted sum of (2k-n) times the square of n-choose-k vanishes. |
open | 3 | — | #400 Identity Engine (ADR-043) — binomial family; promoted from candidate backlog (#610). | The weighted sum of (2k-n) times the square of n-choose-k vanishes. Not a named mathlib lemma in this form. |
sum-range-two-k-sub-one-mul-three-pow-closed — The sum of (2k-1) times three-to-the-k over k below n has the clean closed form (n-2)3^n+2. |
open | 2 | — | #400 Identity Engine (ADR-043) — binomial family; promoted from candidate backlog (#610). | The sum of (2k-1) times three-to-the-k over k below n has the clean closed form (n-2)3^n+2. Not a named mathlib lemma in this form. |
sum-range-two-k-succ-mul-choose-eq — The sum of (2k+1) times C(n,k) over k equals (n+1) times 2 to the n. |
open | 2 | — | #400 Identity Engine (ADR-043) — binomial family; promoted from candidate backlog (#610). | The sum of (2k+1) times C(n,k) over k equals (n+1) times 2 to the n. Not a named mathlib lemma in this form. |
sum-range-two-mul-add-one — The sum of the first n odd numbers ∑_{k<n}(2k+1) equals n². |
open | 2 | — | #400 Identity Engine (ADR-043) — figurate family. | The sum of the first n odd numbers ∑_{k<n}(2k+1) equals n². Not a named mathlib lemma in this form. |
sum-range-vandermonde-self-eq-central-choose — The self-convolution of binomial coefficients of n at total degree r equals binom(2n, r), a Vandermonde/generating-function product identity. |
open | 3 | — | #400 Identity Engine (ADR-043) — partition/generating-function family; promoted from candidate backlog (#610). | The self-convolution of binomial coefficients of n at total degree r equals binom(2n, r), a Vandermonde/generating-function product identity. Not a named mathlib lemma in this form. |
sum-range-window-five-fib-eq-fib-diff-nat — The sum of five consecutive Fibonacci numbers starting at fib(n) equals fib(n+6) minus fib(n+1). |
open | 2 | — | #400 Identity Engine (ADR-043) — Fibonacci/Lucas family; promoted from candidate backlog (#610). | The sum of five consecutive Fibonacci numbers starting at fib(n) equals fib(n+6) minus fib(n+1). Not a named mathlib lemma in this form. |
sum-range-window-four-fib-eq-fib-diff-nat — The sum of four consecutive Fibonacci numbers starting at fib(n) equals fib(n+5) minus fib(n+1). |
open | 2 | — | #400 Identity Engine (ADR-043) — Fibonacci/Lucas family; promoted from candidate backlog (#610). | The sum of four consecutive Fibonacci numbers starting at fib(n) equals fib(n+5) minus fib(n+1). Not a named mathlib lemma in this form. |
sum-recip-times-sum-ge-nine — For positive reals, (a+b+c)(1/a+1/b+1/c) is at least 9 (Cauchy-Schwarz / AM-HM corollary). |
open | 3 | — | #400 Identity Engine (ADR-043) — inequality (SOS) family; promoted from candidate backlog (#610). | For positive reals, (a+b+c)(1/a+1/b+1/c) is at least 9 (Cauchy-Schwarz / AM-HM corollary). Not a named mathlib lemma in this form. |
sum-rhombic-dodecahedral-eq-fourth-power — The running sum of the rhombic-dodecahedral gnomons (2k-1)(2k^2-2k+1) equals n^4 exactly. |
open | 2 | — | #400 Identity Engine (ADR-043) — figurate-number family; promoted from candidate backlog. | The running sum of the rhombic-dodecahedral gnomons (2k-1)(2k^2-2k+1) equals n^4 exactly. Not a named mathlib lemma in this form. |
sum-sixth-ge-mixed-fourth-second — The sum of sixth powers dominates the mixed terms a⁴b²+a²b⁴. |
open | 2 | — | #400 Identity Engine (ADR-043) — algebraic identity family; promoted from candidate backlog (#610). | The sum of sixth powers dominates the mixed terms a⁴b²+a²b⁴. Not a named mathlib lemma in this form. |
sum-square-pyramidal-eq-hyper — Twelve times the sum of the first n square-pyramidal numbers equals n(n+1)^2(n+2). |
open | 3 | — | #400 Identity Engine (ADR-043) — figurate-number family; promoted from candidate backlog (#610). | Twelve times the sum of the first n square-pyramidal numbers equals n(n+1)^2(n+2). Not a named mathlib lemma in this form. |
sum-squares-eq-square-pyramidal — Six times the sum of the first n squares equals the n-th square-pyramidal number n(n+1)(2n+1). |
open | 2 | — | #400 Identity Engine (ADR-043) — figurate-number family; promoted from candidate backlog (#610). | Six times the sum of the first n squares equals the n-th square-pyramidal number n(n+1)(2n+1). Not a named mathlib lemma in this form. |
sum-star-numbers-closed-form — The sum of the first n star numbers equals n times (2n^2-1). |
open | 2 | — | #400 Identity Engine (ADR-043) — figurate-number family; promoted from candidate backlog. | The sum of the first n star numbers equals n times (2n^2-1). Not a named mathlib lemma in this form. |
sum-stella-octangula-closed-form — Twice the running sum of stella octangula numbers k(2k^2-1) equals n(n+1)(n^2+n-1). |
open | 2 | — | #400 Identity Engine (ADR-043) — figurate-number family; promoted from candidate backlog. | Twice the running sum of stella octangula numbers k(2k^2-1) equals n(n+1)(n^2+n-1). Not a named mathlib lemma in this form. |
sum-tetrahedral-eq-pentatope — Twenty-four times the sum of the first n tetrahedral numbers equals the pentatope number n(n+1)(n+2)(n+3). |
open | 3 | — | #400 Identity Engine (ADR-043) — figurate-number family; promoted from candidate backlog (#610). | Twenty-four times the sum of the first n tetrahedral numbers equals the pentatope number n(n+1)(n+2)(n+3). Not a named mathlib lemma in this form. |
sum-three-squares-zmod-eight-ne-seven — A sum of three integer squares is never congruent to 7 modulo 8 (a case of the three-square theorem). |
open | 3 | — | #400 Identity Engine (ADR-043) — modular-arith family. | A sum of three integer squares is never congruent to 7 modulo 8 (a case of the three-square theorem). Not a named mathlib lemma in this form. |
sum-three-squares-zmod-sixteen-ne-fifteen — A sum of three integer squares is never congruent to 15 modulo 16. |
open | 3 | — | #400 Identity Engine (ADR-043) — power-residue family; promoted from candidate backlog (#610). | A sum of three integer squares is never congruent to 15 modulo 16. Not a named mathlib lemma in this form. |
sum-triangular-squared-closed-form — Fifteen times the sum of squares of consecutive products k^2(k+1)^2 equals n(n+1)(n+2)(3n^2+6n+1). |
open | 3 | — | #400 Identity Engine (ADR-043) — figurate-number family; promoted from candidate backlog (#610). | Fifteen times the sum of squares of consecutive products k^2(k+1)^2 equals n(n+1)(n+2)(3n^2+6n+1). Not a named mathlib lemma in this form. |
sum-triple-product-eq — Four times the sum of products of three consecutive integers k(k+1)(k+2) equals (n-1)n(n+1)(n+2). |
open | 3 | — | #400 Identity Engine (ADR-043) — figurate family. | Four times the sum of products of three consecutive integers k(k+1)(k+2) equals (n-1)n(n+1)(n+2). Not a named mathlib lemma in this form. |
sum-two-cubes-zmod-nine-ne-four — A sum of two integer cubes is never congruent to 4 modulo 9 (cubes mod 9 are 0,1,8). |
open | 3 | — | #400 Identity Engine (ADR-043) — modular-arith family. | A sum of two integer cubes is never congruent to 4 modulo 9 (cubes mod 9 are 0,1,8). Not a named mathlib lemma in this form. |
sum-two-cubes-zmod-seven-mem — A sum of two integer cubes is never congruent to 3 or 4 modulo 7. |
open | 3 | — | #400 Identity Engine (ADR-043) — power-residue family; promoted from candidate backlog (#610). | A sum of two integer cubes is never congruent to 3 or 4 modulo 7. Not a named mathlib lemma in this form. |
sum-two-fourth-powers-zmod-sixteen-mem — A sum of two integer fourth powers is congruent to 0, 1, or 2 modulo 16. |
open | 3 | — | #400 Identity Engine (ADR-043) — power-residue family; promoted from candidate backlog (#610). | A sum of two integer fourth powers is congruent to 0, 1, or 2 modulo 16. Not a named mathlib lemma in this form. |
sum-two-k-add-one-mul-two-pow — The sum over k<n of (2k+1)·2^k equals (2n−3)·2^n + 3. |
open | 2 | — | #400 Identity Engine (ADR-043) — closed-form-sums family. | The sum over k<n of (2k+1)·2^k equals (2n−3)·2^n + 3. Not a named mathlib lemma in this form. |
sum-two-k-plus-one-div-sq-succ-sq-telescope — The sum over k<n of (2(k+1)+1)/((k+1)²(k+2)²) equals 1 − 1/(n+1)². |
open | 3 | — | #400 Identity Engine (ADR-043) — telescoping family. | The sum over k<n of (2(k+1)+1)/((k+1)²(k+2)²) equals 1 − 1/(n+1)². Not a named mathlib lemma in this form. |
sum-two-k-sub-one-mul-two-pow — The sum over k<n of (2k−1)·2^k equals (2n−5)·2^n + 5. |
open | 2 | — | #400 Identity Engine (ADR-043) — closed-form-sums family. | The sum over k<n of (2k−1)·2^k equals (2n−5)·2^n + 5. Not a named mathlib lemma in this form. |
sum-two-squares-zmod-eight-ne-six — A sum of two integer squares is never congruent to 6 modulo 8. |
open | 3 | — | #400 Identity Engine (ADR-043) — modular-arith family. | A sum of two integer squares is never congruent to 6 modulo 8. Not a named mathlib lemma in this form. |
sum-two-squares-zmod-four-ne-three — A sum of two integer squares is never congruent to 3 modulo 4. |
open | 2 | — | #400 Identity Engine (ADR-043) — power-residue family; promoted from candidate backlog (#610). | A sum of two integer squares is never congruent to 3 modulo 4. Not a named mathlib lemma in this form. |
sum-vandermonde-diagonal-eq-choose — The diagonal Vandermonde convolution, summing C(n,k) times C(m,k) over k, equals C(n+m,n). |
open | 3 | — | #400 Identity Engine (ADR-043) — binomial family; promoted from candidate backlog (#610). | The diagonal Vandermonde convolution, summing C(n,k) times C(m,k) over k, equals C(n+m,n). Not a named mathlib lemma in this form. |
sumsq-ge-ab-plus-bc — The sum of three squares dominates the two adjacent cross terms ab+bc. |
open | 2 | — | #400 Identity Engine (ADR-043) — inequality (SOS) family; promoted from candidate backlog (#610). | The sum of three squares dominates the two adjacent cross terms ab+bc. Not a named mathlib lemma in this form. |
sumsq-products-ge-abc-times-sum — The sum of squared pairwise products of three reals is at least the product abc times their sum. |
open | 2 | — | #400 Identity Engine (ADR-043) — inequality (SOS) family; promoted from candidate backlog. | The sum of squared pairwise products of three reals is at least the product abc times their sum. Not a named mathlib lemma in this form. |
sym-deg-three-ge-six-mul — For nonnegative a,b,c, a²b+ab²+b²c+bc²+c²a+ca² ≥ 6abc. |
open | 3 | — | #400 Identity Engine (ADR-043) — inequalities family. | For nonnegative a,b,c, a²b+ab²+b²c+bc²+c²a+ca² ≥ 6abc. Not a named mathlib lemma in this form. |
sym-grouped-deg-three-ge-six-abc — For nonnegatives the grouped symmetric degree-three form a^2(b+c)+… is at least 6abc. |
open | 3 | — | #400 Identity Engine (ADR-043) — inequality (SOS) family; promoted from candidate backlog (#610). | For nonnegatives the grouped symmetric degree-three form a^2(b+c)+… is at least 6abc. Not a named mathlib lemma in this form. |
tangent-line-cube-trick — The tangent-line bound at x=1 for the cube: 3x is at most x cubed plus two for nonnegative x. |
open | 3 | — | #400 Identity Engine (ADR-043) — inequality (SOS) family; promoted from candidate backlog (#610). | The tangent-line bound at x=1 for the cube: 3x is at most x cubed plus two for nonnegative x. Not a named mathlib lemma in this form. |
three-cubes-minus-three-prod-dvd-sum — The sum a+b+c divides the symmetric expression a cubed plus b cubed plus c cubed minus three times abc. |
open | 2 | — | #400 Identity Engine (ADR-043) — algebraic identity family; promoted from candidate backlog (#610). | The sum a+b+c divides the symmetric expression a cubed plus b cubed plus c cubed minus three times abc. Not a named mathlib lemma in this form. |
three-cubes-zmod-nine-ne-four-five — A sum of three integer cubes is never congruent to 4 or 5 modulo 9. |
open | 2 | — | #400 Identity Engine (ADR-043) — power-residue family; promoted from candidate backlog. | A sum of three integer cubes is never congruent to 4 or 5 modulo 9. Not a named mathlib lemma in this form. |
three-fourth-powers-zmod-sixteen-mem — A sum of three integer fourth powers is always congruent to 0, 1, 2, or 3 modulo 16. |
open | 3 | — | #400 Identity Engine (ADR-043) — power-residue family; promoted from candidate backlog. | A sum of three integer fourth powers is always congruent to 0, 1, 2, or 3 modulo 16. Not a named mathlib lemma in this form. |
three-mul-fib-eq-fib-add-two-add-fib-sub-two — Three times fib(n+2) equals fib(n+4) plus fib n. |
open | 2 | — | #400 Identity Engine (ADR-043) — Fibonacci/Lucas family; promoted from candidate backlog (#610). | Three times fib(n+2) equals fib(n+4) plus fib n. Not a named mathlib lemma in this form. |
three-quartic-sum-ge-sumsq-sq — Three times the sum of fourth powers dominates the square of the sum of squares (QM-AM on squares). |
open | 3 | — | #400 Identity Engine (ADR-043) — inequality (SOS) family; promoted from candidate backlog (#610). | Three times the sum of fourth powers dominates the square of the sum of squares (QM-AM on squares). Not a named mathlib lemma in this form. |
two-cubes-zmod-nine-ne-three-four-five-six — A sum of two integer cubes is never congruent to 3, 4, 5, or 6 modulo 9. |
open | 2 | — | #400 Identity Engine (ADR-043) — power-residue family; promoted from candidate backlog. | A sum of two integer cubes is never congruent to 3, 4, 5, or 6 modulo 9. Not a named mathlib lemma in this form. |
two-fib-add-int — 2·fib(m+n) = fib(m)·L(n) + L(m)·fib(n), the symmetric Fibonacci addition law. |
open | 3 | — | #400 Identity Engine (ADR-043) — Fibonacci/Lucas family; promoted from candidate backlog (#610). | 2·fib(m+n) = fib(m)·L(n) + L(m)·fib(n), the symmetric Fibonacci addition law. Not a named mathlib lemma in this form. |
two-fourth-powers-zmod-five-ne-three-four — A sum of two integer fourth powers is never congruent to 3 or 4 modulo 5. |
open | 2 | — | #400 Identity Engine (ADR-043) — power-residue family; promoted from candidate backlog. | A sum of two integer fourth powers is never congruent to 3 or 4 modulo 5. Not a named mathlib lemma in this form. |
two-mul-sum-icc-three-k-sub-two-eq-pentagonal — Twice the sum of (3k-2) for k from 1 to n equals n(3n-1), making the n-th partial sum the pentagonal number P_n. |
open | 2 | — | #400 Identity Engine (ADR-043) — partition/generating-function family; promoted from candidate backlog (#610). | Twice the sum of (3k-2) for k from 1 to n equals n(3n-1), making the n-th partial sum the pentagonal number P_n. Not a named mathlib lemma in this form. |
two-mul-sum-range-fib-triple-eq-fib-pred — Twice the sum of fib at multiples of three up to 3n is one less than fib(3n-1). |
open | 4 | — | #400 Identity Engine (ADR-043) — Fibonacci/Lucas family; promoted from candidate backlog (#610). | Twice the sum of fib at multiples of three up to 3n is one less than fib(3n-1). Not a named mathlib lemma in this form. |
two-squares-zmod-sixteen-ne-three-seven-eleven — A sum of two integer squares is never congruent to 3, 7, 11, or 15 modulo 16. |
open | 2 | — | #400 Identity Engine (ADR-043) — power-residue family; promoted from candidate backlog. | A sum of two integer squares is never congruent to 3, 7, 11, or 15 modulo 16. Not a named mathlib lemma in this form. |
two-sum-cubes-ge-sym-quadratics — For nonnegative a,b,c, 2(a³+b³+c³) ≥ ab(a+b)+bc(b+c)+ca(c+a). |
open | 3 | — | #400 Identity Engine (ADR-043) — inequalities family. | For nonnegative a,b,c, 2(a³+b³+c³) ≥ ab(a+b)+bc(b+c)+ca(c+a). Not a named mathlib lemma in this form. |
nesbitt-inequality — Nesbitt’s inequality: for positive reals a, b, c, a/(b+c) + b/(c+a) + c/(a+b) ≥ 3/2. |
blocked | 4 | — | Nesbitt’s inequality (1903), a classic three-variable cyclic inequality; AoPS/olympiad canon. | 3/2 ≤ a/(b+c) + b/(c+a) + c/(a+b) for a,b,c > 0. mathlib has inner_mul_le_norm_mul_norm and div_add_div_same-style lemmas but no Nesbitt lemma. |
sq-add-sq-eq-three-mul-sq — The Diophantine equation $x^2 + y^2 = 3z^2$ has only the trivial solution $x=y=z=0$ in integers. |
blocked | 4 | — | elementary number theory | Classic infinite descent argument modulo 3 showing that $3 \mid x$ and $3 \mid y$, which leads to infinite descent. |
sum-icc-choose-hockey-stick — The hockey-stick identity: ∑_{k=r}^{n} C(k,r) = C(n+1,r+1). |
blocked | 3 | — | Classic combinatorial / finite-sum identity (library-growth batch, #400 plan Phase 3). | The hockey-stick identity: ∑_{k=r}^{n} C(k,r) = C(n+1,r+1). Not a named mathlib lemma (Vandermonde/Pascal are present but not these specific closed forms). |
abc-nine-le-sum-times-pairsum — For nonnegative reals nine times abc is at most (a+b+c)(ab+bc+ca). |
proved | 3 | — | #400 Identity Engine (ADR-043) — inequality (SOS) family; promoted from candidate backlog (#610). | For nonnegative reals nine times abc is at most (a+b+c)(ab+bc+ca). Not a named mathlib lemma in this form. |
abstract-regular-polyhedron-classification — For an abstract regular polyhedron — V vertices, E edges, F faces that are p-gons, vertices of degree q — with the two handshakes p·F = 2E and q·V = 2E and Euler’s relation V + F = E + 2, the pair (p, q) is one of the five Platonic Schläfli pairs {(3,3),(3,4),(4,3),(3,5),(5,3)}. The classification (⟹) half of Freek #50 in combinatorial/Euler form. |
proved | 3 | — | Freek 100 (#50), combinatorial form (ADR-031 / SPEC-031-A, Track 1) | The classification half of ‘there are exactly five Platonic solids’, reusing the proved platonic_schlafli_pairs as keystone (Euler + handshake ⟹ 1/p+1/q > 1/2 ⟹ the five pairs). Coxeter, Regular Polytopes, Ch. 1. NOT the geometric Freek #50 (that is Track 2, gated on a mathlib polytope face lattice + Euler–Poincaré). |
alternating-sum-naturals — For every natural n, the sum over i in 0..n-1 of (-1)^i (i+1) equals -(n/2) if n is even and (n/2)+1 if n is odd (integer division over ℤ). |
proved | 3 | packet-ready | classic identities | Standard arithmetic alternating-series partial sums (1-2+3-4+…); tabulated in Hardy, Divergent Series, Ch. 1; elementary induction exercise in discrete-math texts. |
am-gm-three-cube-s1 — am-gm-three-cube-s1 |
proved | 1 | — | — | — |
am-gm-three-cube-s2 — am-gm-three-cube-s2 |
proved | 1 | — | — | — |
am-gm-three-cube-s2-s1 — am-gm-three-cube-s2-s1 |
proved | 1 | — | — | — |
am-gm-three-cube-s2-s2 — am-gm-three-cube-s2-s2 |
proved | 1 | — | — | — |
am-gm-three-cube-s2-s2-s1 — am-gm-three-cube-s2-s2-s1 |
proved | 1 | — | — | — |
am-gm-three-cube-s2-s2-s2 — am-gm-three-cube-s2-s2-s2 |
proved | 1 | — | — | — |
am-hm-two-var-s1 — am-hm-two-var-s1 |
proved | 1 | — | — | — |
am-hm-two-var-s2 — am-hm-two-var-s2 |
proved | 1 | — | — | — |
am-hm-two-var-s3 — am-hm-two-var-s3 |
proved | 1 | — | — | — |
amgm-four-cross-three-var — The sum of fourth powers dominates the sum of squared pairwise products. |
proved | 3 | — | #400 Identity Engine (ADR-043) — inequality (SOS) family; promoted from candidate backlog (#610). | The sum of fourth powers dominates the sum of squared pairwise products. Not a named mathlib lemma in this form. |
amgm-prod-half-sum-le-cubes — Twice ab(a+b) is at most twice the sum of cubes for nonnegative reals. |
proved | 3 | — | #400 Identity Engine (ADR-043) — inequality (SOS) family; promoted from candidate backlog (#610). | Twice ab(a+b) is at most twice the sum of cubes for nonnegative reals. Not a named mathlib lemma in this form. |
and-comm-imp — Conjunction commutes. |
proved | 1 | — | — | — |
aurifeuillian-quartic-dvd — The quadratic a²+a+1 always divides a⁴+a²+1. |
proved | 2 | — | #400 Identity Engine (ADR-043) — algebraic family. | The quadratic a²+a+1 always divides a⁴+a²+1. Not a named mathlib lemma in this form. |
bezout-eleven-thirteen-eq-one — There exist integers x, y with 11x + 13y = 1. |
proved | 2 | — | #400 Identity Engine (ADR-043) — gcd/coprimality family; promoted from candidate backlog (#610). | There exist integers x, y with 11x + 13y = 1. Not a named mathlib lemma in this form. |
bezout-five-seven-eq-one — There exist integers x, y with 5x + 7y = 1. |
proved | 2 | — | #400 Identity Engine (ADR-043) — gcd/coprimality family; promoted from candidate backlog (#610). | There exist integers x, y with 5x + 7y = 1. Not a named mathlib lemma in this form. |
binder-shape-canary — A Gate A regression fixture, not a mathematical target. It carries the implicit-then-named-hypothesis binder shape ({n : Nat} (h : 1 < n)) that issue #231 showed makes a goal’s regenerated ADR-011 binding obligation trip linter.unusedVariables under the Gate A --wfail build — which had made every goal of this shape unprovable regardless of the proof’s correctness. |
proved | 1 | — | Gate A regression fixture (issue #231) | — |
candido-sum-quartics-twice-square — Candido’s identity: the sum of the fourth powers of a, b and a+b is always twice a perfect square. |
proved | 2 | — | #400 Identity Engine (ADR-043) — algebraic identity family; promoted from candidate backlog (#610). | Candido’s identity: the sum of the fourth powers of a, b and a+b is always twice a perfect square. Not a named mathlib lemma in this form. |
cauchy-schwarz-three-term — For all real a,b,c,x,y,z, (ax+by+cz)² ≤ (a²+b²+c²)(x²+y²+z²) — the 3-term Cauchy–Schwarz inequality. |
proved | 3 | — | Classic real inequality (library-growth batch, #400 plan Phase 3). The project had almost no inequalities; this seeds the SOS/nlinarith family. | For all real a,b,c,x,y,z, (ax+by+cz)² ≤ (a²+b²+c²)(x²+y²+z²) — the 3-term Cauchy–Schwarz inequality. mathlib has the abstract Cauchy–Schwarz / power-mean lemmas but not this concrete polynomial form as a named lemma. |
cauchy-schwarz-two-term — For reals, the square of a dot product of two 2-vectors is at most the product of their squared norms (the two-term Cauchy-Schwarz inequality). |
proved | 2 | — | #400 Identity Engine (ADR-043) — algebraic identity family; promoted from candidate backlog (#610). | For reals, the square of a dot product of two 2-vectors is at most the product of their squared norms (the two-term Cauchy-Schwarz inequality). Not a named mathlib lemma in this form. |
consec-prod-succ-coprime — Any number n(n+1) is coprime to its successor. |
proved | 2 | — | #400 Identity Engine (ADR-043) — gcd/coprimality family; promoted from candidate backlog. | Any number n(n+1) is coprime to its successor. Not a named mathlib lemma in this form. |
consecutive-cubes-diff-odd — For every integer n, (n+1)³ − n³ is odd. |
proved | 2 | — | Classic elementary inequality / number-theory fact (#400 plan Phase 3 — library growth). | For every integer n, (n+1)³ − n³ is odd. Not a named mathlib lemma in this concrete form. |
consecutive-triangular-eq-square — For every natural n, Tₙ + Tₙ₋₁ = n², where Tₙ = ∑_{i≤n} i; the sum of two consecutive triangular numbers is a perfect square. |
proved | 2 | — | classic identities (triangular-number gems — compounds on the Gauss sum) | Theon of Smyrna’s classical observation that consecutive triangular numbers sum to a square (Tₙ₋₁ + Tₙ = n²). Conway & Guy, The Book of Numbers; Heath, A History of Greek Mathematics. |
constrained-pairsum-le-three-sum-three — If three reals sum to 3 then their pairwise product sum is at most 3. |
proved | 2 | — | #400 Identity Engine (ADR-043) — inequality (SOS) family; promoted from candidate backlog (#610). | If three reals sum to 3 then their pairwise product sum is at most 3. Not a named mathlib lemma in this form. |
constrained-prod-le-sum-cubes-third — Among nonnegative reals summing to 1 the product abc is at most 1/27. |
proved | 2 | — | #400 Identity Engine (ADR-043) — inequality (SOS) family; promoted from candidate backlog. | Among nonnegative reals summing to 1 the product abc is at most 1/27. Not a named mathlib lemma in this form. |
constrained-sum-le-sumsq-prod-one — If three positive reals have product 1 then their sum of squares is at least their sum. |
proved | 2 | — | #400 Identity Engine (ADR-043) — inequality (SOS) family; promoted from candidate backlog. | If three positive reals have product 1 then their sum of squares is at least their sum. Not a named mathlib lemma in this form. |
constrained-sum-sq-ge-one-third — If three reals sum to 1 then their sum of squares is at least 1/3. |
proved | 2 | — | #400 Identity Engine (ADR-043) — inequality (SOS) family; promoted from candidate backlog (#610). | If three reals sum to 1 then their sum of squares is at least 1/3. Not a named mathlib lemma in this form. |
constrained-sum-sq-ge-three — For real a,b,c with a+b+c=3, a²+b²+c² ≥ 3 — the constrained tangent-line bound. |
proved | 2 | — | Classic real inequality (library-growth batch, #400 plan Phase 3). The project had almost no inequalities; this seeds the SOS/nlinarith family. | For real a,b,c with a+b+c=3, a²+b²+c² ≥ 3 — the constrained tangent-line bound. mathlib has the abstract Cauchy–Schwarz / power-mean lemmas but not this concrete polynomial form as a named lemma. |
coprime-2n1-2n3 — Two consecutive odd numbers 2n+1 and 2n+3 are coprime. |
proved | 2 | — | #400 Identity Engine (ADR-043) — gcd/coprimality family; promoted from candidate backlog (#610). | Two consecutive odd numbers 2n+1 and 2n+3 are coprime. Not a named mathlib lemma in this form. |
coprime-2n1-3n2 — 2n+1 and 3n+2 are always coprime. |
proved | 2 | — | #400 Identity Engine (ADR-043) — gcd/coprimality family; promoted from candidate backlog (#610). | 2n+1 and 3n+2 are always coprime. Not a named mathlib lemma in this form. |
coprime-2n1-n1 — 2n+1 and n+1 are coprime for every n. |
proved | 3 | — | #400 Identity Engine (ADR-043) — gcd-coprime family. | 2n+1 and n+1 are coprime for every n. Not a named mathlib lemma in this form. |
coprime-3n1-4n1 — 3n+1 and 4n+1 are always coprime. |
proved | 2 | — | #400 Identity Engine (ADR-043) — gcd/coprimality family; promoted from candidate backlog (#610). | 3n+1 and 4n+1 are always coprime. Not a named mathlib lemma in this form. |
coprime-consec-tri — The odd number 2n+1 is coprime to the product n(n+1). |
proved | 3 | — | #400 Identity Engine (ADR-043) — gcd/coprimality family; promoted from candidate backlog (#610). | The odd number 2n+1 is coprime to the product n(n+1). Not a named mathlib lemma in this form. |
coprime-fib-sq-fib-succ — The square of fib n is coprime to fib (n+1). |
proved | 3 | — | #400 Identity Engine (ADR-043) — gcd/coprimality family; promoted from candidate backlog (#610). | The square of fib n is coprime to fib (n+1). Not a named mathlib lemma in this form. |
coprime-n-cube-add-one — n is coprime to n cubed plus one. |
proved | 2 | — | #400 Identity Engine (ADR-043) — gcd/coprimality family; promoted from candidate backlog (#610). | n is coprime to n cubed plus one. Not a named mathlib lemma in this form. |
coprime-n-sq-n-add-one — n is coprime to n squared plus n plus one. |
proved | 2 | — | #400 Identity Engine (ADR-043) — gcd/coprimality family; promoted from candidate backlog (#610). | n is coprime to n squared plus n plus one. Not a named mathlib lemma in this form. |
coprime-n1-nsq1 — The gcd of n+1 and n^2+1 always divides 2. |
proved | 3 | — | #400 Identity Engine (ADR-043) — gcd/coprimality family; promoted from candidate backlog (#610). | The gcd of n+1 and n^2+1 always divides 2. Not a named mathlib lemma in this form. |
coprime-n2p1-n2p2 — n^2+1 and n^2+2 are consecutive integers, hence coprime. |
proved | 2 | — | #400 Identity Engine (ADR-043) — gcd/coprimality family; promoted from candidate backlog (#610). | n^2+1 and n^2+2 are consecutive integers, hence coprime. Not a named mathlib lemma in this form. |
coprime-ncube1-ncube2 — The consecutive values n^3+1 and n^3+2 are coprime for every n. |
proved | 2 | — | #400 Identity Engine (ADR-043) — gcd/coprimality family; promoted from candidate backlog (#610). | The consecutive values n^3+1 and n^3+2 are coprime for every n. Not a named mathlib lemma in this form. |
coprime-nsq2-nsq3 — The consecutive values n^2+2 and n^2+3 are coprime for every n. |
proved | 2 | — | #400 Identity Engine (ADR-043) — gcd/coprimality family; promoted from candidate backlog (#610). | The consecutive values n^2+2 and n^2+3 are coprime for every n. Not a named mathlib lemma in this form. |
coprime-succ-sq-add — n+1 is coprime to n²+n+1. |
proved | 3 | — | #400 Identity Engine (ADR-043) — gcd-coprime family. | n+1 is coprime to n²+n+1. Not a named mathlib lemma in this form. |
coprime-twopow-sub-one-two — For every positive n, 2^n - 1 is odd and hence coprime to 2. |
proved | 3 | — | #400 Identity Engine (ADR-043) — gcd/coprimality family; promoted from candidate backlog (#610). | For every positive n, 2^n - 1 is odd and hence coprime to 2. Not a named mathlib lemma in this form. |
cube-eq-triangular-sq-diff — For every natural n, Tₙ₋₁² + n³ = Tₙ², where Tₙ = ∑_{i≤n} i; equivalently n³ = Tₙ² − Tₙ₋₁², the per-term form of Nicomachus’s theorem (the n-th cube is the n-th difference of squared triangular numbers). |
proved | 2 | — | classic identities (triangular-number gems — the term-wise Nicomachus; compounds on nicomachus-sum-cubes) |
The telescoping core of Nicomachus’s identity ∑k³ = (∑k)² = Tₙ²: each cube n³ = Tₙ² − Tₙ₋₁². Conway & Guy, The Book of Numbers; Mathematics in Lean §5 (the Nicomachus exercise). |
cube-mod-eighteen-mem — The cubes modulo 18 are exactly {0,1,8,9,10,17}. |
proved | 3 | — | #400 Identity Engine (ADR-043) — power-residue family; promoted from candidate backlog (#610). | The cubes modulo 18 are exactly {0,1,8,9,10,17}. Not a named mathlib lemma in this form. |
cube-mod-fortythree-mem — The cubic residues modulo the prime 43 are exactly the fifteen values {0,1,2,4,8,11,16,21,22,27,32,35,39,41,42}. |
proved | 3 | — | #400 Identity Engine (ADR-043) — power-residue family; promoted from candidate backlog. | The cubic residues modulo the prime 43 are exactly the fifteen values {0,1,2,4,8,11,16,21,22,27,32,35,39,41,42}. Not a named mathlib lemma in this form. |
cube-mod-four — For every natural n, n³ % 4 ∈ {0,1,3} (cubic residues mod 4). |
proved | 2 | — | #400 Identity Engine (ADR-043) — power-residue family. | For every natural n, n³ % 4 ∈ {0,1,3} (cubic residues mod 4). Not a named mathlib lemma in this form. |
cube-mod-fourteen-mem — The cubic residues modulo 14 are exactly 0, 1, 6, 7, 8, and 13. |
proved | 2 | — | #400 Identity Engine (ADR-043) — power-residue family; promoted from candidate backlog (#610). | The cubic residues modulo 14 are exactly 0, 1, 6, 7, 8, and 13. Not a named mathlib lemma in this form. |
cube-mod-nine — For every natural number n, the cube n³ is ≡ 0, 1, or 8 (mod 9). |
proved | 2 | — | #400 Identity Engine (ADR-043) — power-residue family. | The cubic residues mod 9 are exactly {0,1,8}. Not a named mathlib lemma. |
cube-mod-nineteen-mem — The cubic residues modulo 19 are exactly {0,1,7,8,11,12,18}. |
proved | 3 | — | #400 Identity Engine (ADR-043) — power-residue family; promoted from candidate backlog (#610). | The cubic residues modulo 19 are exactly {0,1,7,8,11,12,18}. Not a named mathlib lemma in this form. |
cube-mod-seven — For every natural n, n³ % 7 ∈ {0,1,6}. |
proved | 2 | — | #400 Identity Engine (ADR-043) — power-residue family. | For every natural n, n³ % 7 ∈ {0,1,6}. Not a named mathlib lemma in this form. |
cube-mod-thirteen-mem — Every cube is congruent to 0, 1, 5, 8, or 12 modulo 13 (the cubic residues mod 13). |
proved | 3 | — | #400 Identity Engine (ADR-043) — power-residue family. | Every cube is congruent to 0, 1, 5, 8, or 12 modulo 13 (the cubic residues mod 13). Not a named mathlib lemma in this form. |
cube-mod-thirtyone-nonresidue-five — None of 3, 5, 6, 7 is a cubic residue modulo 31. |
proved | 3 | — | #400 Identity Engine (ADR-043) — power-residue family; promoted from candidate backlog (#610). | None of 3, 5, 6, 7 is a cubic residue modulo 31. Not a named mathlib lemma in this form. |
cube-mod-thirtyseven-mem — The cubic residues modulo the prime 37 are exactly {0,1,6,8,10,11,14,23,26,27,29,31,36}. |
proved | 3 | — | #400 Identity Engine (ADR-043) — power-residue family; promoted from candidate backlog. | The cubic residues modulo the prime 37 are exactly {0,1,6,8,10,11,14,23,26,27,29,31,36}. Not a named mathlib lemma in this form. |
cube-mod-twentyone-mem — Every cube is congruent to one of {0,1,6,7,8,13,14,15,20} modulo 21. |
proved | 2 | — | #400 Identity Engine (ADR-043) — power-residue family; promoted from candidate backlog (#610). | Every cube is congruent to one of {0,1,6,7,8,13,14,15,20} modulo 21. Not a named mathlib lemma in this form. |
cube-mod-twentyseven-mem — The cubic residues modulo 27 are exactly 0, 1, 8, 10, 17, 19, and 26. |
proved | 3 | — | #400 Identity Engine (ADR-043) — power-residue family; promoted from candidate backlog (#610). | The cubic residues modulo 27 are exactly 0, 1, 8, 10, 17, 19, and 26. Not a named mathlib lemma in this form. |
cube-mod-twentysix-mem — The cubic residues modulo 26 are exactly 0,1,5,8,12,13,14,18,21,25. |
proved | 3 | — | #400 Identity Engine (ADR-043) — power-residue family; promoted from candidate backlog (#610). | The cubic residues modulo 26 are exactly 0,1,5,8,12,13,14,18,21,25. Not a named mathlib lemma in this form. |
cube-of-sum-minus-cubes-div-by-sum — The difference between (a+b+c)³ and a³+b³+c³ is divisible by a+b (it equals 3(a+b)(b+c)(c+a)). |
proved | 2 | — | #400 Identity Engine (ADR-043) — algebraic identity family; promoted from candidate backlog (#610). | The difference between (a+b+c)³ and a³+b³+c³ is divisible by a+b (it equals 3(a+b)(b+c)(c+a)). Not a named mathlib lemma in this form. |
cube-sum-ge-mul-sq — For nonneg reals a,b, a³+b³ ≥ a²b+ab² (since a³+b³−a²b−ab² = (a+b)(a−b)²). |
proved | 2 | — | Classic elementary inequality / number-theory fact (#400 plan Phase 3). | For nonneg reals a,b, a³+b³ ≥ a²b+ab² (since a³+b³−a²b−ab² = (a+b)(a−b)²). Not a named mathlib lemma in this form. |
cube-sum-ge-three-prod — For nonneg reals, 3abc ≤ a³+b³+c³ — AM-GM for cubes (a³+b³+c³−3abc = (a+b+c)·½Σ(a−b)²). |
proved | 2 | — | Classic elementary real inequality (#400 plan Phase 3 — library growth). | For nonneg reals, 3abc ≤ a³+b³+c³ — AM-GM for cubes (a³+b³+c³−3abc = (a+b+c)·½Σ(a−b)²). Not a named mathlib lemma in this concrete polynomial/abs form. |
cube-sum-ge-three-prod-s1 — cube-sum-ge-three-prod-s1 |
proved | 1 | — | — | — |
cube-sum-ge-three-prod-s2 — cube-sum-ge-three-prod-s2 |
proved | 1 | — | — | — |
cube-sum-ge-three-prod-s3 — cube-sum-ge-three-prod-s3 |
proved | 1 | — | — | — |
cyclic-quad-ge-abc-times-sum — The sum of squared pairwise products dominates abc(a+b+c) for all reals. |
proved | 3 | — | #400 Identity Engine (ADR-043) — inequality (SOS) family; promoted from candidate backlog (#610). | The sum of squared pairwise products dominates abc(a+b+c) for all reals. Not a named mathlib lemma in this form. |
cyclic-quartic-ge-asym-cubic-cross — For nonnegative reals the sum of fourth powers dominates the cyclic sum a^3 b + b^3 c + c^3 a. |
proved | 2 | — | #400 Identity Engine (ADR-043) — inequality (SOS) family; promoted from candidate backlog. | For nonnegative reals the sum of fourth powers dominates the cyclic sum a^3 b + b^3 c + c^3 a. Not a named mathlib lemma in this form. |
descartes-total-angular-defect — Descartes’ theorem: the total angular defect of an abstract regular {p,q} polyhedron is 4π — V(2π − q·(p−2)/p·π) = 4π. |
proved | 4 | — | Freek #50 combinatorial classification, Track-1 completion (ADR-031; #400 plan Phase 1). | Descartes’ theorem: the total angular defect of an abstract regular {p,q} polyhedron is 4π — V(2π − q·(p−2)/p·π) = 4π. Not in mathlib (no abstract-regular-polyhedron theory). |
diff-sixth-power-dvd-by-sum — The sum of two integers divides the difference of their sixth powers. |
proved | 2 | — | #400 Identity Engine (ADR-043) — algebraic identity family; promoted from candidate backlog (#610). | The sum of two integers divides the difference of their sixth powers. Not a named mathlib lemma in this form. |
diff-twelfth-power-dvd-by-diff-cube — The difference of cubes divides the difference of twelfth powers. |
proved | 2 | — | #400 Identity Engine (ADR-043) — algebraic identity family; promoted from candidate backlog (#610). | The difference of cubes divides the difference of twelfth powers. Not a named mathlib lemma in this form. |
diff-two-cubes-zmod-seven-ne-three-four — A difference of two integer cubes is never congruent to 3 or 4 modulo 7. |
proved | 2 | — | #400 Identity Engine (ADR-043) — power-residue family; promoted from candidate backlog. | A difference of two integer cubes is never congruent to 3 or 4 modulo 7. Not a named mathlib lemma in this form. |
diff-two-squares-zmod-four-ne-two — A difference of two integer squares is never congruent to 2 modulo 4. |
proved | 2 | — | #400 Identity Engine (ADR-043) — power-residue family; promoted from candidate backlog (#610). | A difference of two integer squares is never congruent to 2 modulo 4. Not a named mathlib lemma in this form. |
diff-two-squares-zmod-sixteen-ne-two-six — A difference of two integer squares is never congruent to 2, 6, 10, or 14 modulo 16. |
proved | 2 | — | #400 Identity Engine (ADR-043) — power-residue family; promoted from candidate backlog. | A difference of two integer squares is never congruent to 2, 6, 10, or 14 modulo 16. Not a named mathlib lemma in this form. |
discriminant-nonneg — If a>0 and b²≤4ac, then ax²+bx+c ≥ 0 for all x (the discriminant nonnegativity criterion). |
proved | 3 | — | Classic elementary real inequality (#400 plan Phase 3 — library growth). | If a>0 and b²≤4ac, then ax²+bx+c ≥ 0 for all x (the discriminant nonnegativity criterion). Not a named mathlib lemma in this concrete polynomial/abs form. |
discriminant-nonneg-s1 — discriminant-nonneg-s1 |
proved | 1 | — | — | — |
discriminant-nonneg-s2 — discriminant-nonneg-s2 |
proved | 1 | — | — | — |
discriminant-nonneg-s3 — discriminant-nonneg-s3 |
proved | 1 | — | — | — |
dvd-1023-pow-thirtyone-sub-self — The integer 1023 = 3·11·31 divides n^31 - n for every integer n. |
proved | 3 | — | #400 Identity Engine (ADR-043) — divisibility family; promoted from candidate backlog (#610). | The integer 1023 = 3·11·31 divides n^31 - n for every integer n. Not a named mathlib lemma in this form. |
dvd-120-five-consecutive-product — 120 (=5!) divides n·(n^2-1)·(n^2-4), the product of five consecutive integers centred at n. |
proved | 3 | — | #400 Identity Engine (ADR-043) — divisibility family; promoted from candidate backlog. | 120 (=5!) divides n·(n^2-1)·(n^2-4), the product of five consecutive integers centred at n. Not a named mathlib lemma in this form. |
dvd-120-pow-seven-sub-pow-three — 120 divides n^7 minus n^3 for every integer n. |
proved | 3 | — | #400 Identity Engine (ADR-043) — divisibility family; promoted from candidate backlog (#610). | 120 divides n^7 minus n^3 for every integer n. Not a named mathlib lemma in this form. |
dvd-1365-pow-thirteen-sub-self — The integer 1365 = 3·5·7·13 divides n^13 - n for every integer n. |
proved | 2 | — | #400 Identity Engine (ADR-043) — divisibility family; promoted from candidate backlog (#610). | The integer 1365 = 3·5·7·13 divides n^13 - n for every integer n. Not a named mathlib lemma in this form. |
dvd-138-pow-fortyfive-sub-pow-twentythree — 138 divides n^45 - n^23 for every integer n. |
proved | 2 | — | #400 Identity Engine (ADR-043) — divisibility family; promoted from candidate backlog. | 138 divides n^45 - n^23 for every integer n. Not a named mathlib lemma in this form. |
dvd-210-pow-fifteen-sub-pow-three-s1 — dvd-210-pow-fifteen-sub-pow-three-s1 |
proved | 1 | — | — | — |
dvd-210-pow-fifteen-sub-pow-three-s2 — dvd-210-pow-fifteen-sub-pow-three-s2 |
proved | 1 | — | — | — |
dvd-210-pow-fifteen-sub-pow-three-s3 — dvd-210-pow-fifteen-sub-pow-three-s3 |
proved | 1 | — | — | — |
dvd-210-pow-fifteen-sub-pow-three-s4 — dvd-210-pow-fifteen-sub-pow-three-s4 |
proved | 1 | — | — | — |
dvd-240-pow-eight-sub-pow-four — 240 divides n^8 minus n^4 for every integer n. |
proved | 3 | — | #400 Identity Engine (ADR-043) — divisibility family; promoted from candidate backlog (#610). | 240 divides n^8 minus n^4 for every integer n. Not a named mathlib lemma in this form. |
dvd-264-pow-thirteen-sub-pow-three — The integer 264 = 2^3·3·11 divides n^13 - n^3 for every integer n. |
proved | 3 | — | #400 Identity Engine (ADR-043) — divisibility family; promoted from candidate backlog (#610). | The integer 264 = 2^3·3·11 divides n^13 - n^3 for every integer n. Not a named mathlib lemma in this form. |
dvd-282-pow-fortyseven-sub-self — 282 divides n^47 - n for every integer n. |
proved | 3 | — | #400 Identity Engine (ADR-043) — divisibility family; promoted from candidate backlog. | 282 divides n^47 - n for every integer n. Not a named mathlib lemma in this form. |
dvd-30-pow-nine-sub-self — 30 divides n^9 - n for every integer n. |
proved | 3 | — | #400 Identity Engine (ADR-043) — divisibility family. | 30 divides n^9 - n for every integer n. Not a named mathlib lemma in this form. |
dvd-30-pow-twentyone-sub-pow-five — 30 divides n^21 - n^5 for every integer n. |
proved | 2 | — | #400 Identity Engine (ADR-043) — divisibility family; promoted from candidate backlog. | 30 divides n^21 - n^5 for every integer n. Not a named mathlib lemma in this form. |
dvd-330-pow-twentyone-sub-self — 330 divides n^21 minus n for every integer n. |
proved | 3 | — | #400 Identity Engine (ADR-043) — divisibility family; promoted from candidate backlog (#610). | 330 divides n^21 minus n for every integer n. Not a named mathlib lemma in this form. |
dvd-399-pow-nineteen-sub-self — The integer 399 = 3·7·19 divides n^19 - n for every integer n. |
proved | 2 | — | #400 Identity Engine (ADR-043) — divisibility family; promoted from candidate backlog (#610). | The integer 399 = 3·7·19 divides n^19 - n for every integer n. Not a named mathlib lemma in this form. |
dvd-42-pow-twentyfive-sub-pow-seven — 42 divides n^25 - n^7 for every integer n. |
proved | 2 | — | #400 Identity Engine (ADR-043) — divisibility family; promoted from candidate backlog. | 42 divides n^25 - n^7 for every integer n. Not a named mathlib lemma in this form. |
dvd-455-pow-thirteen-sub-self — The integer 455 = 5·7·13 divides n^13 - n for every integer n. |
proved | 2 | — | #400 Identity Engine (ADR-043) — divisibility family; promoted from candidate backlog (#610). | The integer 455 = 5·7·13 divides n^13 - n for every integer n. Not a named mathlib lemma in this form. |
dvd-462-pow-thirtyone-sub-self — The integer 462 = 2·3·7·11 divides n^31 - n for every integer n. |
proved | 3 | — | #400 Identity Engine (ADR-043) — divisibility family; promoted from candidate backlog (#610). | The integer 462 = 2·3·7·11 divides n^31 - n for every integer n. Not a named mathlib lemma in this form. |
dvd-480-pow-thirteen-sub-pow-five — 480 divides n^13 minus n^5 for every integer n. |
proved | 3 | — | #400 Identity Engine (ADR-043) — divisibility family; promoted from candidate backlog (#610). | 480 divides n^13 minus n^5 for every integer n. Not a named mathlib lemma in this form. |
dvd-510-pow-seventeen-sub-self — 510 divides n^17 minus n for every integer n. |
proved | 3 | — | #400 Identity Engine (ADR-043) — divisibility family; promoted from candidate backlog (#610). | 510 divides n^17 minus n for every integer n. Not a named mathlib lemma in this form. |
dvd-66-pow-eleven-sub-self — 66 divides n^11 - n for every integer n. |
proved | 3 | — | #400 Identity Engine (ADR-043) — divisibility family. | 66 divides n^11 - n for every integer n. Not a named mathlib lemma in this form. |
dvd-66-pow-twentyone-sub-pow-eleven — For every integer n, 66 divides n to the 21st power minus n to the 11th power. |
proved | 3 | — | #400 Identity Engine (ADR-043) — divisibility family; promoted from candidate backlog (#610). | For every integer n, 66 divides n to the 21st power minus n to the 11th power. Not a named mathlib lemma in this form. |
dvd-798-pow-nineteen-sub-self — 798 divides n^19 minus n for every integer n. |
proved | 3 | — | #400 Identity Engine (ADR-043) — divisibility family; promoted from candidate backlog (#610). | 798 divides n^19 minus n for every integer n. Not a named mathlib lemma in this form. |
dvd-798-pow-thirtyseven-sub-pow-nineteen — 798 divides n^37 - n^19 for every integer n. |
proved | 3 | — | #400 Identity Engine (ADR-043) — divisibility family; promoted from candidate backlog. | 798 divides n^37 - n^19 for every integer n. Not a named mathlib lemma in this form. |
dvd-910-pow-fifteen-sub-pow-three — The integer 910 = 2·5·7·13 divides n^15 - n^3 for every integer n. |
proved | 3 | — | #400 Identity Engine (ADR-043) — divisibility family; promoted from candidate backlog (#610). | The integer 910 = 2·5·7·13 divides n^15 - n^3 for every integer n. Not a named mathlib lemma in this form. |
dvd-nine-pow-nine-sub-pow-three — 9 divides n^9 - n^3 for every integer n. |
proved | 3 | — | #400 Identity Engine (ADR-043) — divisibility family. | 9 divides n^9 - n^3 for every integer n. Not a named mathlib lemma in this form. |
dvd-sixty-pow-six-sub-sq — 60 divides n^6 minus n^2 for every integer n. |
proved | 2 | — | #400 Identity Engine (ADR-043) — divisibility family; promoted from candidate backlog (#610). | 60 divides n^6 minus n^2 for every integer n. Not a named mathlib lemma in this form. |
dvd-sixty-pow-ten-sub-sq — 60 divides n^10 minus n^2 for every integer n. |
proved | 2 | — | #400 Identity Engine (ADR-043) — divisibility family; promoted from candidate backlog (#610). | 60 divides n^10 minus n^2 for every integer n. Not a named mathlib lemma in this form. |
dvd-twentyfour-pow-five-sub-pow-three — 24 divides n^5 minus n^3 for every integer n. |
proved | 2 | — | #400 Identity Engine (ADR-043) — divisibility family; promoted from candidate backlog (#610). | 24 divides n^5 minus n^3 for every integer n. Not a named mathlib lemma in this form. |
dvd-twentyfour-pow-seven-sub-pow-five — 24 divides n^7 minus n^5 for every integer n. |
proved | 2 | — | #400 Identity Engine (ADR-043) — divisibility family; promoted from candidate backlog (#610). | 24 divides n^7 minus n^5 for every integer n. Not a named mathlib lemma in this form. |
dvd-twentyfour-pow-six-sub-pow-four — 24 divides n^6 minus n^4 for every integer n. |
proved | 2 | — | #400 Identity Engine (ADR-043) — divisibility family; promoted from candidate backlog (#610). | 24 divides n^6 minus n^4 for every integer n. Not a named mathlib lemma in this form. |
eight-dvd-consecutive-odd-sq-diff — For every integer n, 8 ∣ (2n+3)² − (2n+1)² (difference of consecutive odd squares). |
proved | 2 | — | Classic elementary inequality / number-theory fact (#400 plan Phase 3 — library growth). | For every integer n, 8 ∣ (2n+3)² − (2n+1)² (difference of consecutive odd squares). Not a named mathlib lemma in this concrete form. |
eight-sum-pow-four-ge-sum-pow-four — For all reals a,b, (a+b)⁴ ≤ 8(a⁴+b⁴). |
proved | 3 | — | #400 Identity Engine (ADR-043) — inequalities family. | For all reals a,b, (a+b)⁴ ≤ 8(a⁴+b⁴). Not a named mathlib lemma in this form. |
eight-triangular-add-one-eq-odd-sq — For every natural n, 8·Tₙ + 1 = (2n+1)², where Tₙ = ∑_{i≤n} i is the n-th triangular number; the classic “8T+1 is a perfect (odd) square” test for triangular numbers. |
proved | 2 | — | classic identities (triangular-number gems — compounds on the Gauss sum) | The triangular-number characterisation: m is triangular iff 8m+1 is a perfect square (the forward direction). Conway & Guy, The Book of Numbers; standard recreational/elementary number theory. |
eighth-power-mod-fifteen-mem — Every eighth power is congruent to only 0, 1, 6 or 10 modulo 15. |
proved | 2 | — | #400 Identity Engine (ADR-043) — power-residue family; promoted from candidate backlog (#610). | Every eighth power is congruent to only 0, 1, 6 or 10 modulo 15. Not a named mathlib lemma in this form. |
eighth-power-mod-seventeen-mem — Every natural number’s eighth power is congruent to 0, 1, or 16 modulo 17. |
proved | 3 | — | #400 Identity Engine (ADR-043) — power-residue family; promoted from candidate backlog (#610). | Every natural number’s eighth power is congruent to 0, 1, or 16 modulo 17. Not a named mathlib lemma in this form. |
eighth-power-mod-sixteen-mem — Every eighth power is congruent to only 0 or 1 modulo 16. |
proved | 2 | — | #400 Identity Engine (ADR-043) — power-residue family; promoted from candidate backlog (#610). | Every eighth power is congruent to only 0 or 1 modulo 16. Not a named mathlib lemma in this form. |
eighth-power-mod-thirtytwo-mem — Every eighth power is congruent to only 0 or 1 modulo 32. |
proved | 2 | — | #400 Identity Engine (ADR-043) — power-residue family; promoted from candidate backlog (#610). | Every eighth power is congruent to only 0 or 1 modulo 32. Not a named mathlib lemma in this form. |
eleventh-power-mod-twentythree-mem — Every eleventh power is congruent to only 0, 1 or 22 modulo the prime 23. |
proved | 2 | — | #400 Identity Engine (ADR-043) — power-residue family; promoted from candidate backlog (#610). | Every eleventh power is congruent to only 0, 1 or 22 modulo the prime 23. Not a named mathlib lemma in this form. |
euclid-perfect-numbers — Euclid’s theorem on perfect numbers: if $2^p - 1$ is prime (a Mersenne prime), then $2^{p-1} \cdot (2^p - 1)$ is perfect. |
proved | 3 | — | Euclid, Elements IX.36 | https://en.wikipedia.org/wiki/Euclid%E2%80%93Euler_theorem |
euclid-perfect-numbers-s1 — euclid-perfect-numbers-s1 |
proved | 1 | — | — | — |
euclid-perfect-numbers-s2 — euclid-perfect-numbers-s2 |
proved | 1 | — | — | — |
euclid-perfect-numbers-s3 — euclid-perfect-numbers-s3 |
proved | 1 | — | — | — |
euclid-perfect-numbers-s4 — euclid-perfect-numbers-s4 |
proved | 1 | — | — | — |
euclid-perfect-numbers-s5 — euclid-perfect-numbers-s5 |
proved | 1 | — | — | — |
euclid-perfect-numbers-s6 — euclid-perfect-numbers-s6 |
proved | 1 | — | — | — |
factorial-telescope-sum — For every natural n, the sum over i in 0..n of i * (i!) equals (n+1)! - 1. |
proved | 2 | packet-ready | classic identities | Classic telescoping identity from i·i! = (i+1)! - i!; exercise in Graham, Knuth & Patashnik, Concrete Mathematics, 2nd ed., Ch. 2 (perturbation/telescoping). |
fifth-power-mod-eleven — For every natural number n, the fifth power n⁵ is ≡ 0, 1, or 10 (mod 11) — i.e. 0 or ±1, by Fermat. |
proved | 2 | — | #400 Identity Engine (ADR-043) — power-residue family (Fermat’s little theorem instance). | By Fermat, n⁵ ≡ 0 or ±1 (mod 11); the residues are exactly {0,1,10}. Not a named mathlib lemma. |
fifth-power-mod-sixteen-odd-mem — A fifth power modulo 16 is either 0 or one of the odd residues, and in fact equals n itself modulo 16 up to even classes. |
proved | 3 | — | #400 Identity Engine (ADR-043) — power-residue family; promoted from candidate backlog (#610). | A fifth power modulo 16 is either 0 or one of the odd residues, and in fact equals n itself modulo 16 up to even classes. Not a named mathlib lemma in this form. |
fifth-power-mod-twentyfive-mem — The fifth-power residues modulo 25 are exactly {0,1,7,18,24}. |
proved | 3 | — | #400 Identity Engine (ADR-043) — power-residue family; promoted from candidate backlog (#610). | The fifth-power residues modulo 25 are exactly {0,1,7,18,24}. Not a named mathlib lemma in this form. |
fifth-power-mod-twentytwo-mem — The fifth-power residues modulo 22 are exactly 0, 1, 10, 11, 12, and 21. |
proved | 3 | — | #400 Identity Engine (ADR-043) — power-residue family; promoted from candidate backlog (#610). | The fifth-power residues modulo 22 are exactly 0, 1, 10, 11, 12, and 21. Not a named mathlib lemma in this form. |
forty-two-dvd-pow-seven-sub-self — For every integer n, 42 ∣ n⁷ − n (Fermat: 2,3,7 each divide n⁷−n). |
proved | 2 | — | Classic elementary number theory (library-growth batch, #400 plan Phase 3). | For every integer n, 42 ∣ n⁷ − n (Fermat: 2,3,7 each divide n⁷−n). mathlib has ZMod.pow_card (Fermat) but not these specific named divisibility lemmas. |
four-consecutive-product-add-one-square — For every natural n, the product of four consecutive integers n(n+1)(n+2)(n+3), plus one, is a perfect square. |
proved | 2 | — | Classic elementary-number-theory identity (the “four consecutive integers” square). | n(n+1)(n+2)(n+3) + 1 = (n² + 3n + 1)². mathlib has no lemma that the product of four consecutive integers plus one is square; it is not a named result. |
four-consecutive-product-add-one-square-s1 — four-consecutive-product-add-one-square-s1 |
proved | 1 | — | — | — |
four-consecutive-product-add-one-square-s2 — four-consecutive-product-add-one-square-s2 |
proved | 1 | — | — | — |
four-consecutive-product-add-one-square-s3 — four-consecutive-product-add-one-square-s3 |
proved | 1 | — | — | — |
four-mul-prod-le-sq-sum — For all real a,b, 4ab ≤ (a+b)² (the unnormalized AM-GM kernel). |
proved | 2 | — | Classic elementary real inequality (#400 plan Phase 3 — library growth). | For all real a,b, 4ab ≤ (a+b)² (the unnormalized AM-GM kernel). Not a named mathlib lemma in this concrete polynomial/abs form. |
four-not-dvd-sq-add-two — 4 never divides n^2 + 2, since n^2 mod 4 is 0 or 1. |
proved | 3 | — | #400 Identity Engine (ADR-043) — modular-arith family. | 4 never divides n^2 + 2, since n^2 mod 4 is 0 or 1. Not a named mathlib lemma in this form. |
four-var-cyclic-sos — For all real a,b,c,d, a²+b²+c²+d² ≥ ab+bc+cd+da — the four-variable cyclic sum-of-squares bound. |
proved | 2 | — | Classic real inequality (library-growth batch, #400 plan Phase 3). The project had almost no inequalities; this seeds the SOS/nlinarith family. | For all real a,b,c,d, a²+b²+c²+d² ≥ ab+bc+cd+da — the four-variable cyclic sum-of-squares bound. mathlib has the abstract Cauchy–Schwarz / power-mean lemmas but not this concrete polynomial form as a named lemma. |
four-var-qm-am — For all real a,b,c,d, (a+b+c+d)² ≤ 4(a²+b²+c²+d²) — the 4-variable QM–AM inequality. |
proved | 2 | — | Classic elementary inequality / number-theory fact (#400 plan Phase 3). | For all real a,b,c,d, (a+b+c+d)² ≤ 4(a²+b²+c²+d²) — the 4-variable QM–AM inequality. Not a named mathlib lemma in this form. |
four-var-qm-am-s1 — four-var-qm-am-s1 |
proved | 1 | — | — | — |
four-var-qm-am-s2 — four-var-qm-am-s2 |
proved | 1 | — | — | — |
four-var-qm-am-s3 — four-var-qm-am-s3 |
proved | 1 | — | — | — |
fourth-power-mod-eight-mem — Every fourth power is congruent to 0 or 1 modulo 8. |
proved | 3 | — | #400 Identity Engine (ADR-043) — power-residue family. | Every fourth power is congruent to 0 or 1 modulo 8. Not a named mathlib lemma in this form. |
fourth-power-mod-eighty-mem — Every fourth power is congruent to only 0, 1, 16 or 65 modulo 80. |
proved | 3 | — | #400 Identity Engine (ADR-043) — power-residue family; promoted from candidate backlog. | Every fourth power is congruent to only 0, 1, 16 or 65 modulo 80. Not a named mathlib lemma in this form. |
fourth-power-mod-five — The fourth power of any natural number not divisible by 5 leaves remainder 1 on division by 5: if n % 5 ≠ 0 then n⁴ % 5 = 1. |
proved | 3 | — | classic identities (fourth-power congruence tower — leaf; the Fermat case p=5) | Fermat’s little theorem at the prime 5: a⁴ ≡ 1 (mod 5) for gcd(a,5)=1. Hardy & Wright, An Introduction to the Theory of Numbers. The mod-5 leaf that the others (mod 16, mod 3) do not cover. |
fourth-power-mod-five-mem — Every natural number’s fourth power is congruent to 0 or 1 modulo 5. |
proved | 1 | — | #400 Identity Engine (ADR-043) — power-residue family; promoted from candidate backlog (#610). | Every natural number’s fourth power is congruent to 0 or 1 modulo 5. Not a named mathlib lemma in this form. |
fourth-power-mod-five-s1 — fourth-power-mod-five-s1 |
proved | 1 | — | — | — |
fourth-power-mod-five-s2 — fourth-power-mod-five-s2 |
proved | 1 | — | — | — |
fourth-power-mod-fortyeight-mem — Every fourth power is congruent to only 0, 1, 16 or 33 modulo 48. |
proved | 3 | — | #400 Identity Engine (ADR-043) — power-residue family; promoted from candidate backlog. | Every fourth power is congruent to only 0, 1, 16 or 33 modulo 48. Not a named mathlib lemma in this form. |
fourth-power-mod-hundred-mem — The last two decimal digits of a fourth power are always one of twelve values {00,01,16,21,25,36,41,56,61,76,81,96}. |
proved | 3 | — | #400 Identity Engine (ADR-043) — power-residue family; promoted from candidate backlog. | The last two decimal digits of a fourth power are always one of twelve values {00,01,16,21,25,36,41,56,61,76,81,96}. Not a named mathlib lemma in this form. |
fourth-power-mod-nine-mem — Every fourth power is congruent to 0, 1, 4 or 7 modulo 9. |
proved | 2 | — | #400 Identity Engine (ADR-043) — power-residue family; promoted from candidate backlog (#610). | Every fourth power is congruent to 0, 1, 4 or 7 modulo 9. Not a named mathlib lemma in this form. |
fourth-power-mod-seventeen-mem — The fourth-power residues modulo 17 are exactly {0,1,4,13,16}. |
proved | 3 | — | #400 Identity Engine (ADR-043) — power-residue family; promoted from candidate backlog (#610). | The fourth-power residues modulo 17 are exactly {0,1,4,13,16}. Not a named mathlib lemma in this form. |
fourth-power-mod-sixteen-mem — Every natural number’s fourth power is congruent to 0 or 1 modulo 16. |
proved | 2 | — | #400 Identity Engine (ADR-043) — power-residue family; promoted from candidate backlog (#610). | Every natural number’s fourth power is congruent to 0 or 1 modulo 16. Not a named mathlib lemma in this form. |
fourth-power-mod-ten-mem — The last decimal digit of any fourth power is always 0, 1, 5, or 6. |
proved | 2 | — | #400 Identity Engine (ADR-043) — power-residue family; promoted from candidate backlog (#610). | The last decimal digit of any fourth power is always 0, 1, 5, or 6. Not a named mathlib lemma in this form. |
fourth-power-mod-thirteen-mem — Every fourth power is congruent to 0, 1, 3, or 9 modulo 13 (the quartic residues mod 13). |
proved | 3 | — | #400 Identity Engine (ADR-043) — power-residue family. | Every fourth power is congruent to 0, 1, 3, or 9 modulo 13 (the quartic residues mod 13). Not a named mathlib lemma in this form. |
fourth-power-mod-thirtytwo-mem — Every natural number’s fourth power is congruent to 0, 1, 16, or 17 modulo 32. |
proved | 3 | — | #400 Identity Engine (ADR-043) — power-residue family; promoted from candidate backlog (#610). | Every natural number’s fourth power is congruent to 0, 1, 16, or 17 modulo 32. Not a named mathlib lemma in this form. |
fourth-power-mod-three — The fourth power of any natural number not divisible by 3 leaves remainder 1 on division by 3: if n % 3 ≠ 0 then n⁴ % 3 = 1. |
proved | 2 | — | classic identities (fourth-power congruence tower — leaf; compounds on sq-mod-three) |
Quadratic residues mod 3: n² ≡ 1 (mod 3) for 3∤n, hence n⁴ ≡ 1 (mod 3). Hardy & Wright, An Introduction to the Theory of Numbers. One power up from the proved sq-mod-three. |
fourth-power-mod-twentyfive-mem — Every fourth power modulo 25 lies in the arithmetic-progression set {0,1,6,11,16,21}. |
proved | 2 | — | #400 Identity Engine (ADR-043) — power-residue family; promoted from candidate backlog (#610). | Every fourth power modulo 25 lies in the arithmetic-progression set {0,1,6,11,16,21}. Not a named mathlib lemma in this form. |
gcd-2n1-2n5-dvd-four — The gcd of 2n+1 and 2n+5 always divides 4. |
proved | 2 | — | #400 Identity Engine (ADR-043) — gcd/coprimality family; promoted from candidate backlog (#610). | The gcd of 2n+1 and 2n+5 always divides 4. Not a named mathlib lemma in this form. |
gcd-2n1-2n7-dvd-six — The gcd of 2n+1 and 2n+7 always divides 6. |
proved | 2 | — | #400 Identity Engine (ADR-043) — gcd/coprimality family; promoted from candidate backlog (#610). | The gcd of 2n+1 and 2n+7 always divides 6. Not a named mathlib lemma in this form. |
gcd-2n1-3n4-dvd-five — The gcd of 2n+1 and 3n+4 always divides 5. |
proved | 3 | — | #400 Identity Engine (ADR-043) — gcd/coprimality family; promoted from candidate backlog (#610). | The gcd of 2n+1 and 3n+4 always divides 5. Not a named mathlib lemma in this form. |
gcd-2n3-3n5-eq-one — The linear forms 2n+3 and 3n+5 (determinant 1) are coprime for every n. |
proved | 2 | — | #400 Identity Engine (ADR-043) — gcd/coprimality family; promoted from candidate backlog. | The linear forms 2n+3 and 3n+5 (determinant 1) are coprime for every n. Not a named mathlib lemma in this form. |
gcd-2n3-4n5-dvd-two — The gcd of 2n+3 and 4n+5 always divides 2. |
proved | 3 | — | #400 Identity Engine (ADR-043) — gcd/coprimality family; promoted from candidate backlog (#610). | The gcd of 2n+3 and 4n+5 always divides 2. Not a named mathlib lemma in this form. |
gcd-2n5-3n7-eq-one — The linear forms 2n+5 and 3n+7 are coprime for every natural number n. |
proved | 3 | — | #400 Identity Engine (ADR-043) — gcd/coprimality family; promoted from candidate backlog (#610). | The linear forms 2n+5 and 3n+7 are coprime for every natural number n. Not a named mathlib lemma in this form. |
gcd-2pow-3pow-eq-one — Powers of 2 and powers of 3 with the same exponent are coprime. |
proved | 2 | — | #400 Identity Engine (ADR-043) — gcd/coprimality family; promoted from candidate backlog. | Powers of 2 and powers of 3 with the same exponent are coprime. Not a named mathlib lemma in this form. |
gcd-3n1-5n2-eq-one — The linear forms 3n+1 and 5n+2 (determinant 1) are coprime for every n. |
proved | 2 | — | #400 Identity Engine (ADR-043) — gcd/coprimality family; promoted from candidate backlog. | The linear forms 3n+1 and 5n+2 (determinant 1) are coprime for every n. Not a named mathlib lemma in this form. |
gcd-3n1-9n4-eq-one — The gcd of 3n+1 and 9n+4 is always one. |
proved | 2 | — | #400 Identity Engine (ADR-043) — gcd/coprimality family; promoted from candidate backlog (#610). | The gcd of 3n+1 and 9n+4 is always one. Not a named mathlib lemma in this form. |
gcd-3n2-4n3-eq-one — The linear forms 3n+2 and 4n+3 are coprime for every natural number n. |
proved | 3 | — | #400 Identity Engine (ADR-043) — gcd/coprimality family; promoted from candidate backlog (#610). | The linear forms 3n+2 and 4n+3 are coprime for every natural number n. Not a named mathlib lemma in this form. |
gcd-3n2-5n4-dvd-two — The gcd of 3n+2 and 5n+4 always divides 2. |
proved | 2 | — | #400 Identity Engine (ADR-043) — gcd/coprimality family; promoted from candidate backlog. | The gcd of 3n+2 and 5n+4 always divides 2. Not a named mathlib lemma in this form. |
gcd-3n4-5n7-eq-one — The linear forms 3n+4 and 5n+7 are coprime for every natural number n. |
proved | 3 | — | #400 Identity Engine (ADR-043) — gcd/coprimality family; promoted from candidate backlog (#610). | The linear forms 3n+4 and 5n+7 are coprime for every natural number n. Not a named mathlib lemma in this form. |
gcd-4n1-6n1-dvd-two — The gcd of 4n+1 and 6n+1 always divides 2. |
proved | 3 | — | #400 Identity Engine (ADR-043) — gcd/coprimality family; promoted from candidate backlog (#610). | The gcd of 4n+1 and 6n+1 always divides 2. Not a named mathlib lemma in this form. |
gcd-4n3-5n4-eq-one — The linear forms 4n+3 and 5n+4 (determinant 1) are coprime for every n. |
proved | 2 | — | #400 Identity Engine (ADR-043) — gcd/coprimality family; promoted from candidate backlog. | The linear forms 4n+3 and 5n+4 (determinant 1) are coprime for every n. Not a named mathlib lemma in this form. |
gcd-4n3-6n5-eq-one — The gcd of 4n+3 and 6n+5 is always one. |
proved | 3 | — | #400 Identity Engine (ADR-043) — gcd/coprimality family; promoted from candidate backlog (#610). | The gcd of 4n+3 and 6n+5 is always one. Not a named mathlib lemma in this form. |
gcd-5n2-7n3-eq-one — The gcd of 5n+2 and 7n+3 is always one. |
proved | 3 | — | #400 Identity Engine (ADR-043) — gcd/coprimality family; promoted from candidate backlog (#610). | The gcd of 5n+2 and 7n+3 is always one. Not a named mathlib lemma in this form. |
gcd-5n3-7n4-eq-one — The linear forms 5n+3 and 7n+4 (determinant -1) are coprime for every n. |
proved | 2 | — | #400 Identity Engine (ADR-043) — gcd/coprimality family; promoted from candidate backlog. | The linear forms 5n+3 and 7n+4 (determinant -1) are coprime for every n. Not a named mathlib lemma in this form. |
gcd-6n5-4n3-eq-one — The linear forms 6n+5 and 4n+3 are coprime for every natural number n. |
proved | 3 | — | #400 Identity Engine (ADR-043) — gcd/coprimality family; promoted from candidate backlog (#610). | The linear forms 6n+5 and 4n+3 are coprime for every natural number n. Not a named mathlib lemma in this form. |
gcd-6n5-6n11-eq-one — The values 6n+5 and 6n+11 are coprime for every natural number n. |
proved | 2 | — | #400 Identity Engine (ADR-043) — gcd/coprimality family; promoted from candidate backlog (#610). | The values 6n+5 and 6n+11 are coprime for every natural number n. Not a named mathlib lemma in this form. |
gcd-consec-odd-eq-one — Two consecutive odd numbers 2n+1 and 2n+3 are coprime. |
proved | 3 | — | #400 Identity Engine (ADR-043) — gcd-coprime family. | Two consecutive odd numbers 2n+1 and 2n+3 are coprime. Not a named mathlib lemma in this form. |
gcd-factorial-succ-eq-factorial — The gcd of n! and (n+1)! equals n!, since (n+1)! = (n+1)·n!. |
proved | 3 | — | #400 Identity Engine (ADR-043) — gcd/coprimality family; promoted from candidate backlog (#610). | The gcd of n! and (n+1)! equals n!, since (n+1)! = (n+1)·n!. Not a named mathlib lemma in this form. |
gcd-fib-add-two-eq-gcd-fib-succ — gcd(F_n, F_{n+2}) equals gcd(F_n, F_{n+1}). |
proved | 3 | — | #400 Identity Engine (ADR-043) — gcd/coprimality family; promoted from candidate backlog (#610). | gcd(F_n, F_{n+2}) equals gcd(F_n, F_{n+1}). Not a named mathlib lemma in this form. |
gcd-lin-3n2-5n3 — The linear forms 3n+2 and 5n+3 are coprime for every n. |
proved | 3 | — | #400 Identity Engine (ADR-043) — gcd-coprime family. | The linear forms 3n+2 and 5n+3 are coprime for every n. Not a named mathlib lemma in this form. |
gcd-n-add-six-dvd-six — The gcd of n and n+6 always divides 6. |
proved | 2 | — | #400 Identity Engine (ADR-043) — gcd/coprimality family; promoted from candidate backlog (#610). | The gcd of n and n+6 always divides 6. Not a named mathlib lemma in this form. |
gcd-n-factorial-succ-eq-one — For positive n, n is coprime to n factorial plus one. |
proved | 3 | — | #400 Identity Engine (ADR-043) — gcd/coprimality family; promoted from candidate backlog (#610). | For positive n, n is coprime to n factorial plus one. Not a named mathlib lemma in this form. |
gcd-n1-n4-dvd-three — The gcd of n+1 and n+4 always divides 3. |
proved | 2 | — | #400 Identity Engine (ADR-043) — gcd-coprime family. | The gcd of n+1 and n+4 always divides 3. Not a named mathlib lemma in this form. |
gcd-n1-n7-dvd-six — The gcd of n+1 and n+7 always divides 6. |
proved | 2 | — | #400 Identity Engine (ADR-043) — gcd/coprimality family; promoted from candidate backlog (#610). | The gcd of n+1 and n+7 always divides 6. Not a named mathlib lemma in this form. |
gcd-n2-2n5-eq-one — The gcd of n+2 and 2n+5 is always one. |
proved | 2 | — | #400 Identity Engine (ADR-043) — gcd/coprimality family; promoted from candidate backlog (#610). | The gcd of n+2 and 2n+5 is always one. Not a named mathlib lemma in this form. |
gcd-n2-n4-dvd-two — The gcd of n+2 and n+4 always divides 2. |
proved | 2 | — | #400 Identity Engine (ADR-043) — gcd/coprimality family; promoted from candidate backlog (#610). | The gcd of n+2 and n+4 always divides 2. Not a named mathlib lemma in this form. |
gcd-n2-n6-dvd-four — The gcd of n+2 and n+6 always divides 4. |
proved | 2 | — | #400 Identity Engine (ADR-043) — gcd/coprimality family; promoted from candidate backlog (#610). | The gcd of n+2 and n+6 always divides 4. Not a named mathlib lemma in this form. |
gcd-n2-n8-dvd-six — The gcd of n+2 and n+8 always divides 6. |
proved | 2 | — | #400 Identity Engine (ADR-043) — gcd/coprimality family; promoted from candidate backlog (#610). | The gcd of n+2 and n+8 always divides 6. Not a named mathlib lemma in this form. |
gcd-n2p1-n2p3-dvd-two — The gcd of n^2+1 and n^2+3 always divides 2. |
proved | 2 | — | #400 Identity Engine (ADR-043) — gcd/coprimality family; promoted from candidate backlog. | The gcd of n^2+1 and n^2+3 always divides 2. Not a named mathlib lemma in this form. |
gcd-n3-2n7-eq-one — The linear forms n+3 and 2n+7 are coprime for every natural number n. |
proved | 2 | — | #400 Identity Engine (ADR-043) — gcd/coprimality family; promoted from candidate backlog (#610). | The linear forms n+3 and 2n+7 are coprime for every natural number n. Not a named mathlib lemma in this form. |
gcd-n3p1-np1-eq-np1 — Since n+1 divides n^3+1, the gcd of n^3+1 and n+1 is n+1. |
proved | 2 | — | #400 Identity Engine (ADR-043) — gcd/coprimality family; promoted from candidate backlog. | Since n+1 divides n^3+1, the gcd of n^3+1 and n+1 is n+1. Not a named mathlib lemma in this form. |
gcd-n4p1-n2p1-dvd-two — The gcd of n^4+1 and n^2+1 always divides 2. |
proved | 2 | — | #400 Identity Engine (ADR-043) — gcd/coprimality family; promoted from candidate backlog. | The gcd of n^4+1 and n^2+1 always divides 2. Not a named mathlib lemma in this form. |
gcd-np1-2np1-eq-one — Consecutive-ratio terms n+1 and 2n+1 are always coprime. |
proved | 2 | — | #400 Identity Engine (ADR-043) — gcd/coprimality family; promoted from candidate backlog (#610). | Consecutive-ratio terms n+1 and 2n+1 are always coprime. Not a named mathlib lemma in this form. |
gcd-np1-n2p1-dvd-two — The gcd of n+1 and n^2+1 always divides 2. |
proved | 2 | — | #400 Identity Engine (ADR-043) — gcd/coprimality family; promoted from candidate backlog. | The gcd of n+1 and n^2+1 always divides 2. Not a named mathlib lemma in this form. |
gcd-nsq1-n1-dvd-two — The gcd of n^2+1 and n+1 always divides 2. |
proved | 3 | — | #400 Identity Engine (ADR-043) — gcd/coprimality family; promoted from candidate backlog (#610). | The gcd of n^2+1 and n+1 always divides 2. Not a named mathlib lemma in this form. |
gcd-nsq1-nsq3-dvd-two — The gcd of n^2+1 and n^2+3 always divides 2. |
proved | 2 | — | #400 Identity Engine (ADR-043) — gcd/coprimality family; promoted from candidate backlog (#610). | The gcd of n^2+1 and n^2+3 always divides 2. Not a named mathlib lemma in this form. |
gcd-quad-factored-n1-eq-n1 — Since n^2+3n+2 = (n+1)(n+2), its gcd with n+1 is exactly n+1. |
proved | 3 | — | #400 Identity Engine (ADR-043) — gcd/coprimality family; promoted from candidate backlog (#610). | Since n^2+3n+2 = (n+1)(n+2), its gcd with n+1 is exactly n+1. Not a named mathlib lemma in this form. |
gcd-self-add-dvd — The gcd of n and n+k divides k. |
proved | 2 | — | #400 Identity Engine (ADR-043) — gcd-coprime family. | The gcd of n and n+k divides k. Not a named mathlib lemma in this form. |
gcd-sq-n-sq-n-one — n squared is coprime to n squared plus n plus one. |
proved | 3 | — | #400 Identity Engine (ADR-043) — gcd/coprimality family; promoted from candidate backlog (#610). | n squared is coprime to n squared plus n plus one. Not a named mathlib lemma in this form. |
gcd-three-pow-succ-three-pow-add-one — Three to the n+1 is coprime to three to the n plus one. |
proved | 3 | — | #400 Identity Engine (ADR-043) — gcd/coprimality family; promoted from candidate backlog (#610). | Three to the n+1 is coprime to three to the n plus one. Not a named mathlib lemma in this form. |
gcd-threen-n7-dvd-twentyone — The gcd of 3n and n+7 always divides 21. |
proved | 3 | — | #400 Identity Engine (ADR-043) — gcd/coprimality family; promoted from candidate backlog (#610). | The gcd of 3n and n+7 always divides 21. Not a named mathlib lemma in this form. |
gcd-two-pow-add-one-sub-one-dvd-two — The gcd of 2^n+1 and 2^n-1 always divides 2. |
proved | 3 | — | #400 Identity Engine (ADR-043) — gcd/coprimality family; promoted from candidate backlog (#610). | The gcd of 2^n+1 and 2^n-1 always divides 2. Not a named mathlib lemma in this form. |
gcd-twon-n5-dvd-ten — The gcd of 2n and n+5 always divides 10. |
proved | 3 | — | #400 Identity Engine (ADR-043) — gcd/coprimality family; promoted from candidate backlog (#610). | The gcd of 2n and n+5 always divides 10. Not a named mathlib lemma in this form. |
int-add-neg — Adding the negation of an integer yields zero. |
proved | 1 | — | — | — |
int-neg-neg — Double negation of an integer is the identity. |
proved | 1 | — | — | — |
int-sub-eq-add-neg — Integer subtraction equals adding the negation. |
proved | 1 | — | — | — |
list-reverse-reverse — Reversing a list twice yields the original list. |
proved | 1 | — | — | — |
nat-add-assoc-thm — Addition of natural numbers is associative. |
proved | 1 | — | — | — |
nat-add-comm-thm — Addition of natural numbers is commutative. |
proved | 1 | — | — | — |
nat-add-left-cancel — Left addition is cancellative on the naturals. |
proved | 1 | — | — | — |
nat-add-zero-thm — Zero is a right identity for natural-number addition. |
proved | 1 | — | — | — |
nat-dvd-refl — Divisibility is reflexive on the naturals. |
proved | 1 | — | — | — |
nat-even-or-odd — Every natural number is even or odd. |
proved | 1 | — | — | — |
nat-gcd-comm — The gcd of two naturals is symmetric. |
proved | 1 | — | — | — |
nat-le-add-right — A natural number is at most itself plus another. |
proved | 1 | — | — | — |
nat-le-succ — Every natural number is at most its successor. |
proved | 1 | — | — | — |
nat-mul-add-distrib — Multiplication distributes over addition on the left for naturals. |
proved | 1 | — | — | — |
nat-mul-comm-thm — Multiplication of natural numbers is commutative. |
proved | 1 | — | — | — |
nat-mul-one-thm — One is a right identity for natural-number multiplication. |
proved | 1 | — | — | — |
nat-mul-zero-thm — Any natural number times zero is zero. |
proved | 1 | — | — | — |
nat-sq-lt-two-pow — For every natural n ≥ 5, n² < 2ⁿ — the quadratic-vs-exponential crossover. |
proved | 3 | — | Classic crossover inequality (standard induction exercise) | n² < 2ⁿ for n ≥ 5. mathlib has linear Nat.lt_two_pow-style bounds and Bernoulli (one_add_mul_le_pow) but no quadratic-vs-exponential crossover lemma. |
nat-sq-lt-two-pow-s1 — nat-sq-lt-two-pow-s1 |
proved | 1 | — | — | — |
nat-sq-lt-two-pow-s2-s1 — nat-sq-lt-two-pow-s2-s1 |
proved | 1 | — | — | — |
nat-sq-lt-two-pow-s2-s2 — nat-sq-lt-two-pow-s2-s2 |
proved | 1 | — | — | — |
nat-sq-lt-two-pow-s2-s3 — nat-sq-lt-two-pow-s2-s3 |
proved | 1 | — | — | — |
nat-zero-le — Every natural number is at least zero. |
proved | 1 | — | — | — |
nesbitt-inequality-s2 — nesbitt-inequality-s2 |
proved | 1 | — | — | — |
nesbitt-inequality-s3 — nesbitt-inequality-s3 |
proved | 1 | — | — | — |
nesbitt-inequality-s4 — nesbitt-inequality-s4 |
proved | 1 | — | — | — |
nicomachus-sum-cubes — Nicomachus’s theorem: the sum of the first n cubes equals the square of the sum of the first n naturals. For every natural number n, ∑{k<n} k³ = (∑{k<n} k)². |
proved | 3 | packet-ready | Phase-2 seeded target (pre-ADR-012) | Nicomachus of Gerasa, Introduction to Arithmetic II.20; left as a reader exercise in Mathematics in Lean §5 |
nicomachus-sum-cubes-triangular — For every natural n, the sum over i in 0..n of i^3 equals (n(n+1)/2)^2 (the explicit triangular-number form of Nicomachus’ theorem). |
proved | 3 | packet-ready | Freek 100 / classic | Nicomachus of Gerasa, Introduction to Arithmetic, Book II, in explicit closed form; Graham, Knuth & Patashnik, Concrete Mathematics, §2.5 (∑k^3 = (n(n+1)/2)^2). |
ninth-power-mod-nineteen-mem — Every ninth power is congruent to only 0, 1 or 18 modulo the prime 19. |
proved | 2 | — | #400 Identity Engine (ADR-043) — power-residue family; promoted from candidate backlog (#610). | Every ninth power is congruent to only 0, 1 or 18 modulo the prime 19. Not a named mathlib lemma in this form. |
no-int-sq-eq-eight-mul-add-three — No integer square has the form 8n+3 (squares are 0,1,4 mod 8). |
proved | 3 | — | Classic elementary number theory (library-growth batch, #400 plan Phase 3). | No integer square has the form 8n+3 (squares are 0,1,4 mod 8). mathlib has ZMod.pow_card (Fermat) but not these specific named divisibility lemmas. |
no-nat-sq-eq-two-mul-sq — There are no positive naturals a, b with a² = 2·b² — ¬∃ a b, 0 < b ∧ a² = 2b²: the irrationality of √2 in elementary infinite-descent form. |
proved | 4 | — | Freek 100 (#1, irrationality of √2), infinite-descent / parity form | Classic infinite descent: a²=2b² ⟹ a even ⟹ b even ⟹ a strictly smaller solution. mathlib proves irrational_sqrt_two over ℝ via prime factorisation; this self-contained ℕ descent statement (no reals, no sqrt) is absent and is the elementary heart of Freek #1. |
no-nat-sq-eq-two-mul-sq-s1 — no-nat-sq-eq-two-mul-sq-s1 |
proved | 1 | — | — | — |
no-nat-sq-eq-two-mul-sq-s2 — no-nat-sq-eq-two-mul-sq-s2 |
proved | 1 | — | — | — |
no-nat-sq-eq-two-mul-sq-s3 — no-nat-sq-eq-two-mul-sq-s3 |
proved | 1 | — | — | — |
no-nat-sq-eq-two-mul-sq-s4 — no-nat-sq-eq-two-mul-sq-s4 |
proved | 1 | — | — | — |
not-prime-pow-four-add-four — For every natural n with n > 1, n^4 + 4 is not prime, via the Sophie Germain factorization n^4+4 = (n^2-2n+2)(n^2+2n+2). |
proved | 3 | — | classic identities | Sophie Germain’s identity, compositeness corollary. Sierpiński, Elementary Theory of Numbers (PWN/North-Holland, 1988); standard olympiad result. |
numderangements-add-two-int-form — The derangement count of an (n+2)-set is (n+1) times the sum of the derangement counts of the (n+1)- and n-element sets, stated over the integers. |
proved | 2 | — | #400 Identity Engine (ADR-043) — partition/generating-function family; promoted from candidate backlog. | The derangement count of an (n+2)-set is (n+1) times the sum of the derangement counts of the (n+1)- and n-element sets, stated over the integers. Not a named mathlib lemma in this form. |
odd-fourth-power-mod-sixteen — The fourth power of every odd natural number leaves remainder 1 on division by 16: if n is odd then n⁴ % 16 = 1. |
proved | 2 | — | classic identities (fourth-power congruence tower — leaf; compounds on odd-sq-mod-eight) |
Standard elementary number theory: odd squares are ≡ 1 (mod 8), so odd fourth powers are ≡ 1 (mod 16). Hardy & Wright, An Introduction to the Theory of Numbers (quadratic-residue preliminaries). One power up from the proved odd-sq-mod-eight. |
odd-sq-mod-eight — The square of every odd natural number leaves remainder 1 on division by 8: if n is odd then n^2 % 8 = 1. |
proved | 2 | — | classic identities | Odd squares are ≡ 1 (mod 8); Hardy & Wright, An Introduction to the Theory of Numbers (quadratic-residue preliminaries); standard elementary number theory. |
one-add-four-b-fourth-not-prime — For every natural b > 1, 1 + 4b⁴ is not prime; by the Sophie Germain factorization 1 + 4b⁴ = (2b²+2b+1)(2b²−2b+1), with both factors exceeding 1. |
proved | 3 | — | classic identities (compositeness-via-factorization — the Sophie Germain a=1 corollary) | The a=1 case of Sophie Germain’s identity a⁴+4b⁴ = (a²−2ab+2b²)(a²+2ab+2b²); a companion to the proved not-prime-pow-four-add-four (which is the b=1 case n⁴+4). Sierpiński, Elementary Theory of Numbers. |
one-add-three-x-le-cube — For x ≥ 0, 1+3x ≤ (1+x)³ (a Bernoulli instance, n=3). |
proved | 2 | — | Classic elementary inequality / number-theory fact (#400 plan Phase 3 — library growth). | For x ≥ 0, 1+3x ≤ (1+x)³ (a Bernoulli instance, n=3). Not a named mathlib lemma in this concrete form. |
one-add-two-x-le-sq — For all real x, 1+2x ≤ (1+x)² (the Bernoulli n=2 instance, unconstrained). |
proved | 2 | — | Classic elementary real inequality (#400 plan Phase 3 — library growth). | For all real x, 1+2x ≤ (1+x)² (the Bernoulli n=2 instance, unconstrained). Not a named mathlib lemma in this concrete polynomial/abs form. |
or-comm-imp — Disjunction commutes. |
proved | 1 | — | — | — |
pair-sum-sq-ge-three-abc-sum — The square of the elementary symmetric sum ab+bc+ca is at least 3abc(a+b+c) for all reals (Newton/Maclaurin). |
proved | 2 | — | #400 Identity Engine (ADR-043) — inequality (SOS) family; promoted from candidate backlog. | The square of the elementary symmetric sum ab+bc+ca is at least 3abc(a+b+c) for all reals (Newton/Maclaurin). Not a named mathlib lemma in this form. |
pairwise-product-sum-sq-ge-three-abc-sum — The square of the pairwise-product sum dominates 3abc(a+b+c). |
proved | 3 | — | #400 Identity Engine (ADR-043) — inequality (SOS) family; promoted from candidate backlog (#610). | The square of the pairwise-product sum dominates 3abc(a+b+c). Not a named mathlib lemma in this form. |
pell-brahmagupta-composition-d2 — Brahmagupta composition: multiplying two solutions of x²−2y²=1 via (ac+2be, ae+bc) gives another solution. |
proved | 3 | — | #400 Identity Engine (ADR-043) — Pell-equation family; promoted from candidate backlog (#610). | Brahmagupta composition: multiplying two solutions of x²−2y²=1 via (ac+2be, ae+bc) gives another solution. Not a named mathlib lemma in this form. |
pell-brahmagupta-composition-generic-d — For every parameter d, the Brahmagupta product (ac+dbe, ae+bc) composes two solutions of x²−dy²=1 into a third. |
proved | 3 | — | #400 Identity Engine (ADR-043) — Pell-equation family; promoted from candidate backlog (#610). | For every parameter d, the Brahmagupta product (ac+dbe, ae+bc) composes two solutions of x²−dy²=1 into a third. Not a named mathlib lemma in this form. |
pell-d10-fundamental-ladder-step-preserves — The d=10 fundamental ladder map (x,y) ↦ (19x+60y, 6x+19y), built from the fundamental solution (19,6), preserves x²−10y²=1. |
proved | 2 | — | #400 Identity Engine (ADR-043) — Pell-equation family; promoted from candidate backlog (#610). | The d=10 fundamental ladder map (x,y) ↦ (19x+60y, 6x+19y), built from the fundamental solution (19,6), preserves x²−10y²=1. Not a named mathlib lemma in this form. |
pell-d11-ladder-step-preserves — Applying the fundamental solution (10,3) of x^2-11y^2=1 to any solution yields another solution. |
proved | 2 | — | #400 Identity Engine (ADR-043) — Pell-equation family; promoted from candidate backlog (#610). | Applying the fundamental solution (10,3) of x^2-11y^2=1 to any solution yields another solution. Not a named mathlib lemma in this form. |
pell-d12-ladder-step-preserves — The fundamental solution (7,2) of x^2-12y^2=1 maps any solution to another solution. |
proved | 2 | — | #400 Identity Engine (ADR-043) — Pell-equation family; promoted from candidate backlog (#610). | The fundamental solution (7,2) of x^2-12y^2=1 maps any solution to another solution. Not a named mathlib lemma in this form. |
pell-d13-ladder-step-preserves — The d=13 fundamental ladder map (x,y) ↦ (649x+2340y, 180x+649y), from the large fundamental solution (649,180), preserves x²−13y²=1. |
proved | 3 | — | #400 Identity Engine (ADR-043) — Pell-equation family; promoted from candidate backlog (#610). | The d=13 fundamental ladder map (x,y) ↦ (649x+2340y, 180x+649y), from the large fundamental solution (649,180), preserves x²−13y²=1. Not a named mathlib lemma in this form. |
pell-d14-ladder-step-preserves — The fundamental solution (15,4) of x^2-14y^2=1 preserves the Pell relation under the ladder step. |
proved | 2 | — | #400 Identity Engine (ADR-043) — Pell-equation family; promoted from candidate backlog (#610). | The fundamental solution (15,4) of x^2-14y^2=1 preserves the Pell relation under the ladder step. Not a named mathlib lemma in this form. |
pell-d15-ladder-step-preserves — The fundamental solution (4,1) of x^2-15y^2=1 maps any solution to another solution. |
proved | 2 | — | #400 Identity Engine (ADR-043) — Pell-equation family; promoted from candidate backlog (#610). | The fundamental solution (4,1) of x^2-15y^2=1 maps any solution to another solution. Not a named mathlib lemma in this form. |
pell-d17-ladder-step-preserves — The fundamental solution (33,8) of x^2-17y^2=1 preserves the Pell relation under the ladder step. |
proved | 2 | — | #400 Identity Engine (ADR-043) — Pell-equation family; promoted from candidate backlog (#610). | The fundamental solution (33,8) of x^2-17y^2=1 preserves the Pell relation under the ladder step. Not a named mathlib lemma in this form. |
pell-d18-ladder-step-preserves — The fundamental solution (17,4) of x^2-18y^2=1 maps any solution to another solution. |
proved | 2 | — | #400 Identity Engine (ADR-043) — Pell-equation family; promoted from candidate backlog (#610). | The fundamental solution (17,4) of x^2-18y^2=1 maps any solution to another solution. Not a named mathlib lemma in this form. |
pell-d2-convergent-cross-difference — Consecutive √2-convergents produced by the ladder satisfy the determinant relation p_{n+1}q_n − p_n q_{n+1} = −1. |
proved | 2 | — | #400 Identity Engine (ADR-043) — Pell-equation family; promoted from candidate backlog. | Consecutive √2-convergents produced by the ladder satisfy the determinant relation p_{n+1}q_n − p_n q_{n+1} = −1. Not a named mathlib lemma in this form. |
pell-d2-form-product-telescope-step — The √2 norm form is multiplicative along the ladder: multiplying the form value by the fundamental-unit norm equals the form value of the ladder image. |
proved | 2 | — | #400 Identity Engine (ADR-043) — Pell-equation family; promoted from candidate backlog. | The √2 norm form is multiplicative along the ladder: multiplying the form value by the fundamental-unit norm equals the form value of the ladder image. Not a named mathlib lemma in this form. |
pell-d2-ladder-cross-determinant — For a √2-Pell solution, the cross-determinant of (x,y) with its ladder image (3x+4y, 2x+3y) equals −2. |
proved | 2 | — | #400 Identity Engine (ADR-043) — Pell-equation family; promoted from candidate backlog (#610). | For a √2-Pell solution, the cross-determinant of (x,y) with its ladder image (3x+4y, 2x+3y) equals −2. Not a named mathlib lemma in this form. |
pell-d2-ladder-step-preserves — Applying the fundamental Pell ladder map (x,y) ↦ (3x+4y, 2x+3y) to any solution of x²−2y²=1 yields another solution. |
proved | 2 | — | #400 Identity Engine (ADR-043) — Pell-equation family; promoted from candidate backlog (#610). | Applying the fundamental Pell ladder map (x,y) ↦ (3x+4y, 2x+3y) to any solution of x²−2y²=1 yields another solution. Not a named mathlib lemma in this form. |
pell-d2-negative-seven-ladder-preserves — The same √2 ladder map (x,y) ↦ (3x+4y, 2x+3y) preserves the value −7 in the equation x²−2y²=−7. |
proved | 2 | — | #400 Identity Engine (ADR-043) — Pell-equation family; promoted from candidate backlog (#610). | The same √2 ladder map (x,y) ↦ (3x+4y, 2x+3y) preserves the value −7 in the equation x²−2y²=−7. Not a named mathlib lemma in this form. |
pell-d2-negative-to-positive-step — One half-step (x,y) ↦ (x+2y, x+y) turns a solution of the negative Pell equation x²−2y²=−1 into a solution of x²−2y²=1. |
proved | 2 | — | #400 Identity Engine (ADR-043) — Pell-equation family; promoted from candidate backlog (#610). | One half-step (x,y) ↦ (x+2y, x+y) turns a solution of the negative Pell equation x²−2y²=−1 into a solution of x²−2y²=1. Not a named mathlib lemma in this form. |
pell-d2-no-small-nontrivial-y — There is no solution of x²−2y²=1 with y=1; the smallest positive y is 2 (the fundamental solution). |
proved | 3 | — | #400 Identity Engine (ADR-043) — Pell-equation family; promoted from candidate backlog (#610). | There is no solution of x²−2y²=1 with y=1; the smallest positive y is 2 (the fundamental solution). Not a named mathlib lemma in this form. |
pell-d2-positive-multiple-of-form — Any √2-Pell solution satisfies (x−y)(x+y)=y²+1, a factored form of x²−2y²=1 rearranged. |
proved | 2 | — | #400 Identity Engine (ADR-043) — Pell-equation family; promoted from candidate backlog (#610). | Any √2-Pell solution satisfies (x−y)(x+y)=y²+1, a factored form of x²−2y²=1 rearranged. Not a named mathlib lemma in this form. |
pell-d2-positive-to-negative-step — The same half-step (x,y) ↦ (x+2y, x+y) sends a solution of x²−2y²=1 to a solution of the negative Pell equation x²−2y²=−1. |
proved | 2 | — | #400 Identity Engine (ADR-043) — Pell-equation family; promoted from candidate backlog (#610). | The same half-step (x,y) ↦ (x+2y, x+y) sends a solution of x²−2y²=1 to a solution of the negative Pell equation x²−2y²=−1. Not a named mathlib lemma in this form. |
pell-d2-quad-ladder-step-preserves — The fourth-power solution (99,70) of x^2-2y^2=1 advances any solution four ladder rungs at once. |
proved | 2 | — | #400 Identity Engine (ADR-043) — Pell-equation family; promoted from candidate backlog (#610). | The fourth-power solution (99,70) of x^2-2y^2=1 advances any solution four ladder rungs at once. Not a named mathlib lemma in this form. |
pell-d2-rational-bound-above — Every positive Pell solution of x²−2y²=1 makes x/y exceed √2, i.e. 2y² < x². |
proved | 2 | — | #400 Identity Engine (ADR-043) — Pell-equation family; promoted from candidate backlog (#610). | Every positive Pell solution of x²−2y²=1 makes x/y exceed √2, i.e. 2y² < x². Not a named mathlib lemma in this form. |
pell-d2-rational-bound-gap — The √2-approximation gap is controlled: for a solution of x²−2y²=1 one has x²−2y² ≤ y²+1. |
proved | 2 | — | #400 Identity Engine (ADR-043) — Pell-equation family; promoted from candidate backlog (#610). | The √2-approximation gap is controlled: for a solution of x²−2y²=1 one has x²−2y² ≤ y²+1. Not a named mathlib lemma in this form. |
pell-d2-solution-coords-coprime — In any integer solution of x²−2y²=1 the two coordinates are coprime, since any common divisor squared divides 1. |
proved | 2 | — | #400 Identity Engine (ADR-043) — Pell-equation family; promoted from candidate backlog. | In any integer solution of x²−2y²=1 the two coordinates are coprime, since any common divisor squared divides 1. Not a named mathlib lemma in this form. |
pell-d2-square-doubling-identity — Squaring a solution of x²−2y²=1 via (x²+2y², 2xy) again solves x²−2y²=1. |
proved | 2 | — | #400 Identity Engine (ADR-043) — Pell-equation family; promoted from candidate backlog (#610). | Squaring a solution of x²−2y²=1 via (x²+2y², 2xy) again solves x²−2y²=1. Not a named mathlib lemma in this form. |
pell-d2-square-ladder-step-preserves — The squared fundamental solution (17,12) of x^2-2y^2=1 advances any solution two ladder rungs at once. |
proved | 2 | — | #400 Identity Engine (ADR-043) — Pell-equation family; promoted from candidate backlog (#610). | The squared fundamental solution (17,12) of x^2-2y^2=1 advances any solution two ladder rungs at once. Not a named mathlib lemma in this form. |
pell-d2-stormer-seven-ladder-preserves — The √2 fundamental ladder map (x,y) ↦ (3x+4y, 2x+3y) sends a solution of the Pell-like equation x²−2y²=7 to another solution with the same value 7. |
proved | 2 | — | #400 Identity Engine (ADR-043) — Pell-equation family; promoted from candidate backlog (#610). | The √2 fundamental ladder map (x,y) ↦ (3x+4y, 2x+3y) sends a solution of the Pell-like equation x²−2y²=7 to another solution with the same value 7. Not a named mathlib lemma in this form. |
pell-d2-x-odd — In every integer solution of x²−2y²=1 the x-coordinate is odd. |
proved | 3 | — | #400 Identity Engine (ADR-043) — Pell-equation family; promoted from candidate backlog (#610). | In every integer solution of x²−2y²=1 the x-coordinate is odd. Not a named mathlib lemma in this form. |
pell-d2-x-sq-congr-one-mod-eight — For every integer solution of x²−2y²=1 the x-coordinate satisfies x²≡1 (mod 8), reflecting that x is odd. |
proved | 2 | — | #400 Identity Engine (ADR-043) — Pell-equation family; promoted from candidate backlog. | For every integer solution of x²−2y²=1 the x-coordinate satisfies x²≡1 (mod 8), reflecting that x is odd. Not a named mathlib lemma in this form. |
pell-d2-y-even — The product xy of any integer solution of x²−2y²=1 is even. |
proved | 3 | — | #400 Identity Engine (ADR-043) — Pell-equation family; promoted from candidate backlog (#610). | The product xy of any integer solution of x²−2y²=1 is even. Not a named mathlib lemma in this form. |
pell-d2-y-lt-x-of-pos — Every positive solution of x²−2y²=1 has y strictly less than x. |
proved | 2 | — | #400 Identity Engine (ADR-043) — Pell-equation family; promoted from candidate backlog. | Every positive solution of x²−2y²=1 has y strictly less than x. Not a named mathlib lemma in this form. |
pell-d21-ladder-step-preserves — The fundamental solution (55,12) of x^2-21y^2=1 preserves the Pell relation under the ladder step. |
proved | 2 | — | #400 Identity Engine (ADR-043) — Pell-equation family; promoted from candidate backlog (#610). | The fundamental solution (55,12) of x^2-21y^2=1 preserves the Pell relation under the ladder step. Not a named mathlib lemma in this form. |
pell-d23-ladder-step-preserves — The fundamental solution (24,5) of x^2-23y^2=1 preserves the Pell relation under the ladder step. |
proved | 2 | — | #400 Identity Engine (ADR-043) — Pell-equation family; promoted from candidate backlog (#610). | The fundamental solution (24,5) of x^2-23y^2=1 preserves the Pell relation under the ladder step. Not a named mathlib lemma in this form. |
pell-d3-form-value-ne-two-zmod3 — The form x²−3y² never takes a value congruent to 2 (mod 3), so x²−3y²=2 (and =−1) are unsolvable. |
proved | 2 | — | #400 Identity Engine (ADR-043) — Pell-equation family; promoted from candidate backlog. | The form x²−3y² never takes a value congruent to 2 (mod 3), so x²−3y²=2 (and =−1) are unsolvable. Not a named mathlib lemma in this form. |
pell-d3-fundamental-square-doubling — Squaring a solution of x²−3y²=1 via (x²+3y², 2xy) again solves x²−3y²=1. |
proved | 2 | — | #400 Identity Engine (ADR-043) — Pell-equation family; promoted from candidate backlog (#610). | Squaring a solution of x²−3y²=1 via (x²+3y², 2xy) again solves x²−3y²=1. Not a named mathlib lemma in this form. |
pell-d3-ladder-step-preserves — The d=3 fundamental ladder map (x,y) ↦ (2x+3y, x+2y) sends each solution of x²−3y²=1 to another solution. |
proved | 2 | — | #400 Identity Engine (ADR-043) — Pell-equation family; promoted from candidate backlog (#610). | The d=3 fundamental ladder map (x,y) ↦ (2x+3y, x+2y) sends each solution of x²−3y²=1 to another solution. Not a named mathlib lemma in this form. |
pell-d3-no-negative-solution-zmod3 — The negative Pell equation x²−3y²=−1 has no integer solution, because x²≡2 (mod 3) is impossible. |
proved | 3 | — | #400 Identity Engine (ADR-043) — Pell-equation family; promoted from candidate backlog (#610). | The negative Pell equation x²−3y²=−1 has no integer solution, because x²≡2 (mod 3) is impossible. Not a named mathlib lemma in this form. |
pell-d3-no-small-nontrivial-y — Every positive solution of x²−3y²=1 has y≥1 and x≥2 (the fundamental solution (2,1) is minimal). |
proved | 3 | — | #400 Identity Engine (ADR-043) — Pell-equation family; promoted from candidate backlog (#610). | Every positive solution of x²−3y²=1 has y≥1 and x≥2 (the fundamental solution (2,1) is minimal). Not a named mathlib lemma in this form. |
pell-d3-rational-bound-above — Any positive-index solution of x^2-3y^2=1 satisfies the strict bound 3y^2 < x^2. |
proved | 2 | — | #400 Identity Engine (ADR-043) — Pell-equation family; promoted from candidate backlog (#610). | Any positive-index solution of x^2-3y^2=1 satisfies the strict bound 3y^2 < x^2. Not a named mathlib lemma in this form. |
pell-d3-x-coord-pos-gt-y — Any positive solution of x²−3y²=1 has y strictly less than x. |
proved | 3 | — | #400 Identity Engine (ADR-043) — Pell-equation family; promoted from candidate backlog (#610). | Any positive solution of x²−3y²=1 has y strictly less than x. Not a named mathlib lemma in this form. |
pell-d5-ladder-step-preserves — The d=5 fundamental ladder map (x,y) ↦ (9x+20y, 4x+9y) preserves the Pell relation x²−5y²=1. |
proved | 2 | — | #400 Identity Engine (ADR-043) — Pell-equation family; promoted from candidate backlog (#610). | The d=5 fundamental ladder map (x,y) ↦ (9x+20y, 4x+9y) preserves the Pell relation x²−5y²=1. Not a named mathlib lemma in this form. |
pell-d5-negative-ladder-step-preserves — Applying the d=5 fundamental ladder map (x,y) ↦ (9x+20y, 4x+9y) to a solution of the negative Pell equation x²−5y²=−1 yields another negative solution. |
proved | 2 | — | #400 Identity Engine (ADR-043) — Pell-equation family; promoted from candidate backlog (#610). | Applying the d=5 fundamental ladder map (x,y) ↦ (9x+20y, 4x+9y) to a solution of the negative Pell equation x²−5y²=−1 yields another negative solution. Not a named mathlib lemma in this form. |
pell-d5-positive-from-negative-square — Squaring a solution of the negative Pell equation x²−5y²=−1 produces a solution of the positive equation x²−5y²=1, since (−1)²=1. |
proved | 2 | — | #400 Identity Engine (ADR-043) — Pell-equation family; promoted from candidate backlog. | Squaring a solution of the negative Pell equation x²−5y²=−1 produces a solution of the positive equation x²−5y²=1, since (−1)²=1. Not a named mathlib lemma in this form. |
pell-d6-ladder-step-preserves — The d=6 fundamental ladder map (x,y) ↦ (5x+12y, 2x+5y), from the solution (5,2), preserves x²−6y²=1. |
proved | 2 | — | #400 Identity Engine (ADR-043) — Pell-equation family; promoted from candidate backlog (#610). | The d=6 fundamental ladder map (x,y) ↦ (5x+12y, 2x+5y), from the solution (5,2), preserves x²−6y²=1. Not a named mathlib lemma in this form. |
pell-d7-ladder-step-preserves — The d=7 fundamental ladder map (x,y) ↦ (8x+21y, 3x+8y), from the solution (8,3), preserves x²−7y²=1. |
proved | 2 | — | #400 Identity Engine (ADR-043) — Pell-equation family; promoted from candidate backlog (#610). | The d=7 fundamental ladder map (x,y) ↦ (8x+21y, 3x+8y), from the solution (8,3), preserves x²−7y²=1. Not a named mathlib lemma in this form. |
pell-d7-no-negative-solution-zmod7 — The negative Pell equation x²−7y²=−1 has no integer solution, since 6 is a quadratic non-residue mod 7. |
proved | 2 | — | #400 Identity Engine (ADR-043) — Pell-equation family; promoted from candidate backlog. | The negative Pell equation x²−7y²=−1 has no integer solution, since 6 is a quadratic non-residue mod 7. Not a named mathlib lemma in this form. |
pell-doubling-identity-generic-d — Squaring a fundamental-type solution via (a²+db², 2ab) again solves x²−dy²=1, for any d. |
proved | 3 | — | #400 Identity Engine (ADR-043) — Pell-equation family; promoted from candidate backlog (#610). | Squaring a fundamental-type solution via (a²+db², 2ab) again solves x²−dy²=1, for any d. Not a named mathlib lemma in this form. |
pell-negative-brahmagupta-composition-generic-d — Brahmagupta composition of two solutions of the negative Pell equation x²−dy²=−1 produces a solution of the positive equation x²−dy²=1, since (−1)(−1)=1. |
proved | 2 | — | #400 Identity Engine (ADR-043) — Pell-equation family; promoted from candidate backlog. | Brahmagupta composition of two solutions of the negative Pell equation x²−dy²=−1 produces a solution of the positive equation x²−dy²=1, since (−1)(−1)=1. Not a named mathlib lemma in this form. |
platonic-schlafli-core — For p,q >= 3, the only solutions to 1/p + 1/q > 1/2 are the five Schläfli pairs {3,3},{3,4},{4,3},{3,5},{5,3} — the bounded-arithmetic core of ‘there are exactly five Platonic solids’. |
proved | 4 | packet-ready | Freek 100 (#50) | Freek Wiedijk’s 100 Theorems #50 (The Number of Platonic Solids) — EMPTY in the Lean column (only HOL Light). Euclid, Elements XIII; Coxeter, Regular Polytopes, Ch. 1. The 1/p+1/q>1/2 reduction is… |
platonic-schlafli-core-s1 — platonic-schlafli-core-s1 |
proved | 1 | — | — | — |
platonic-schlafli-core-s1-s1 — platonic-schlafli-core-s1-s1 |
proved | 1 | — | — | — |
platonic-schlafli-core-s1-s1-s1 — platonic-schlafli-core-s1-s1-s1 |
proved | 1 | — | — | — |
platonic-schlafli-core-s1-s1-s2 — platonic-schlafli-core-s1-s1-s2 |
proved | 1 | — | — | — |
platonic-schlafli-core-s1-s2 — platonic-schlafli-core-s1-s2 |
proved | 1 | — | — | — |
platonic-schlafli-core-s1-s3 — platonic-schlafli-core-s1-s3 |
proved | 1 | — | — | — |
platonic-schlafli-core-s2 — platonic-schlafli-core-s2 |
proved | 1 | — | — | — |
platonic-schlafli-core-s2-s1 — platonic-schlafli-core-s2-s1 |
proved | 1 | — | — | — |
platonic-schlafli-core-s2-s2 — platonic-schlafli-core-s2-s2 |
proved | 1 | — | — | — |
platonic-schlafli-core-s2-s3 — platonic-schlafli-core-s2-s3 |
proved | 1 | — | — | — |
platonic-schlafli-core-s3 — platonic-schlafli-core-s3 |
proved | 1 | — | — | — |
platonic-schlafli-core-s4 — platonic-schlafli-core-s4 |
proved | 1 | — | — | — |
pow-four-add-pow-four-ge-cube-mul — For all reals a,b, a⁴+b⁴ ≥ a³b+ab³. |
proved | 2 | — | #400 Identity Engine (ADR-043) — inequalities family. | For all reals a,b, a⁴+b⁴ ≥ a³b+ab³. Not a named mathlib lemma in this form. |
pow-four-add-sq-add-one-factor — For every integer n, n⁴ + n² + 1 = (n² + n + 1)(n² − n + 1); the classic Aurifeuillian-style factorization of x⁴+x²+1 (a product of the two “cyclotomic-like” quadratics). |
proved | 2 | — | classic identities (compositeness-via-factorization — the factorization leaf) | Standard algebra: x⁴+x²+1 = (x²+1)²−x² = (x²+x+1)(x²−x+1). Appears throughout olympiad number theory as the lever for showing n⁴+n²+1 is composite. Engel, Problem-Solving Strategies; Andreescu & Andrica, Number Theory. |
pow-four-add-sq-add-one-not-prime — For every natural n > 1, n⁴ + n² + 1 is not prime; it factors as (n²+n+1)(n²−n+1) with both factors exceeding 1. |
proved | 3 | — | classic identities (compositeness-via-factorization — the capstone; compounds on pow-four-add-sq-add-one-factor) |
Classic olympiad compositeness result, the x⁴+x²+1 analogue of the proved not-prime-pow-four-add-four (Sophie Germain). Engel, Problem-Solving Strategies (divisibility/compositeness). |
prime-fourth-power-mod-240 — The fourth power of every prime p > 5 leaves remainder 1 on division by 240: if p is prime and p > 5 then p⁴ % 240 = 1. |
proved | 4 | — | classic identities (fourth-power congruence tower — root; deps: the mod-16, mod-3, mod-5 leaves) | Classic competition gem “240 ∣ p⁴ − 1 for every prime p > 5”, one power up from the proved-here “24 ∣ p² − 1 for primes p > 3” (binto-labs, prime-sq-mod-twenty-four). 240 = 16·3·5; the result is CRT over the three coprime moduli. Sierpiński, Elementary Theory of Numbers; standard olympiad result. |
prime-sq-mod-twenty-four — The square of every prime p > 3 leaves remainder 1 on division by 24: if p is prime and p > 3 then p^2 % 24 = 1. |
proved | 3 | — | classic identities (thread-B depth-chain mid; deps: odd-sq-mod-eight, sq-mod-three) | Classic chestnut “24 divides p² − 1 for every prime p > 3”; Sierpiński, Elementary Theory of Numbers; standard olympiad/intro-NT result via CRT from the mod-8 and mod-3 facts. |
prime-sq-sub-sq-div-twenty-four — For any two primes p, q both greater than 3, 24 divides p^2 - q^2 (stated over ℤ). |
proved | 2 | — | classic identities (thread-B depth-chain root; deps: prime-sq-mod-twenty-four) | Standard corollary of “p² ≡ 1 (mod 24) for primes p > 3”; Sierpiński, Elementary Theory of Numbers; common olympiad exercise. |
prod-pair-sums-ge-eight-mul — For nonnegative a,b,c, (a+b)(b+c)(c+a) ≥ 8abc. |
proved | 3 | — | #400 Identity Engine (ADR-043) — inequalities family. | For nonnegative a,b,c, (a+b)(b+c)(c+a) ≥ 8abc. Not a named mathlib lemma in this form. |
prod-range-one-add-inv — For all n, ∏_{k=1}^{n} (k+1)/k = n+1 over ℚ — a telescoping product. |
proved | 3 | — | Classic combinatorial / finite-sum identity (library-growth batch, #400 plan Phase 3). | For all n, ∏_{k=1}^{n} (k+1)/k = n+1 over ℚ — a telescoping product. Not a named mathlib lemma (Vandermonde/Pascal are present but not these specific closed forms). |
product-le-quarter-of-sum-one — For nonneg reals a,b with a+b=1, ab ≤ 1/4. |
proved | 2 | — | Classic real inequality (library-growth batch, #400 plan Phase 3). The project had almost no inequalities; this seeds the SOS/nlinarith family. | For nonneg reals a,b with a+b=1, ab ≤ 1/4. mathlib has the abstract Cauchy–Schwarz / power-mean lemmas but not this concrete polynomial form as a named lemma. |
product-of-two-sums-of-squares-ge-square-of-cross — A product of two sums of squares is at least the square of the antisymmetric cross term (Lagrange consequence). |
proved | 2 | — | #400 Identity Engine (ADR-043) — algebraic identity family; promoted from candidate backlog (#610). | A product of two sums of squares is at least the square of the antisymmetric cross term (Lagrange consequence). Not a named mathlib lemma in this form. |
qm-am-three-var — For all real a,b,c, (a+b+c)² ≤ 3(a²+b²+c²) — the QM–AM (power-mean) inequality for three reals. |
proved | 2 | — | Classic real inequality (library-growth batch, #400 plan Phase 3). The project had almost no inequalities; this seeds the SOS/nlinarith family. | For all real a,b,c, (a+b+c)² ≤ 3(a²+b²+c²) — the QM–AM (power-mean) inequality for three reals. mathlib has the abstract Cauchy–Schwarz / power-mean lemmas but not this concrete polynomial form as a named lemma. |
quad-form-divides-cube-sum — The quadratic a²-ab+b² divides the sum of cubes a³+b³. |
proved | 1 | — | #400 Identity Engine (ADR-043) — algebraic identity family; promoted from candidate backlog (#610). | The quadratic a²-ab+b² divides the sum of cubes a³+b³. Not a named mathlib lemma in this form. |
quad-form-ge-three-quarter-sq — The quadratic form a^2+ab+b^2 is at least three quarters of (a+b)^2. |
proved | 2 | — | #400 Identity Engine (ADR-043) — inequality (SOS) family; promoted from candidate backlog (#610). | The quadratic form a^2+ab+b^2 is at least three quarters of (a+b)^2. Not a named mathlib lemma in this form. |
quartic-ge-cross — For all real a,b, a³b+ab³ ≤ a⁴+b⁴ (= (a−b)²(a²+ab+b²) ≥ 0). |
proved | 2 | — | Classic elementary real inequality (#400 plan Phase 3 — library growth). | For all real a,b, a³b+ab³ ≤ a⁴+b⁴ (= (a−b)²(a²+ab+b²) ≥ 0). Not a named mathlib lemma in this concrete polynomial/abs form. |
quartic-ge-sq-prod — For all real a,b, 2a²b² ≤ a⁴+b⁴. |
proved | 2 | — | Classic elementary real inequality (#400 plan Phase 3 — library growth). | For all real a,b, 2a²b² ≤ a⁴+b⁴. Not a named mathlib lemma in this concrete polynomial/abs form. |
quartic-n4-plus-four-dvd-by-shift-quadratic — The quadratic n^2-2n+2 divides n^4+4, the Sophie Germain factorisation at b equal to one. |
proved | 2 | — | #400 Identity Engine (ADR-043) — algebraic identity family; promoted from candidate backlog (#610). | The quadratic n^2-2n+2 divides n^4+4, the Sophie Germain factorisation at b equal to one. Not a named mathlib lemma in this form. |
quartic-x4-plus-64-dvd-by-x2-minus-4x-plus-8 — The quadratic x^2-4x+8 divides x^4+64 (Sophie-Germain factorization with b=2). |
proved | 2 | — | #400 Identity Engine (ADR-043) — algebraic identity family; promoted from candidate backlog (#610). | The quadratic x^2-4x+8 divides x^4+64 (Sophie-Germain factorization with b=2). Not a named mathlib lemma in this form. |
recip-succ-lt-recip — For n ≥ 1, 1/(n+1) < 1/n over ℝ — the harmonic sequence is strictly decreasing. |
proved | 2 | — | Classic elementary inequality / number-theory fact (#400 plan Phase 3 — library growth). | For n ≥ 1, 1/(n+1) < 1/n over ℝ — the harmonic sequence is strictly decreasing. Not a named mathlib lemma in this concrete form. |
shifted-sophie-germain-x4-plus-4-dvd-by-x2-plus-2x-plus-2 — The quadratic x^2+2x+2 divides x^4+4 (one Sophie-Germain factor at b=1). |
proved | 2 | — | #400 Identity Engine (ADR-043) — algebraic identity family; promoted from candidate backlog (#610). | The quadratic x^2+2x+2 divides x^4+4 (one Sophie-Germain factor at b=1). Not a named mathlib lemma in this form. |
shifted-sum-sq-ge-twice-sum-three-var — Each variable’s square plus one dominates twice the variable, summed over three variables. |
proved | 2 | — | #400 Identity Engine (ADR-043) — inequality (SOS) family; promoted from candidate backlog (#610). | Each variable’s square plus one dominates twice the variable, summed over three variables. Not a named mathlib lemma in this form. |
six-dvd-n-mul-succ-mul-two-n-add-one — 6 divides n(n+1)(2n+1) for every integer n (the numerator of ∑k²). |
proved | 2 | — | #400 Identity Engine (ADR-043) — divisibility family. | 6 divides n(n+1)(2n+1) for every integer n (the numerator of ∑k²). Not a named mathlib lemma in this form. |
six-dvd-pow-three-add-five-mul-s1 — six-dvd-pow-three-add-five-mul-s1 |
proved | 1 | — | — | — |
six-dvd-pow-three-add-five-mul-s2 — six-dvd-pow-three-add-five-mul-s2 |
proved | 1 | — | — | — |
six-dvd-pow-three-sub-self — For every integer n, 6 ∣ n³ − n (= n(n−1)(n+1)). |
proved | 2 | — | Classic elementary inequality / number-theory fact (#400 plan Phase 3). | For every integer n, 6 ∣ n³ − n (= n(n−1)(n+1)). Not a named mathlib lemma in this form. |
six-dvd-three-consecutive — For every natural n, 6 ∣ n(n+1)(n+2): the product of three consecutive integers is divisible by 6. |
proved | 2 | — | elementary number theory (product of k consecutive integers is divisible by k!) | Hardy & Wright, An Introduction to the Theory of Numbers, §6 — the k=3 case. mathlib has Nat.factorial_dvd_descFactorial but no standalone 6 ∣ n(n+1)(n+2). |
six-dvd-three-consecutive-int — For every integer n, 6 ∣ n(n+1)(n+2) — divisibility of the product of three consecutive integers, over ℤ. |
proved | 2 | — | Classic elementary number theory (library-growth batch, #400 plan Phase 3). | For every integer n, 6 ∣ n(n+1)(n+2) — divisibility of the product of three consecutive integers, over ℤ. mathlib has ZMod.pow_card (Fermat) but not these specific named divisibility lemmas. |
sixth-power-mod-fourteen-mem — Every natural number’s sixth power is congruent to 0, 1, 7, or 8 modulo 14. |
proved | 2 | — | #400 Identity Engine (ADR-043) — power-residue family; promoted from candidate backlog (#610). | Every natural number’s sixth power is congruent to 0, 1, 7, or 8 modulo 14. Not a named mathlib lemma in this form. |
sixth-power-mod-nine-mem — Every natural number’s sixth power is congruent to 0 or 1 modulo 9. |
proved | 2 | — | #400 Identity Engine (ADR-043) — power-residue family; promoted from candidate backlog (#610). | Every natural number’s sixth power is congruent to 0 or 1 modulo 9. Not a named mathlib lemma in this form. |
sixth-power-mod-nineteen-mem — Every sixth power is congruent to only 0, 1, 7 or 11 modulo the prime 19. |
proved | 2 | — | #400 Identity Engine (ADR-043) — power-residue family; promoted from candidate backlog (#610). | Every sixth power is congruent to only 0, 1, 7 or 11 modulo the prime 19. Not a named mathlib lemma in this form. |
sixth-power-mod-seven — For every natural n, n⁶ % 7 ∈ {0,1} (Fermat). |
proved | 2 | — | #400 Identity Engine (ADR-043) — power-residue family. | For every natural n, n⁶ % 7 ∈ {0,1} (Fermat). Not a named mathlib lemma in this form. |
sixth-power-mod-sixtythree-mem — Every natural number’s sixth power is congruent to 0, 1, 28, or 36 modulo 63. |
proved | 3 | — | #400 Identity Engine (ADR-043) — power-residue family; promoted from candidate backlog (#610). | Every natural number’s sixth power is congruent to 0, 1, 28, or 36 modulo 63. Not a named mathlib lemma in this form. |
sixth-power-mod-thirteen-mem — Every natural number’s sixth power is congruent to 0, 1, or 12 modulo 13. |
proved | 3 | — | #400 Identity Engine (ADR-043) — power-residue family; promoted from candidate backlog (#610). | Every natural number’s sixth power is congruent to 0, 1, or 12 modulo 13. Not a named mathlib lemma in this form. |
sixth-power-mod-thirtyone-mem — Every sixth power modulo the prime 31 lies in the order-5 subgroup {1,2,4,8,16} together with 0. |
proved | 2 | — | #400 Identity Engine (ADR-043) — power-residue family; promoted from candidate backlog (#610). | Every sixth power modulo the prime 31 lies in the order-5 subgroup {1,2,4,8,16} together with 0. Not a named mathlib lemma in this form. |
sixth-power-mod-twentyone-mem — Every natural number’s sixth power is congruent to 0, 1, 7, or 15 modulo 21. |
proved | 2 | — | #400 Identity Engine (ADR-043) — power-residue family; promoted from candidate backlog (#610). | Every natural number’s sixth power is congruent to 0, 1, 7, or 15 modulo 21. Not a named mathlib lemma in this form. |
sophie-germain-factor-dvd — The Sophie Germain factor a²−2ab+2b² always divides a⁴+4b⁴. |
proved | 2 | — | #400 Identity Engine (ADR-043) — algebraic family. | The Sophie Germain factor a²−2ab+2b² always divides a⁴+4b⁴. Not a named mathlib lemma in this form. |
sophie-germain-not-prime — For a≥2, b≥1 the number a⁴+4b⁴ is composite (never prime) via the Sophie Germain factorisation. |
proved | 4 | — | #400 Identity Engine (ADR-043) — algebraic family. | For a≥2, b≥1 the number a⁴+4b⁴ is composite (never prime) via the Sophie Germain factorisation. Not a named mathlib lemma in this form. |
sq-add-sq-eq-three-mul-sq-s1 — sq-add-sq-eq-three-mul-sq-s1 |
proved | 1 | — | — | — |
sq-add-sq-eq-three-mul-sq-s2 — sq-add-sq-eq-three-mul-sq-s2 |
proved | 1 | — | — | — |
sq-add-sq-eq-three-mul-sq-s3 — sq-add-sq-eq-three-mul-sq-s3 |
proved | 1 | — | — | — |
sq-lt-cube-of-one-lt — For x > 1, x² < x³. |
proved | 2 | — | Classic elementary inequality / number-theory fact (#400 plan Phase 3 — library growth). | For x > 1, x² < x³. Not a named mathlib lemma in this concrete form. |
sq-mod-eight-mem — Every natural number’s square leaves remainder 0, 1, or 4 when divided by 8. |
proved | 2 | — | #400 Identity Engine (ADR-043) — power-residue family; promoted from candidate backlog (#610). | Every natural number’s square leaves remainder 0, 1, or 4 when divided by 8. Not a named mathlib lemma in this form. |
sq-mod-eighteen-mem — Every perfect square lies in {0,1,4,7,9,10,13,16} modulo 18. |
proved | 2 | — | #400 Identity Engine (ADR-043) — power-residue family; promoted from candidate backlog (#610). | Every perfect square lies in {0,1,4,7,9,10,13,16} modulo 18. Not a named mathlib lemma in this form. |
sq-mod-eleven-mem — The quadratic residues modulo 11 are exactly {0,1,3,4,5,9}. |
proved | 2 | — | #400 Identity Engine (ADR-043) — power-residue family; promoted from candidate backlog (#610). | The quadratic residues modulo 11 are exactly {0,1,3,4,5,9}. Not a named mathlib lemma in this form. |
sq-mod-fifteen-mem — Every perfect square is congruent to 0, 1, 4, 6, 9, or 10 modulo 15. |
proved | 2 | — | #400 Identity Engine (ADR-043) — power-residue family; promoted from candidate backlog (#610). | Every perfect square is congruent to 0, 1, 4, 6, 9, or 10 modulo 15. Not a named mathlib lemma in this form. |
sq-mod-five — For every natural n, n² % 5 ∈ {0,1,4}. |
proved | 2 | — | #400 Identity Engine (ADR-043) — power-residue family. | For every natural n, n² % 5 ∈ {0,1,4}. Not a named mathlib lemma in this form. |
sq-mod-forty-mem — Every perfect square is congruent to one of 0,1,4,9,16,20,24,25,36 modulo 40. |
proved | 3 | — | #400 Identity Engine (ADR-043) — power-residue family; promoted from candidate backlog (#610). | Every perfect square is congruent to one of 0,1,4,9,16,20,24,25,36 modulo 40. Not a named mathlib lemma in this form. |
sq-mod-fourteen-mem — Every perfect square is congruent to 0, 1, 2, 4, 7, 8, 9 or 11 modulo 14. |
proved | 2 | — | #400 Identity Engine (ADR-043) — power-residue family; promoted from candidate backlog (#610). | Every perfect square is congruent to 0, 1, 2, 4, 7, 8, 9 or 11 modulo 14. Not a named mathlib lemma in this form. |
sq-mod-nine — For every natural n, n² % 9 ∈ {0,1,4,7} (quadratic residues mod 9). |
proved | 2 | — | #400 Identity Engine (ADR-043) — power-residue family. | For every natural n, n² % 9 ∈ {0,1,4,7} (quadratic residues mod 9). Not a named mathlib lemma in this form. |
sq-mod-seven — For every natural n, n² % 7 ∈ {0,1,2,4} (quadratic residues mod 7). |
proved | 2 | — | #400 Identity Engine (ADR-043) — power-residue family. | For every natural n, n² % 7 ∈ {0,1,2,4} (quadratic residues mod 7). Not a named mathlib lemma in this form. |
sq-mod-sixteen-mem — Every natural number’s square is congruent to 0, 1, 4, or 9 modulo 16. |
proved | 2 | — | #400 Identity Engine (ADR-043) — power-residue family; promoted from candidate backlog (#610). | Every natural number’s square is congruent to 0, 1, 4, or 9 modulo 16. Not a named mathlib lemma in this form. |
sq-mod-ten-mem — The last decimal digit of any perfect square is always one of 0, 1, 4, 5, 6, or 9. |
proved | 2 | — | #400 Identity Engine (ADR-043) — power-residue family; promoted from candidate backlog (#610). | The last decimal digit of any perfect square is always one of 0, 1, 4, 5, 6, or 9. Not a named mathlib lemma in this form. |
sq-mod-thirteen-mem — The quadratic residues modulo 13 are exactly {0,1,3,4,9,10,12}. |
proved | 3 | — | #400 Identity Engine (ADR-043) — power-residue family; promoted from candidate backlog (#610). | The quadratic residues modulo 13 are exactly {0,1,3,4,9,10,12}. Not a named mathlib lemma in this form. |
sq-mod-thirtytwo-mem — The quadratic residues modulo 32 are exactly 0, 1, 4, 9, 16, 17, and 25. |
proved | 3 | — | #400 Identity Engine (ADR-043) — power-residue family; promoted from candidate backlog (#610). | The quadratic residues modulo 32 are exactly 0, 1, 4, 9, 16, 17, and 25. Not a named mathlib lemma in this form. |
sq-mod-three — The square of any natural number not divisible by 3 leaves remainder 1 on division by 3: if n % 3 ≠ 0 then n^2 % 3 = 1. |
proved | 2 | — | classic identities (thread-B depth-chain leaf) | Quadratic residues mod 3; Hardy & Wright, An Introduction to the Theory of Numbers (congruence preliminaries); standard elementary number theory. |
sq-mod-twelve-mem — Every natural number’s square is congruent to 0, 1, 4, or 9 modulo 12. |
proved | 2 | — | #400 Identity Engine (ADR-043) — power-residue family; promoted from candidate backlog (#610). | Every natural number’s square is congruent to 0, 1, 4, or 9 modulo 12. Not a named mathlib lemma in this form. |
sq-mod-twenty-mem — Every perfect square is congruent to 0, 1, 4, 5, 9, or 16 modulo 20. |
proved | 2 | — | #400 Identity Engine (ADR-043) — power-residue family; promoted from candidate backlog (#610). | Every perfect square is congruent to 0, 1, 4, 5, 9, or 16 modulo 20. Not a named mathlib lemma in this form. |
sq-mod-twentyfive-mem — Every perfect square modulo the prime-power 25 lies in {0,1,4,6,9,11,14,16,19,21,24}. |
proved | 2 | — | #400 Identity Engine (ADR-043) — power-residue family; promoted from candidate backlog (#610). | Every perfect square modulo the prime-power 25 lies in {0,1,4,6,9,11,14,16,19,21,24}. Not a named mathlib lemma in this form. |
sq-mod-twentyfour-mem — The squares modulo 24 fall in exactly {0,1,4,9,12,16}. |
proved | 3 | — | #400 Identity Engine (ADR-043) — power-residue family; promoted from candidate backlog (#610). | The squares modulo 24 fall in exactly {0,1,4,9,12,16}. Not a named mathlib lemma in this form. |
sq-mod-twentytwo-mem — Every perfect square modulo 22 is one of the twelve quadratic residues {0,1,3,4,5,9,11,12,14,15,16,20}. |
proved | 2 | — | #400 Identity Engine (ADR-043) — power-residue family; promoted from candidate backlog (#610). | Every perfect square modulo 22 is one of the twelve quadratic residues {0,1,3,4,5,9,11,12,14,15,16,20}. Not a named mathlib lemma in this form. |
sq-sum-le-two-mul-sum-sq — For all real a,b, (a+b)² ≤ 2(a²+b²). |
proved | 2 | — | Classic elementary real inequality (#400 plan Phase 3 — library growth). | For all real a,b, (a+b)² ≤ 2(a²+b²). Not a named mathlib lemma in this concrete polynomial/abs form. |
square-of-sum-ge-three-pairwise — For all real a,b,c, (a+b+c)² ≥ 3(ab+bc+ca). |
proved | 2 | — | Classic real inequality (library-growth batch, #400 plan Phase 3). The project had almost no inequalities; this seeds the SOS/nlinarith family. | For all real a,b,c, (a+b+c)² ≥ 3(ab+bc+ca). mathlib has the abstract Cauchy–Schwarz / power-mean lemmas but not this concrete polynomial form as a named lemma. |
square-triangular-pell-link — A square triangular number m²=T_k is equivalent to the Pell solution (2k+1)²−8m²=1, linking T_k to x²−8y²=1. |
proved | 2 | — | #400 Identity Engine (ADR-043) — Pell-equation family; promoted from candidate backlog (#610). | A square triangular number m²=T_k is equivalent to the Pell solution (2k+1)²−8m²=1, linking T_k to x²−8y²=1. Not a named mathlib lemma in this form. |
sum-cubes-ge-sym-quadratic-two-var — For nonnegative a,b, a³+b³ ≥ a²b+ab². |
proved | 2 | — | #400 Identity Engine (ADR-043) — inequalities family. | For nonnegative a,b, a³+b³ ≥ a²b+ab². Not a named mathlib lemma in this form. |
sum-cubes-sym-divisible-by-quadratic — The symmetric quadratic a²+b²+c²-ab-bc-ca divides a³+b³+c³-3abc. |
proved | 2 | — | #400 Identity Engine (ADR-043) — algebraic identity family; promoted from candidate backlog (#610). | The symmetric quadratic a²+b²+c²-ab-bc-ca divides a³+b³+c³-3abc. Not a named mathlib lemma in this form. |
sum-four-pow-ge-sq-prod — For all real a,b,c, a⁴+b⁴+c⁴ ≥ a²b²+b²c²+c²a². |
proved | 2 | — | Classic elementary inequality / number-theory fact (#400 plan Phase 3). | For all real a,b,c, a⁴+b⁴+c⁴ ≥ a²b²+b²c²+c²a². Not a named mathlib lemma in this form. |
sum-four-pow-ge-sq-prod-s1 — sum-four-pow-ge-sq-prod-s1 |
proved | 1 | — | — | — |
sum-four-pow-ge-sq-prod-s2 — sum-four-pow-ge-sq-prod-s2 |
proved | 1 | — | — | — |
sum-four-sq-ge-two-cross — For all real a,b,c,d, a²+b²+c²+d² ≥ 2ab+2cd. |
proved | 2 | — | Classic elementary inequality / number-theory fact (#400 plan Phase 3). | For all real a,b,c,d, a²+b²+c²+d² ≥ 2ab+2cd. Not a named mathlib lemma in this form. |
sum-four-sq-ge-two-cross-s1 — sum-four-sq-ge-two-cross-s1 |
proved | 1 | — | — | — |
sum-four-sq-ge-two-cross-s2 — sum-four-sq-ge-two-cross-s2 |
proved | 1 | — | — | — |
sum-fourth-powers-ge-cube-times-sum — For nonnegative reals, a^3 b + a b^3 is at most a^4 + b^4. |
proved | 2 | — | #400 Identity Engine (ADR-043) — algebraic identity family; promoted from candidate backlog. | For nonnegative reals, a^3 b + a b^3 is at most a^4 + b^4. Not a named mathlib lemma in this form. |
sum-range-choose-mul-two-pow — For every natural n, the sum over k in 0..n of C(n,k)·2ᵏ equals 3ⁿ; the binomial theorem at x=2: ∑C(n,k)2ᵏ = (1+2)ⁿ = 3ⁿ. |
proved | 2 | — | classic identities (binomial-moment tower — the weighted row sum) | Specialisation of the binomial theorem (1+x)ⁿ = ∑C(n,k)xᵏ at x=2. Standard; Concrete Mathematics, Ch. 5. |
sum-range-cube-even — For every natural n, the sum of the cubes of the first n even numbers equals 2n²(n−1)²; i.e. (2·0)³+2³+4³+…+(2(n−1))³ = 2n²(n−1)². |
proved | 2 | — | classic identities (power-sum tower — compounds on nicomachus-sum-cubes) |
Even-cube sums ∑(2k)³ = 8∑k³ = 8·(n(n−1)/2)²; immediate corollary of Nicomachus’s theorem (∑k³ = (∑k)²) scaled by 8. CRC Standard Mathematical Tables (sums of powers); companion of the proved sum-range-cube-odd. |
sum-range-cube-mul-choose — For every natural n, 8·(sum of k³·C(n,k) for k in 0..n) = n²(n+3)·2ⁿ; the third binomial moment ∑k³C(n,k) = n²(n+3)2^(n−3). |
proved | 3 | — | classic identities (binomial-moment tower — compounds on the proved sum-range-sq-mul-choose) |
The third moment of the binomial distribution scaled by 2ⁿ; Graham, Knuth & Patashnik, Concrete Mathematics, Ch. 5 (binomial coefficients / generating-function moments); Riordan, Combinatorial Identities. |
sum-range-cube-odd — For every natural n, the sum of the cubes of the first n odd numbers equals n^2 * (2n^2 - 1); i.e. 1^3 + 3^3 + … + (2n-1)^3 = n^2(2n^2 - 1). |
proved | 2 | — | classic identities | Standard finite-sum identity ∑(2k-1)^3 = n^2(2n^2-1); CRC Standard Mathematical Tables (sums of powers of odd integers); Gradshteyn & Ryzhik, Table of Integrals, Series, and Products (sums section). |
sum-range-fall-mul-choose — For every natural n, 4·(sum of k(k−1)·C(n,k) for k in 0..n) = n(n−1)·2ⁿ; the second falling-factorial moment ∑k(k−1)C(n,k) = n(n−1)2^(n−2). |
proved | 3 | — | classic identities (binomial-moment tower) | Second factorial moment of the binomial distribution; from double absorption k(k−1)C(n,k) = n(n−1)C(n−2,k−2). Graham, Knuth & Patashnik, Concrete Mathematics, Ch. 5. |
sum-range-fib-even-index — For every natural n, ∑{i<n} F(2(i+1)) = F(2n+1) − 1: the sum of the first n even-indexed Fibonacci numbers F₂ + F₄ + ⋯ + F{2n} equals F(2n+1) − 1. |
proved | 3 | — | Fibonacci identities | Vajda (1989), identity (6); Koshy, Thm 5.2. Companion to the odd-index sum sum-range-fib-odd-index, whose result it can reuse. |
sum-range-fib-odd-index — For every natural n, ∑{i<n} F(2i+1) = F(2n): the sum of the first n odd-indexed Fibonacci numbers F₁ + F₃ + ⋯ + F{2n−1} equals F(2n). |
proved | 2 | — | Fibonacci identities | Vajda, Fibonacci & Lucas Numbers and the Golden Section (1989), identity (5); Koshy, Fibonacci and Lucas Numbers with Applications, Thm 5.1. mathlib has single-term Nat.fib_two_mul and the all-index Nat.fib_succ_eq_succ_sum, but no odd-indexed Fibonacci sum. |
sum-range-fib-sq — For every natural n, the sum over i in 0..n of (fib i)^2 equals fib n * fib (n+1) (the telescoping identity F_0^2+…+F_n^2 = F_n F_{n+1}). |
proved | 2 | packet-ready | classic identities | Standard Fibonacci telescoping identity; Koshy, Fibonacci and Lucas Numbers with Applications, §5; Vajda, Fibonacci & Lucas Numbers, and the Golden Section. |
sum-range-id-eq-choose-two — For every natural n, ∑_{i<n} i = C(n, 2): the Gauss sum 0 + 1 + ⋯ + (n−1) equals the binomial coefficient ‘n choose 2’. |
proved | 2 | — | Gauss summation as a binomial coefficient | The handshake identity ∑k = C(n,2); Graham, Knuth & Patashnik, Concrete Mathematics, §1. mathlib has Finset.sum_range_id and Nat.choose_two_right as separate closed forms (both n(n-1)/2) but not the theorem equating them. |
sum-range-mul-two-pow — For every natural n, the sum over i in 0..n-1 of i * 2^i equals (n - 2) * 2^n + 2 (stated over ℤ, where the right side is negative-free for all n). |
proved | 2 | — | classic identities | Arithmetico-geometric sum ∑k·2^k = (n-2)·2^n + 2; Graham, Knuth & Patashnik, Concrete Mathematics, §2.5 (the perturbation-method worked example ∑k·2^k). |
sum-range-odd-eq-sq — For every natural n, the sum over i in 0..n-1 of (2i+1) equals n^2 (i.e. 1+3+5+…+(2n-1) = n^2). |
proved | 1 | packet-ready | classic identities | Classical ‘gnomon’ identity (sum of consecutive odd numbers is a perfect square). Graham, Knuth & Patashnik, Concrete Mathematics, 2nd ed., §2.5; Rosen, Discrete Mathematics and Its Applications, 7th… |
sum-range-pentagonal-closed-form — Closed form for the sum of the first n pentagonal numbers: $2 \sum_{k=0}^n \frac{3k^2-k}{2} = n^2(n+1)$. |
proved | 3 | — | classic figural number identities | Pentagonal number theorem for partial sums of pentagonal numbers. |
sum-range-pow-five-add-pow-seven — For every natural n, (sum of i⁵ for i in 0..n) + (sum of i⁷ for i in 0..n) = 2·(sum of i for i in 0..n)⁴; i.e. ∑k⁵ + ∑k⁷ = 2(∑k)⁴ = 2T⁴ where T = n(n+1)/2 is the n-th triangular number. |
proved | 4 | — | classic identities (power-sum tower — the crown: compounds on sum-range-pow-five-closed-form + sum-range-pow-seven-closed-form) |
A classic Faulhaber curiosity: the sum of the fifth- and seventh-power sums is exactly twice the fourth power of the triangular number, generalising Nicomachus’s ∑k³ = (∑k)² = T² one octave up. Verified ∀ n; see Knuth, “Johann Faulhaber and sums of powers”, Math. Comp. 61 (1993) for the triangular-number structure of odd-power sums. |
sum-range-pow-five-closed-form — For every natural n, 12 * (sum of i^5 for i in 0..n) = n^2 (n+1)^2 (2n^2 + 2n - 1); Faulhaber’s closed form for fifth powers, ∑k^5 = (2n^6 + 6n^5 + 5n^4 - n^2)/12. |
proved | 3 | — | classic identities | Faulhaber’s formula, p = 5 case; Conway & Guy, The Book of Numbers (sums of powers); D. E. Knuth, “Johann Faulhaber and sums of powers”, Math. Comp. 61 (1993); CRC Standard Mathematical Tables. |
sum-range-pow-five-faulhaber-triangular — For every natural n, 3·(sum of i⁵ for i in 0..n) = (sum of i for i in 0..n)²·(4·(sum of i for i in 0..n)−1); i.e. ∑k⁵ = T²(4T−1)/3 where T = ∑k. Faulhaber’s theorem made concrete: the fifth-power sum is a pure polynomial in the triangular number T. |
proved | 3 | — | classic identities (Faulhaber-in-T tower — odd-power rung; compounds on sum-range-pow-five-closed-form) |
Faulhaber’s 1631 result that odd-power sums are polynomials in T = n(n+1)/2: ∑k⁵ = (4T³−T²)/3 = T²(4T−1)/3. Knuth, “Johann Faulhaber and sums of powers”, Math. Comp. 61 (1993). |
sum-range-pow-four-closed-form — For every natural n, 30 * (sum of k^4 for k in 0..n) = n(n+1)(2n+1)(3n^2+3n-1), the integer (ℤ) form of the Faulhaber p=4 identity. |
proved | 2 | packet-ready | classic identities | Faulhaber’s formula, case p=4. Conway & Guy, The Book of Numbers, Ch. 2; Knuth, ‘Johann Faulhaber and sums of powers’, Math. Comp. 61 (1993). |
sum-range-pow-four-triangular-form — For every natural n, 15·(sum of i⁴ for i in 0..n) = (sum of i for i in 0..n)·(2n+1)·(3n²+3n−1); i.e. ∑k⁴ = T(2n+1)(3n²+3n−1)/15 where T = ∑k. |
proved | 3 | — | classic identities (Faulhaber-in-T tower — even-power rung) | Faulhaber’s theorem, even-power case: ∑k⁴ = n(n+1)(2n+1)(3n²+3n−1)/30 = T(2n+1)(3n²+3n−1)/15. Knuth, “Johann Faulhaber and sums of powers”, Math. Comp. 61 (1993); CRC Standard Mathematical Tables. |
sum-range-pow-seven-closed-form — For every natural n, 24·(sum of i⁷ for i in 0..n) = n²(n+1)²(3n⁴+6n³−n²−4n+2); Faulhaber’s closed form for seventh powers, ∑k⁷ = (3n⁸+12n⁷+14n⁶−7n⁴+2n²)/24. |
proved | 4 | — | classic identities (power-sum tower — the harder odd-power rung) | Faulhaber’s formula, p = 7; Conway & Guy, The Book of Numbers; D. E. Knuth, “Johann Faulhaber and sums of powers”, Math. Comp. 61 (1993). Faulhaber’s own result: odd-power sums are polynomials in the triangular number T = n(n+1)/2. |
sum-range-pow-seven-faulhaber-triangular — For every natural n, 3·(sum of i⁷ for i in 0..n) = (sum of i for i in 0..n)²·(6·(sum of i for i in 0..n)²−4·(sum of i for i in 0..n)+1); i.e. ∑k⁷ = T²(6T²−4T+1)/3 where T = ∑k. The seventh-power sum as a pure polynomial in the triangular number. |
proved | 4 | — | classic identities (Faulhaber-in-T tower — the capstone odd-power rung; compounds on sum-range-pow-seven-closed-form) |
Faulhaber’s theorem for p=7: ∑k⁷ = (6T⁴−4T³+T²)/3 = T²(6T²−4T+1)/3. Knuth, “Johann Faulhaber and sums of powers”, Math. Comp. 61 (1993). |
sum-range-pow-six-closed-form — For every natural n, 42·(sum of i⁶ for i in 0..n) = n(n+1)(2n+1)(3n⁴+6n³−3n+1); Faulhaber’s closed form for sixth powers, ∑k⁶ = (6n⁷+21n⁶+21n⁵−7n³+n)/42. |
proved | 3 | — | classic identities (power-sum tower — the next rung above proved p=2..p=5) | Faulhaber’s formula, p = 6; Conway & Guy, The Book of Numbers (sums of powers); D. E. Knuth, “Johann Faulhaber and sums of powers”, Math. Comp. 61 (1993); CRC Standard Mathematical Tables. |
sum-range-pronic — For every natural n, 3 * (sum of i(i+1) for i in 0..n) = n(n+1)(n+2); the sum of the first pronic (oblong) numbers, equivalently 2 * C(n+2, 3). |
proved | 2 | — | classic identities | Pronic/oblong number sums ∑k(k+1) = n(n+1)(n+2)/3; Graham, Knuth & Patashnik, Concrete Mathematics, Ch. 2; CRC Standard Mathematical Tables (figurate numbers). |
sum-range-recip-pronic — For every natural n, the sum over i in 0..n-1 of 1/((i+1)(i+2)) equals n/(n+1) (over ℚ); the classic telescoping sum 1/(1·2) + 1/(2·3) + … + 1/(n(n+1)) = n/(n+1). |
proved | 3 | — | classic identities | Classic telescoping/partial-fractions identity ∑ 1/(k(k+1)) = n/(n+1); Graham, Knuth & Patashnik, Concrete Mathematics, §2.5 (partial fractions); standard first-year analysis exercise. |
sum-range-recip-triangular — For every natural n, ∑_{k<n} 2/((k+1)(k+2)) = 2n/(n+1) over ℚ: the reciprocals of the triangular numbers telescope (∑ 1/T_k → 2). |
proved | 3 | — | telescoping series (reciprocals of triangular numbers) | Standard telescoping series; the sum of reciprocals of all triangular numbers is 2. Companion to sum-range-recip-pronic (1/(k(k+1))) already in the library, sharing the partial-fraction machinery over ℚ. |
sum-range-sq-closed-form — For every natural n, 6 * (sum of i^2 for i in 0..n) = n(n+1)(2n+1), the integer form of 1^2+…+n^2 = n(n+1)(2n+1)/6. |
proved | 2 | packet-ready | classic identities | Faulhaber’s formula, case p=2 (square pyramidal number). Apostol, Calculus Vol. 1, 2nd ed., §I.4.2; Graham, Knuth & Patashnik, Concrete Mathematics, §2.5; Avigad/Massot, Mathematics in Lean, §5… |
sum-range-sq-even — For every natural n, 3 * (sum of (2i)^2 for i in 0..n-1) = 2n(n-1)(2n-1); the sum of the squares of the first n even numbers 0^2 + 2^2 + … + (2n-2)^2 in closed form. |
proved | 2 | — | classic identities | Even-square sums ∑(2k)^2 = 2m(m+1)(2m+1)/3 (here reindexed from 0); CRC Standard Mathematical Tables (sums of powers); companion of the proved sum-range-sq-odd-closed-form. |
sum-range-sq-mul-choose — Weighted sum of squares of binomial coefficients: $4 \sum_{k=0}^n k^2 \binom{n}{k} = n(n+1)2^n$. |
proved | 3 | — | classic combinatorial identities | Standard combinatorial identity for the second moment of binomial coefficients, derived from differentiating the binomial theorem twice. |
sum-range-sq-odd-closed-form — For every natural n, 3 * (sum of (2i+1)^2 for i in 0..n-1) = n(2n-1)(2n+1); i.e. 1^2+3^2+…+(2n-1)^2 = n(2n-1)(2n+1)/3. |
proved | 2 | — | classic identities | Standard finite-sum identity ∑(2k-1)^2 = n(2n-1)(2n+1)/3; Concrete Mathematics §2.5 exercises; Gradshteyn & Ryzhik, Table of Integrals, Series, and Products (sums section). |
sum-range-sq-triangular-form — For every natural n, 3·(sum of i² for i in 0..n) = (sum of i for i in 0..n)·(2n+1); i.e. ∑k² = T·(2n+1)/3 where T = ∑k = n(n+1)/2 is the n-th triangular number. |
proved | 2 | — | classic identities (Faulhaber-in-T tower — power sums as polynomials in the triangular number) | Faulhaber’s theorem: ∑kᵖ is a polynomial in T = n(n+1)/2; the even-power cases carry a factor (2n+1). ∑k² = n(n+1)(2n+1)/6 = T(2n+1)/3. Knuth, “Johann Faulhaber and sums of powers”, Math. Comp. 61 (1993). |
sum-range-three-consecutive-product — For every natural n, 4·∑_{i<n} i(i+1)(i+2) = (n−1)·n·(n+1)·(n+2): the telescoping sum of products of three consecutive integers (the tetrahedral-by-4 closed form). |
proved | 2 | — | falling-factorial telescoping | Graham, Knuth & Patashnik, Concrete Mathematics, §2.6 (summation by parts on falling factorials); ∑_{i=1}^{m} i(i+1)(i+2) = m(m+1)(m+2)(m+3)/4. |
sum-sixth-power-two-var-ge-mixed-fourth-second — The sum of sixth powers of two reals dominates the mixed fourth-second power terms. |
proved | 2 | — | #400 Identity Engine (ADR-043) — algebraic identity family; promoted from candidate backlog (#610). | The sum of sixth powers of two reals dominates the mixed fourth-second power terms. Not a named mathlib lemma in this form. |
sum-sq-add-one-ge-mul-add — For all real x,y, x²+y²+1 ≥ xy+x+y. |
proved | 2 | — | Classic elementary inequality / number-theory fact (#400 plan Phase 3). | For all real x,y, x²+y²+1 ≥ xy+x+y. Not a named mathlib lemma in this form. |
sum-sq-add-three-ge-two-sum — For all real a,b,c, a²+b²+c²+3 ≥ 2(a+b+c). |
proved | 2 | — | Classic elementary inequality / number-theory fact (#400 plan Phase 3). | For all real a,b,c, a²+b²+c²+3 ≥ 2(a+b+c). Not a named mathlib lemma in this form. |
sum-sq-ge-third-sq-sum — The mean-square form: one third of the squared sum is at most the sum of squares (QM-AM in fractional form). |
proved | 2 | — | #400 Identity Engine (ADR-043) — inequality (SOS) family; promoted from candidate backlog (#610). | The mean-square form: one third of the squared sum is at most the sum of squares (QM-AM in fractional form). Not a named mathlib lemma in this form. |
sum-sq-norm-sq-le-twice-sum-fourth — The square of a²+b² is at most twice the sum of fourth powers (power-mean / QM bound). |
proved | 2 | — | #400 Identity Engine (ADR-043) — algebraic identity family; promoted from candidate backlog (#610). | The square of a²+b² is at most twice the sum of fourth powers (power-mean / QM bound). Not a named mathlib lemma in this form. |
sum-sq-prod-ge-mul-sum — For all reals a,b,c, a²b²+b²c²+c²a² ≥ abc(a+b+c). |
proved | 2 | — | #400 Identity Engine (ADR-043) — inequalities family. | For all reals a,b,c, a²b²+b²c²+c²a² ≥ abc(a+b+c). Not a named mathlib lemma in this form. |
sum-three-squares-ge-sum-products — For all real a, b, c, the sum of squares dominates the sum of pairwise products: a² + b² + c² ≥ ab + bc + ca. |
proved | 2 | — | Classic three-variable inequality (a corollary of the rearrangement / sum-of-squares principle). | ab + bc + ca ≤ a² + b² + c². mathlib has inner_mul_le_norm_mul_norm (Cauchy–Schwarz) and sq_nonneg, but no named three-variable “sum of squares ≥ sum of products” lemma. |
tenth-power-mod-eleven-mem — Every tenth power is congruent to only 0 or 1 modulo the prime 11 (Fermat’s little theorem boundary case). |
proved | 2 | — | #400 Identity Engine (ADR-043) — power-residue family; promoted from candidate backlog (#610). | Every tenth power is congruent to only 0 or 1 modulo the prime 11 (Fermat’s little theorem boundary case). Not a named mathlib lemma in this form. |
thirty-dvd-pow-five-sub-self — For every integer n, 30 ∣ n⁵ − n (Fermat: 2,3,5 each divide n⁵−n). |
proved | 2 | — | Classic elementary number theory (library-growth batch, #400 plan Phase 3). | For every integer n, 30 ∣ n⁵ − n (Fermat: 2,3,5 each divide n⁵−n). mathlib has ZMod.pow_card (Fermat) but not these specific named divisibility lemmas. |
three-cubes-div-nine — For every natural n, 9 divides n^3 + (n+1)^3 + (n+2)^3; the sum of any three consecutive cubes is divisible by 9. |
proved | 2 | — | classic identities | Classic introductory number-theory / olympiad exercise; Engel, Problem-Solving Strategies (divisibility chapter); Sierpiński, Elementary Theory of Numbers (PWN/North-Holland, 1988). |
three-dvd-n-cubed-add-two-n — Three always divides n cubed plus twice n. |
proved | 2 | — | #400 Identity Engine (ADR-043) — algebraic identity family; promoted from candidate backlog (#610). | Three always divides n cubed plus twice n. Not a named mathlib lemma in this form. |
twelve-dvd-pow-four-sub-sq — For every integer n, 12 ∣ n⁴ − n². |
proved | 2 | — | Classic elementary inequality / number-theory fact (#400 plan Phase 3). | For every integer n, 12 ∣ n⁴ − n². Not a named mathlib lemma in this form. |
twenty-four-dvd-four-consecutive — For every integer n, 24 ∣ n(n+1)(n+2)(n+3) — the product of four consecutive integers is divisible by 24. |
proved | 2 | — | Classic elementary inequality / number-theory fact (#400 plan Phase 3). | For every integer n, 24 ∣ n(n+1)(n+2)(n+3) — the product of four consecutive integers is divisible by 24. Not a named mathlib lemma in this form. |
two-abs-le-sq-add-one — For all real x, 2 |
proved | 2 | — | Classic elementary real inequality (#400 plan Phase 3 — library growth). | For all real x, 2 Not a named mathlib lemma in this concrete polynomial/abs form. |
two-abs-mul-le-sq-add-sq — For all real a,b, 2 |
proved | 2 | — | Classic elementary real inequality (#400 plan Phase 3 — library growth). | For all real a,b, 2 Not a named mathlib lemma in this concrete polynomial/abs form. |
two-cube-sum-ge-sum-times-sumsq — For nonnegative reals twice the sum of cubes dominates (a+b)(a^2+b^2). |
proved | 3 | — | #400 Identity Engine (ADR-043) — inequality (SOS) family; promoted from candidate backlog (#610). | For nonnegative reals twice the sum of cubes dominates (a+b)(a^2+b^2). Not a named mathlib lemma in this form. |
two-var-sq-add-one-ge-cross-plus-sum — For any two reals a^2+b^2+1 is at least ab + a + b. |
proved | 2 | — | #400 Identity Engine (ADR-043) — inequality (SOS) family; promoted from candidate backlog (#610). | For any two reals a^2+b^2+1 is at least ab + a + b. Not a named mathlib lemma in this form. |
weighted-am-gm-cubed — For nonneg reals x,y, 2x³+y³ ≥ 3x²y — a weighted AM–GM, since 2x³+y³−3x²y = (x−y)²(2x+y). |
proved | 2 | — | Classic real inequality (library-growth batch, #400 plan Phase 3). The project had almost no inequalities; this seeds the SOS/nlinarith family. | For nonneg reals x,y, 2x³+y³ ≥ 3x²y — a weighted AM–GM, since 2x³+y³−3x²y = (x−y)²(2x+y). mathlib has the abstract Cauchy–Schwarz / power-mean lemmas but not this concrete polynomial form as a named lemma. |