# Targets

<!-- generated by tools/sourcing/targets_board.py — do not edit by hand -->

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](../README.md#running-an-agent) and [ADR-012](adrs/ADR-012-Backlog-Sourcing.md)).

**216 open · 545 proved · 764 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. |
| `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. |
| `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. |
| `cheb-three-cube-ge-sum-times-sumsq` — Chebyshev's sum inequality (degree three): for nonnegative reals, (a+b+c)(a²+b²+c²) ≤ 3(a³+b³+c³). | open | 3 | — | #400 Identity Engine (ADR-043/ADR-060) — classical 2–3 variable SOS / competition inequalities; promoted from backlog/candidates/sos-inequalities.md. | Chebyshev sum inequality, three-term degree-three instance. Not a named mathlib lemma in this form. |
| `cube-of-sum-le-nine-sum-cubes` — Power-mean inequality (cube form): for nonnegative reals, (a+b+c)³ ≤ 9(a³+b³+c³). | open | 3 | — | #400 Identity Engine (ADR-043/ADR-060) — classical 2–3 variable SOS / competition inequalities; promoted from backlog/candidates/sos-inequalities.md. | Power-mean (cubic) inequality, three-term instance. 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-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. |
| `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. |
| `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. |
| `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. |
| `pairsum-sq-le-three-sum-sq-products` — For all reals, the square of the pairwise-product sum is at most three times the sum of squared pairwise products: (ab+bc+ca)² ≤ 3(a²b²+b²c²+c²a²). | open | 3 | — | #400 Identity Engine (ADR-043/ADR-060) — classical 2–3 variable SOS / competition inequalities; promoted from backlog/candidates/sos-inequalities.md. | Power-mean / Cauchy–Schwarz applied to (ab,bc,ca). 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-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-pair-sums-ge-eight-ninths-sum-prod` — For nonnegative reals, 9(a+b)(b+c)(c+a) ≥ 8(a+b+c)(ab+bc+ca). | open | 4 | — | #400 Identity Engine (ADR-043/ADR-060) — classical 2–3 variable SOS / competition inequalities; promoted from backlog/candidates/sos-inequalities.md. | Classical symmetric product inequality. Not a named mathlib lemma in this form. |
| `quartic-four-var-ge-four-prod` — Four-variable AM–GM on fourth powers: for all reals, a⁴+b⁴+c⁴+d⁴ ≥ 4abcd. | open | 3 | — | #400 Identity Engine (ADR-043/ADR-060) — classical 2–3 variable SOS / competition inequalities; promoted from backlog/candidates/sos-inequalities.md. | Four-variable AM–GM instance. 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-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. |
| `ravi-product-le-abc` — Under the triangle-type nonnegativity conditions a+b−c, b+c−a, c+a−b ≥ 0, the product (a+b−c)(b+c−a)(c+a−b) is at most abc (IMO 1964 Problem 2). | open | 4 | — | #400 Identity Engine (ADR-043/ADR-060) — classical 2–3 variable SOS / competition inequalities; promoted from backlog/candidates/sos-inequalities.md. | IMO 1964 Problem 2 (Ravi-substitution form). Not a named mathlib lemma. |
| `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). |
| `schur-inequality-deg-one` — Schur's inequality of degree one: for nonnegative reals the symmetric sum a(a−b)(a−c)+b(b−a)(b−c)+c(c−a)(c−b) is nonnegative. | open | 4 | — | #400 Identity Engine (ADR-043/ADR-060) — classical 2–3 variable SOS / competition inequalities; promoted from backlog/candidates/sos-inequalities.md. | Schur's inequality, exponent t=1 (a classical named inequality; not in mathlib for ordered fields — mathlib's `schur_*` are the Schur complement / Schur product, unrelated). |
| `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-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-cubes-sq-le-three-sum-sixth` — For all reals, the square of the sum of cubes is at most three times the sum of sixth powers: (a³+b³+c³)² ≤ 3(a⁶+b⁶+c⁶). | open | 3 | — | #400 Identity Engine (ADR-043/ADR-060) — classical 2–3 variable SOS / competition inequalities; promoted from backlog/candidates/sos-inequalities.md. | Power-mean / Cauchy–Schwarz applied to (a³,b³,c³). 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-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-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-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-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-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-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-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-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-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-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-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-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-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-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-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-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-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-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-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-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-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-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-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-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-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-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-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-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-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-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-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-cyclic-quartic-sq` — For all reals, the sum of sixth powers dominates the cyclic sum a⁴b²+b⁴c²+c⁴a²: a⁶+b⁶+c⁶ ≥ a⁴b²+b⁴c²+c⁴a². | open | 3 | — | #400 Identity Engine (ADR-043/ADR-060) — classical 2–3 variable SOS / competition inequalities; promoted from backlog/candidates/sos-inequalities.md. | Cyclic degree-six SOS inequality. 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-sq-times-pairsum-ge-three-abc-sum` — For nonnegative reals, (a²+b²+c²)(ab+bc+ca) ≥ 3abc(a+b+c). | open | 4 | — | #400 Identity Engine (ADR-043/ADR-060) — classical 2–3 variable SOS / competition inequalities; promoted from backlog/candidates/sos-inequalities.md. | Degree-four symmetric inequality. 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-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. |
| `sumsq-times-recip-sq-ge-nine` — For positive reals, (a²+b²+c²)(1/a²+1/b²+1/c²) ≥ 9 (Cauchy–Schwarz on squares). | open | 3 | — | #400 Identity Engine (ADR-043/ADR-060) — classical 2–3 variable SOS / competition inequalities; promoted from backlog/candidates/sos-inequalities.md. | Cauchy–Schwarz / AM–HM applied to a²,b²,c². 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-ge-sum-times-cubes` — Chebyshev's sum inequality (degree four): for nonnegative reals, (a+b+c)(a³+b³+c³) ≤ 3(a⁴+b⁴+c⁴). | open | 3 | — | #400 Identity Engine (ADR-043/ADR-060) — classical 2–3 variable SOS / competition inequalities; promoted from backlog/candidates/sos-inequalities.md. | Chebyshev sum inequality, degree-four instance. 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é). |
| `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). | proved | 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. | proved | 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. | proved | 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-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](upstream/alternating-sum-naturals.md) | 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` — For nonneg reals, 27abc ≤ (a+b+c)³ — AM-GM for three terms (polynomial form). | proved | 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-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` — For positive reals a,b, 4/(a+b) ≤ 1/a + 1/b — the two-variable AM–HM inequality. | proved | 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. |
| `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](https://github.com/agenticsnz/unsorry/issues/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. |
| `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). | proved | 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. | proved | 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-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. | proved | 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-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-three-var-product` — The three-variable Cauchy-Schwarz inequality in product form. | proved | 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. |
| `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-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). | proved | 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. |
| `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-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. | proved | 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. |
| `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. |
| `cyclotomic-five-divides-pow-five-sub-one` — The 5th cyclotomic polynomial n⁴+n³+n²+n+1 divides n⁵-1. | proved | 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. | proved | 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. |
| `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-tetrahedral-eq-triangular` — The difference of two consecutive tetrahedral numbers equals the intervening triangular number. | proved | 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. |
| `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-eleven-sub-pow-three` — 120 divides n^11 minus n^3 for every integer n. | proved | 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-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-1302-pow-thirtyone-sub-self` — The integer 1302 = 2·3·7·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 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. | proved | 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. | proved | 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-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-138-pow-twentythree-sub-self` — 138 divides n^23 - n for every integer n. | proved | 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. | proved | 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. | proved | 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-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-240-pow-nine-sub-pow-five` — 240 divides n^9 minus n^5 for every integer n. | proved | 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. | proved | 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. | proved | 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-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-266-pow-nineteen-sub-self` — The integer 266 = 2·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 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. | proved | 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. | proved | 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. | proved | 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-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-330-pow-twentythree-sub-pow-three` — For every integer n, 330 divides n to the 23rd power minus n to the 3rd power. | proved | 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. | proved | 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-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-fifteen-sub-pow-three` — The integer 455 = 5·7·13 divides n^15 - n^3 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^15 - n^3 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-504-pow-nine-sub-pow-three` — 504 divides n^9 minus n^3 for every integer n. | proved | 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. | proved | 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. | proved | 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. | proved | 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-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-510-pow-thirtythree-sub-pow-seventeen` — For every integer n, 510 divides n to the 33rd power minus n to the 17th power. | proved | 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. | proved | 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. | proved | 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. | proved | 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-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-thirtyone-sub-pow-eleven` — 66 divides n^31 - n^11 for every integer n. | proved | 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-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-6765-pow-fortyone-sub-self` — For every integer n, 6765 divides n raised to the 41st power minus n. | proved | 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-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-840-pow-fifteen-sub-pow-three` — The integer 840 = 2^3·3·5·7 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 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. | proved | 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. | proved | 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-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-910-pow-thirteen-sub-self` — The integer 910 = 2·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 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. | proved | 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. | proved | 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-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-sixteen-odd-pow-four-sub-one` — For every odd integer n, 16 divides n^4 minus 1. | proved | 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-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. |
| `eisenstein-norm-multiplicative` — The set of Loeschian numbers x²+xy+y² (Eisenstein integer norms) is closed under multiplication. | proved | 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. |
| `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](upstream/factorial-telescope-sum.md) | classic identities | Classic telescoping identity from i·i! = (i+1)! - i!; exercise in Graham, Knuth & Patashnik, Concrete Mathematics, 2nd ed., Ch. 2 (perturbation/telescoping). |
| `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. | proved | 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. | proved | 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. | proved | 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. | proved | 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. | proved | 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). | proved | 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)ⁿ. | proved | 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-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). | proved | 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. | proved | 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. |
| `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 | — | — | — |
| `lcm-self-succ` — The lcm of n and n+1 is their product n(n+1). | proved | 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. |
| `list-reverse-reverse` — Reversing a list twice yields the original list. | proved | 1 | — | — | — |
| `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). | proved | 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. |
| `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](upstream/nicomachus-sum-cubes.md) | 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](upstream/nicomachus-sum-cubes-triangular.md) | 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. |
| `one-hundred-twenty-dvd-five-consecutive` — 120 = 5! divides the product of any five consecutive integers. | proved | 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. |
| `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](upstream/platonic-schlafli-core.md) | 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-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). | proved | 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-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). |
| `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)). | proved | 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. |
| `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-sum-ge-abc-times-sum` — The sum of fourth powers of three reals dominates abc times their sum a+b+c. | proved | 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-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-centered-cube-eq-biquadratic` — Twice the sum over k<n of k^3+(k+1)^3 equals n^2 times (n^2+1). | proved | 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. | proved | 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). | proved | 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). | proved | 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. | proved | 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-running-closed-form` — The running sum of twice-centered-triangular terms 3k^2+3k+2 equals n(n^2+1). | proved | 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). | proved | 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-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-decagonal-numbers-closed-form` — Six times the running sum of the first n decagonal numbers k(4k-3) equals n(n+1)(8n-5). | proved | 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). | proved | 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. | proved | 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). | proved | 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). | proved | 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. | proved | 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-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-eq` — Thirty times the sum of fourth powers k^4 over range n equals the Faulhaber quartic closed form. | proved | 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-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-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. | proved | 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-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. | proved | 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-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)). | proved | 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-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)). | proved | 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)². | proved | 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-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). | proved | 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-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)). | proved | 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)). | proved | 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)). | proved | 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-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). | proved | 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). | proved | 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-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). | proved | 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. | proved | 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-k-add-one-mul-two-pow` — The sum over k<n of (k+1)·2^k equals (n−1)·2^n + 1. | proved | 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). | proved | 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). | proved | 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). | proved | 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-two-pow` — The sum over k<n of k²·2^k equals (n²−4n+6)·2^n − 6. | proved | 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-numbers-closed-form` — Three times the running sum of the first n nonagonal numbers (as k(7k-5)) equals n(n+1)(7n-4). | proved | 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). | proved | 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-numbers-closed-form` — Twice the running sum of the first n octagonal numbers k(3k-2) equals n(n+1)(2n-1). | proved | 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-octahedral-numbers-closed-form` — Six times the sum of the first n octahedral numbers equals 3n(n+1)(n^2+n+1). | proved | 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-squares-eq` — Three times the sum of the first n odd squares (2k+1)^2 equals n(2n-1)(2n+1). | proved | 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-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). | proved | 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-pentatope-triple-product` — Four times the sum of three consecutive integer products equals n(n+1)(n+2)(n+3), the pentatope closed form. | proved | 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-quadruple-product-closed-form` — Five times the sum of four consecutive integer products equals the five-term product n through n+4. | proved | 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-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-diff-eq-cube` — The sum of (3k²+3k+1) for k from 0 to n-1 equals n³. | proved | 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-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-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. | proved | 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-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](upstream/sum-range-fib-sq.md) | classic identities | Standard Fibonacci telescoping identity; Koshy, Fibonacci and Lucas Numbers with Applications, §5; Vajda, Fibonacci & Lucas Numbers, and the Golden Section. |
| `sum-range-four-cube-diff-eq` — The sum of (4k³+6k²+4k+1) for k from 0 to n-1 equals n⁴. | proved | 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-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. | proved | 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-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-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. | proved | 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. | proved | 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-closed` — Four times the sum of k times three-to-the-k over k below n equals (2n-3)3^n+3. | proved | 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-mul-two-pow-eq` — The sum of k·2^k for k from 0 to n-1 equals (n−2)·2ⁿ + 2. | proved | 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-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. | proved | 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. | proved | 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-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](upstream/sum-range-odd-eq-sq.md) | 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-odd-mul-three-pow` — The sum of (2i+1)·3^i over i below n, plus 3^n, equals n·3^n + 1. | proved | 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-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](upstream/sum-range-pow-four-closed-form.md) | 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-recip-two-pow` — The partial geometric sum of 1/2^i over i below n equals 2 − 2/2^n. | proved | 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-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. | proved | 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-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](upstream/sum-range-sq-closed-form.md) | 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-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. | proved | 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-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-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. | proved | 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-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-stella-octangula-closed-form` — Twice the running sum of stella octangula numbers k(2k^2-1) equals n(n+1)(n^2+n-1). | proved | 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-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. |