Bilateral Fibonacci Lift Classification

Abstract

The bilateral Fibonacci lift is the unique two-line golden eigenlift up to independent component scales.

Theorem 1.1 (The bilateral lift is two-dimensional and componentwise unique).

$$\begin{array}{c}\mathrm{finrank}\left(\mathbb{R},\mathrm{Sol}\left(fibRec\right)\right)=2\wedge \\ \mathrm{Sol}\left(fibRec\right)=\mathrm{span}\left(\mathbb{R},e_{\phi },e_{\psi }\right)\wedge \\ \psi =-\mathrm{inv}\left(\phi \right)\wedge \\ S\left(e_{\phi }\right)=\phi \cdot e_{\phi }\wedge S\left(e_{\psi }\right)=\psi \cdot e_{\psi }\wedge \\ \mathrm{inv}\left(\sqrt{5}\right)\ne 0\wedge -\mathrm{inv}\left(\sqrt{5}\right)\ne 0\wedge \\ (\forall k:\mathbb{N},F\left(k\right)=\frac{e_{\phi }\left(k\right)-e_{\psi }\left(k\right)}{\sqrt{5}})\wedge \\ F\in \mathrm{span}\left(\mathbb{R},e_{\phi },e_{\psi }\right)\wedge (\forall u:\mathrm{Seq}\left(\mathbb{R}\right),u\in \mathrm{span}\left(\mathbb{R},e_{\phi },e_{\psi }\right)\Rightarrow S\left(u\right)\in \mathrm{span}\left(\mathbb{R},e_{\phi },e_{\psi }\right))\wedge \\ (\forall W:\mathrm{Submodule}\left(\mathbb{R},\mathrm{Seq}\left(\mathbb{R}\right)\right),F\in W\wedge (\forall u:\mathrm{Seq}\left(\mathbb{R}\right),u\in W\Rightarrow S\left(u\right)\in W)\Rightarrow \mathrm{span}\left(\mathbb{R},e_{\phi },e_{\psi }\right)\subseteq W)\wedge \\ \mathrm{finrank}\left(\mathbb{R},\mathrm{span}\left(\mathbb{R},e_{\phi },e_{\psi }\right)\right)=2\wedge \\ (\forall u:\mathrm{Seq}\left(\mathbb{R}\right),S\left(u\right)=\phi \cdot u\Rightarrow \exists !a:\mathbb{R},u=a\cdot e_{\phi })\wedge \\ (\forall v:\mathrm{Seq}\left(\mathbb{R}\right),S\left(v\right)=\psi \cdot v\Rightarrow \exists !b:\mathbb{R},v=b\cdot e_{\psi }).\end{array}$$

Proof. Machine-checked in Lean as D5/S1/Recurrence/BilateralLiftClassification.bilateral_lift_classification (✓ std3). ∎

Source. Repository-derived.

Commentary.

The source row phi = (1+sqrt(5))/2 is a definition (not a conjunct).

The public statement retains the solution-space dimension, golden conjugacy identity, shift eigenlaws, nonzero Binet coefficients, least invariant carrier, its dimension, and two independently premised unique component-scalar classifications.

References

• Truth anchor: D5/S1/Recurrence/BilateralLiftClassification.bilateral_lift_classification
• Dependency: D5/S1/Recurrence/BilateralLiftUniqueness