ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-16

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.

Monomer–domino tilings of a board give the Fibonacci recurrence and transfer matrix

Example

Let $T_{n}$ be the number of tilings of a row of $n$ labelled cells by monomers of length one and dominoes of length two. Then

$T_{n} = F_{n + 1}, \sum_{n \geq 0} T_{n} x^{n} = \frac{1}{1 - x - x^{2}} .$

Equivalently, with states $0$ (the current cell is already covered from the left) and $1$ (the current cell is free), the transfer matrix is

$C = (\begin{array}{cc} 0 & 1 \\ 1 & 1 \end{array}),$

and $T_{n} = (C^{n})_{11}$ .

Facts & Assumptions

Given: Linear boards tiled by monomers and dominoes, including the empty tiling at length zero.

[L1]

The Fibonacci sequence is determined by $F_{0} = 0$ , $F_{1} = 1$ , and $F_{n + 2} = F_{n + 1} + F_{n}$ (The Fibonacci sequence $F_{0} = 0, F_{1} = 1$ and Lucas sequence $L_{0} = 2, L_{1} = 1$ ).

[L2]

The $(u, v)$ entry of the $n$ th power of a transfer matrix counts length- $n$ walks from $u$ to $v$ when all edge weights are one (The $(u, v)$ entry of $A^{n}$ is the total weight of length- $n$ walks from $u$ to $v$ ).

[L3]

A fixed-entry walk generating series is the corresponding cofactor of $I - x C$ divided by $\det (I - x C)$ (Transfer-matrix theorem: weighted-walk generating functions are cofactors of $I - x A$ divided by $\det (I - x A)$ ).

Verification

technique · last-tile decomposition and transfer bijection

1.1givenalgebra

There is one empty tiling and one one-cell tiling, so $T_{0} = T_{1} = 1$ . For $n \geq 2$ , the last tile is uniquely a monomer after a tiling of length $n - 1$ or a domino after one of length $n - 2$ , so $T_{n} = T_{n - 1} + T_{n - 2}$ .

1.2L2algebra

In the two-state encoding, $1 \to 1$ places a monomer, $1 \to 0$ starts a domino, and $0 \to 1$ completes it. Thus board tilings are in bijection with length- $n$ walks from state $1$ back to state $1$ , and [L2] gives $T_{n} = (C^{n})_{11}$ .

2.1step 1.1L1algebra

Comparing the initial values and recurrence in step 1.1 with [L1] gives $T_{n} = F_{n + 1}$ for every $n \geq 0$ .

3.1step 1.2L3algebra∎

Since $I - x C = (\begin{matrix} 1 & - x \\ - x & 1 - x \end{matrix})$ has determinant $1 - x - x^{2}$ and the relevant cofactor is $1$ , [L3] gives the displayed generating function.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

14 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

R. P. Stanley, Enumerative Combinatorics, vol. 1, 2nd ed., Example 4.7.16 (standard reference, not scraped)