# The cofibonacci sequence

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-04-08.

module elementary-number-theory.cofibonacci where

Imports
open import elementary-number-theory.divisibility-natural-numbers
open import elementary-number-theory.equality-natural-numbers
open import elementary-number-theory.fibonacci-sequence
open import elementary-number-theory.inequality-natural-numbers
open import elementary-number-theory.modular-arithmetic-standard-finite-types
open import elementary-number-theory.natural-numbers
open import elementary-number-theory.pisano-periods
open import elementary-number-theory.well-ordering-principle-natural-numbers

open import foundation.action-on-identifications-functions
open import foundation.cartesian-product-types
open import foundation.decidable-types
open import foundation.dependent-pair-types
open import foundation.empty-types
open import foundation.identity-types
open import foundation.transport-along-identifications
open import foundation.universe-levels


## Idea

The cofibonacci sequence is the unique function G : ℕ → ℕ satisfying the property that

  div-ℕ (G m) n ↔ div-ℕ m (Fibonacci-ℕ n).


## Definitions

### The predicate of being a multiple of the m-th cofibonacci number

is-multiple-of-cofibonacci : (m x : ℕ) → UU lzero
is-multiple-of-cofibonacci m x =
is-nonzero-ℕ m → is-nonzero-ℕ x × div-ℕ m (Fibonacci-ℕ x)

is-decidable-is-multiple-of-cofibonacci :
(m x : ℕ) → is-decidable (is-multiple-of-cofibonacci m x)
is-decidable-is-multiple-of-cofibonacci m x =
is-decidable-function-type
( is-decidable-is-nonzero-ℕ m)
( is-decidable-product
( is-decidable-is-nonzero-ℕ x)
( is-decidable-div-ℕ m (Fibonacci-ℕ x)))

cofibonacci-multiple : (m : ℕ) → Σ ℕ (is-multiple-of-cofibonacci m)
cofibonacci-multiple zero-ℕ = pair zero-ℕ (λ f → (ex-falso (f refl)))
cofibonacci-multiple (succ-ℕ m) =
pair
( pisano-period m)
( λ f → pair (is-nonzero-pisano-period m) (div-fibonacci-pisano-period m))


### The cofibonacci sequence

least-multiple-of-cofibonacci :
(m : ℕ) → minimal-element-ℕ (is-multiple-of-cofibonacci m)
least-multiple-of-cofibonacci m =
well-ordering-principle-ℕ
( is-multiple-of-cofibonacci m)
( is-decidable-is-multiple-of-cofibonacci m)
( cofibonacci-multiple m)

cofibonacci : ℕ → ℕ
cofibonacci m = pr1 (least-multiple-of-cofibonacci m)

is-multiple-of-cofibonacci-cofibonacci :
(m : ℕ) → is-multiple-of-cofibonacci m (cofibonacci m)
is-multiple-of-cofibonacci-cofibonacci m =
pr1 (pr2 (least-multiple-of-cofibonacci m))

is-lower-bound-cofibonacci :
(m x : ℕ) → is-multiple-of-cofibonacci m x →
cofibonacci m ≤-ℕ x
is-lower-bound-cofibonacci m =
pr2 (pr2 (least-multiple-of-cofibonacci m))


## Properties

### The 0-th cofibonacci number is 0

is-zero-cofibonacci-zero-ℕ : is-zero-ℕ (cofibonacci zero-ℕ)
is-zero-cofibonacci-zero-ℕ =
is-zero-leq-zero-ℕ
( cofibonacci zero-ℕ)
( is-lower-bound-cofibonacci zero-ℕ zero-ℕ ( λ f → ex-falso (f refl)))


### The cofibonacci sequence is left adjoint to the Fibonacci sequence

forward-is-left-adjoint-cofibonacci :
(m n : ℕ) → div-ℕ (cofibonacci m) n → div-ℕ m (Fibonacci-ℕ n)
tr
( div-ℕ zero-ℕ)
( ap
( Fibonacci-ℕ)
( inv
( is-zero-div-zero-ℕ n
( tr (λ t → div-ℕ t n) is-zero-cofibonacci-zero-ℕ H))))
( refl-div-ℕ zero-ℕ)
forward-is-left-adjoint-cofibonacci (succ-ℕ m) zero-ℕ H =
div-zero-ℕ (succ-ℕ m)
forward-is-left-adjoint-cofibonacci (succ-ℕ m) (succ-ℕ n) H =
div-Fibonacci-div-ℕ
( succ-ℕ m)
( cofibonacci (succ-ℕ m))
( succ-ℕ n)
( H)
( pr2
( is-multiple-of-cofibonacci-cofibonacci
( succ-ℕ m)
( is-nonzero-succ-ℕ m)))

{-