ExampleConstruction: AI-adaptedVerification: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-29

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Five-card hands from a $52$ -card deck: $(\binom{52}{5}) = 2598960$ , and the count of hands with all cards of one suit

Example

Model a deck as the set $D : = 13 \times 4$ , a rank paired with a suit, so $∣ D ∣ = 52$ by The product rule: $∣ A \times B ∣ = ∣ A ∣ ∣ B ∣$ , and $∣ \prod_{i < m} A_{i} ∣ = \prod_{i < m} ∣ A_{i} ∣$ . A hand is a five-element subset of $D$ , that is an element of $[D]^{5}$ . Then

$∣ [D]^{5} ∣ = (\binom{52}{5}) = 2598960,$

and the number of hands all of whose cards share a suit is

$4 \cdot (\binom{13}{5}) = 4 \cdot 1287 = 5148.$

No probability is claimed anywhere. There is no probability space in this library at this point in the reading order; these are counts of sets, and nothing below divides one by another or calls a count a chance.

Facts & Assumptions

Given: The deck $D = 13 \times 4$ ; for $s < 4$ the suit $D_{s} : = 13 \times {s}$ ; and the falling factorials computed from $n^{\underline{0}} = 1$ and $n^{\underline{σ (k)}} = n^{\underline{k}} (n - k)$ (The factorial $n!$ and the falling factorial $n^{\underline{k}}$ , defined by recursion in $N$ ).

[L1]

$∣ [X]^{k} ∣ = (\binom{∣ X ∣}{k})$ (The set $[A]^{k}$ of $k$ -element subsets and the binomial coefficient $(\binom{n}{k}) : = ∣ [n]^{k} ∣$ , The cardinality $∣ A ∣$ of a finite set).

[L2]

$(\binom{n}{k}) k! = n^{\underline{k}}$ for $k \leq n$ ( $(\binom{n}{k}) k! (n - k)! = n!$ for $k \leq n$ ; hence $(\binom{n}{k}) k! = n^{\underline{k}}$ , the quotient $n! / (k! (n - k)!)$ is a natural number, and $(\binom{n}{k}) = (\binom{n}{n - k})$ , clause 1), and $5! = 120$ (The factorial $n!$ and the falling factorial $n^{\underline{k}}$ , defined by recursion in $N$ ).

[L3]

The product rule (The product rule: $∣ A \times B ∣ = ∣ A ∣ ∣ B ∣$ , and $∣ \prod_{i < m} A_{i} ∣ = \prod_{i < m} ∣ A_{i} ∣$ ) and the sum rule for a partition indexed by a finite set, with $\sum_{i \in S} c = ∣ S ∣ c$ (The sum rule: a finite disjoint union is finite with $∣ A \cup B ∣ = ∣ A ∣ + ∣ B ∣$ and $∣ ⋃_{i \in I} A_{i} ∣ = \sum_{i \in I} ∣ A_{i} ∣$ , and a sum over a finite index set splits along a partition, The sum $\sum_{i \in S} a_{i}$ over a finite index set, and its product form).

[L4]

Cancellation by a nonzero natural (Cancellation for multiplication by a nonzero factor).

Verification

technique · direct

1.1givenL1L3

The deck has $∣ D ∣ = ∣ 13 ∣ \cdot ∣ 4 ∣ = 13 \cdot 4 = 52$ by [L3], and a hand is by definition an element of $[D]^{5}$ , so the number of hands is $(\binom{52}{5})$ by [L1].

2.1step 1.1L2L4

The total. By [L2], $(\binom{52}{5}) \cdot 5! = 52^{\underline{5}} = 52 \cdot 51 \cdot 50 \cdot 49 \cdot 48$ . Computing the falling factorial step by step: $52 \cdot 51 = 2652$ , $2652 \cdot 50 = 132600$ , $132600 \cdot 49 = 6497400$ , $6497400 \cdot 48 = 311875200$ . Since $5! = 120$ and $120 \cdot 2598960 = 311875200$ , cancellation by $120$ gives $(\binom{52}{5}) = 2598960$ .

2.2step 1.1L1L2L3L4

The single-suit hands. Let $F$ be the set of hands all of whose cards lie in one suit, and for $s < 4$ let $F_{s}$ be the set of hands contained in $D_{s}$ . The $F_{s}$ are pairwise disjoint, since a hand has five cards and cannot lie in two different suits at once, and their union is $F$ . Each $D_{s} = 13 \times {s}$ is in bijection with $13$ under the first projection, so $∣ F_{s} ∣ = ∣ [D_{s}]^{5} ∣ = (\binom{13}{5})$ by [L1]. By [L2], $(\binom{13}{5}) \cdot 120 = 13^{\underline{5}} = 13 \cdot 12 \cdot 11 \cdot 10 \cdot 9 = 154440$ , and $120 \cdot 1287 = 154440$ , so $(\binom{13}{5}) = 1287$ . Finally [L3] gives $∣ F ∣ = \sum_{s \in 4} ∣ F_{s} ∣ = 4 \cdot 1287 = 5148$ .

3.1step 2.1step 2.2∎

So there are $2598960$ hands in all, of which $5148$ have all five cards of one suit. Both numbers are cardinalities of explicitly described sets, and neither is a probability.

Remarks

The sum rule is doing real work in step 2.2, and its hypothesis is checked rather than assumed: two different suits share no card, so the four blocks are disjoint. Without that, adding the four counts would overcount, which is the failure this page's counterexample exhibits.
What is deliberately absent. Turning $5148 / 2598960$ into a probability needs a probability space, which the library does not have here. The temptation to write one down is exactly the place a worked example smuggles in machinery it has not got.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

40 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Poker probability (Wikipedia) (standard reference, not scraped)
Combination (Wikipedia) (standard reference, not scraped)
Binomial coefficient (Wikipedia) (standard reference, not scraped)

Five-card hands from a 5252-card deck: (525)=2598960(552​)=2598960, and the count of hands with all cards of one suit