ExampleConstruction: Literature-sourcedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck 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.

Cyclic monomer–domino tilings are counted by Lucas numbers through a matrix trace

Example

Use the two-state Fibonacci graph with transfer matrix

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

A closed state walk of length $n$ encodes a monomer–domino tiling of $n$ cyclically arranged labelled cells, with state $1$ meaning that the next cell is free and state $0$ meaning that it is already covered by a domino started at the preceding cell. With the conventions inherited from closed walks, length zero has two empty boundary states, length one has one monomer tiling, and length two has three tilings. The number of these cyclic tilings is

$tr (C^{n}) = L_{n} (n \geq 0) .$

Consequently,

$\sum_{n \geq 0} L_{n} x^{n} = \frac{2 - x}{1 - x - x^{2}} .$

Facts & Assumptions

Given: The Fibonacci transfer graph and the stated small-size cyclic convention.

[L1]

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

[L2]

The closed-walk series of a transfer matrix is the generating series of the traces of its powers (Closed walks have trace and logarithmic-derivative generating functions).

[L3]

Cayley–Hamilton makes the trace sequence of powers of an invertible $2 \times 2$ matrix satisfy the recurrence given by its characteristic polynomial (For an invertible matrix over a field, Cayley-Hamilton makes every matrix-power entry and trace sequence linearly recurrent).

Verification

technique · closed-walk bijection and recurrence identification

1.1

The transitions $1 \to 1$ , $1 \to 0$ , and $0 \to 1$ respectively place a monomer, start a domino, and finish that domino. Closing the state walk matches the boundary conditions at the marked seam, giving the asserted cyclic-tiling encoding and the stated counts for $n = 0, 1, 2$ .

givenalgebra

1.2

The matrix $C$ is invertible, has characteristic polynomial $t^{2} - t - 1$ , and has $tr (C^{0}) = 2$ and $tr (C) = 1$ . Thus [L3] and [L1] give $tr (C^{n}) = L_{n}$ for every $n \geq 0$ .

L1L3algebra

2.1

By [L2], the cyclic-tiling series is the trace series. Directly, $adj (I - x C)$ has trace $2 - x$ and $\det (I - x C) = 1 - x - x^{2}$ , so the trace formula in [L2] gives the displayed quotient.

step 1.1step 1.2L2algebra∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 43 results over 10 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

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