Bilateral Fibonacci Lift Uniqueness

Abstract

Fibonacci solutions split into two golden eigenlines with a minimal cyclic carrier.

Theorem 1.1 (Bilateral lift uniqueness).

$$\mathrm{Sol}(F)=⟨e_{\phi },e_{\psi }⟩,S{e}_{\lambda }=\lambda e_{\lambda },F_{k+1}=\frac{{\phi }^{k+1}-{\psi }^{k+1}}{\sqrt{5}},⟨F{⟩}_S=⟨e_{\phi },e_{\psi }⟩.$$

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

Source. Repository-derived.

Commentary.

The aggregate theorem packages the two-dimensional recurrence space, both shift eigenlines, Binet decomposition, cyclic minimality, and the exact contracting residual into one kernel-checked statement.

Theorem 1.2 (Golden decomposition of the solution space).

$$\mathrm{Sol}(u_{k+2}=u_{k+1}+u_k)={\mathrm{span}}_{\mathbb{R}}\{e_{\phi },e_{\psi }\}.$$

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

Source. Repository-derived.

Commentary.

The real solution space of the Fibonacci recurrence is exactly the span of the expanding and contracting golden eigensequences.

Theorem 1.3 (Shift eigenlines).

$$S{e}_{\phi }=\phi e_{\phi },S{e}_{\psi }=\psi e_{\psi }.$$

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

Source. Repository-derived.

Commentary.

Forward shift acts by the expanding golden ratio on one line and by its algebraic conjugate on the other.

Theorem 1.4 (Shifted Binet formula).

$$F_{k+1}=\frac{{\phi }^{k+1}-{\psi }^{k+1}}{\sqrt{5}}.$$

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

Source. Repository-derived.

Commentary.

With Fibonacci weights indexed from F_1, both golden components have nonzero coefficient and their difference is normalized by sqrt(5).

Theorem 1.5 (Minimal shift-invariant carrier).

$$⟨F{⟩}_S={\mathrm{span}}_{\mathbb{R}}\{e_{\phi },e_{\psi }\}.$$

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

Source. Repository-derived.

Commentary.

The golden two-line span contains the Fibonacci weight sequence, is shift-invariant, and lies in every shift-invariant real submodule that contains that sequence. This is the formal uniqueness carrier.

Theorem 1.6 (Exact contracting residual).

$$F_{k+2}-\phi F_{k+1}={\psi }^{k+1}.$$

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

Source. Repository-derived.

Commentary.

Subtracting the expanding golden component from the shifted Fibonacci weight leaves the contracting eigensequence exactly.

References

• Truth anchor: D5/S1/Recurrence/BilateralLiftUniqueness.bilateral_lift_uniqueness
• Truth anchor: D5/S1/Recurrence/BilateralLiftUniqueness.fibonacci_cyclic_span_minimal
• Truth anchor: D5/S1/Recurrence/BilateralLiftUniqueness.fibonacci_solution_space_eq_span
• Truth anchor: D5/S1/Recurrence/BilateralLiftUniqueness.fibonacci_weight_binet
• Truth anchor: D5/S1/Recurrence/BilateralLiftUniqueness.fibonacci_weight_residual
• Truth anchor: D5/S1/Recurrence/BilateralLiftUniqueness.shift_golden_eigenvectors