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

The Fibonacci companion matrix advances $(F_{n}, F_{n + 1})$

Example

The companion matrix of the Fibonacci recurrence is

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

It satisfies

$C (\binom{F_{n}}{F_{n + 1}}) = (\binom{F_{n + 1}}{F_{n + 2}}), χ_{C} (t) = t^{2} - t - 1,$

and, for $n \geq 1$ ,

$C^{n} = (\begin{array}{cc} F_{n - 1} & F_{n} \\ F_{n} & F_{n + 1} \end{array}) .$

Facts & Assumptions

Given: The Fibonacci recurrence and its row-shift companion matrix.

[L1]

The Fibonacci sequence has initial values $F_{0} = 0, F_{1} = 1$ and recurrence $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]

A recurrence companion matrix advances its state vector and its powers give all later states (The companion matrix advances the recurrence state vector by one step).

[L3]

The characteristic polynomial of an order- $d$ recurrence companion matrix equals the recurrence characteristic polynomial (A recurrence companion matrix has the recurrence characteristic polynomial).

[L4]

The row-shift companion matrix of $t^{d} + c_{1} t^{d - 1} + \dots + c_{d}$ has entries $C_{i, i + 1} = 1$ for $0 \leq i < d - 1$ and $C_{d - 1, j} = - c_{d - j}$ for $0 \leq j < d$ , with all other entries zero (The row-shift companion matrix of a linear recurrence).

Verification

technique · induction

1.1

By [L1] the recurrence is $F_{n + 2} - F_{n + 1} - F_{n} = 0$ , so $d = 2$ and $c_{1} = c_{2} = - 1$ . Unfolding [L4] gives $C_{0, 1} = 1$ , $C_{1, 0} = - c_{2} = 1$ and $C_{1, 1} = - c_{1} = 1$ , with $C_{0, 0} = 0$ , which is the displayed matrix $C$ ; [L2] then gives its state-vector identity.

givenL1L2L4

1.2

At $n = 1$ , the proposed power formula reads $C = (\begin{matrix} F_{0} & F_{1} \\ F_{1} & F_{2} \end{matrix})$ , which follows from [L1].

baseL1

1.3

Multiplying the proposed matrix for $C^{n}$ on the right by $C$ replaces each row $(F_{k - 1}, F_{k})$ by $(F_{k}, F_{k - 1} + F_{k}) = (F_{k}, F_{k + 1})$ using [L1], so it gives the proposed matrix for $C^{n + 1}$ .

ihL1algebra

2.1

By [L3], $χ_{C} (t) = t^{2} - t - 1$ .

step 1.1L3

3.1

Steps 1.2 and 1.3 prove the power identity for every $n \geq 1$ .

step 1.2step 1.3discharge-induction∎

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: 24 results over 6 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

M. Waldschmidt, Linear Recurrence Sequences VI, slides 16-18 (standard reference, not scraped)

The Fibonacci companion matrix advances (Fn,Fn+1)(Fn​,Fn+1​)