Pisano periods
module elementary-number-theory.pisano-periods where
Imports
open import elementary-number-theory.divisibility-natural-numbers open import elementary-number-theory.fibonacci-sequence open import elementary-number-theory.inequality-natural-numbers open import elementary-number-theory.lower-bounds-natural-numbers open import elementary-number-theory.modular-arithmetic-standard-finite-types open import elementary-number-theory.natural-numbers open import elementary-number-theory.strict-inequality-natural-numbers open import elementary-number-theory.well-ordering-principle-natural-numbers open import foundation.cartesian-product-types open import foundation.dependent-pair-types open import foundation.empty-types open import foundation.equivalences open import foundation.identity-types open import foundation.injective-maps open import foundation.repetitions-sequences open import foundation.universe-levels open import univalent-combinatorics.cartesian-product-types open import univalent-combinatorics.counting open import univalent-combinatorics.sequences-finite-types open import univalent-combinatorics.standard-finite-types
Idea
The sequence P : ℕ → ℕ of Pisano periods is the sequence where P n is
the period of the Fibonacci sequence modulo n. This sequence is listed as
A001175 in the OEIS.
Definitions
The Fibonacci sequence on Fin (k + 1) × Fin (k + 1)
generating-map-fibonacci-pair-Fin : (k : ℕ) → Fin (succ-ℕ k) × Fin (succ-ℕ k) → Fin (succ-ℕ k) × Fin (succ-ℕ k) generating-map-fibonacci-pair-Fin k p = pair (pr2 p) (add-Fin (succ-ℕ k) (pr2 p) (pr1 p)) inv-generating-map-fibonacci-pair-Fin : (k : ℕ) → Fin (succ-ℕ k) × Fin (succ-ℕ k) → Fin (succ-ℕ k) × Fin (succ-ℕ k) inv-generating-map-fibonacci-pair-Fin k (pair x y) = pair (add-Fin (succ-ℕ k) y (neg-Fin (succ-ℕ k) x)) x issec-inv-generating-map-fibonacci-pair-Fin : (k : ℕ) (p : Fin (succ-ℕ k) × Fin (succ-ℕ k)) → Id ( generating-map-fibonacci-pair-Fin k ( inv-generating-map-fibonacci-pair-Fin k p)) ( p) issec-inv-generating-map-fibonacci-pair-Fin k (pair x y) = ap-binary pair refl ( ( commutative-add-Fin ( succ-ℕ k) ( x) ( add-Fin (succ-ℕ k) y (neg-Fin (succ-ℕ k) x))) ∙ ( ( associative-add-Fin (succ-ℕ k) y (neg-Fin (succ-ℕ k) x) x) ∙ ( ( ap (add-Fin (succ-ℕ k) y) (left-inverse-law-add-Fin k x)) ∙ ( right-unit-law-add-Fin k y)))) isretr-inv-generating-map-fibonacci-pair-Fin : (k : ℕ) (p : Fin (succ-ℕ k) × Fin (succ-ℕ k)) → Id ( inv-generating-map-fibonacci-pair-Fin k ( generating-map-fibonacci-pair-Fin k p)) ( p) isretr-inv-generating-map-fibonacci-pair-Fin k (pair x y) = ap-binary pair ( ( commutative-add-Fin ( succ-ℕ k) ( add-Fin (succ-ℕ k) y x) ( neg-Fin (succ-ℕ k) y)) ∙ ( ( inv (associative-add-Fin (succ-ℕ k) (neg-Fin (succ-ℕ k) y) y x)) ∙ ( ( ap (λ t → add-Fin (succ-ℕ k) t x) (left-inverse-law-add-Fin k y)) ∙ ( left-unit-law-add-Fin k x)))) ( refl) is-equiv-generating-map-fibonacci-pair-Fin : (k : ℕ) → is-equiv (generating-map-fibonacci-pair-Fin k) is-equiv-generating-map-fibonacci-pair-Fin k = is-equiv-has-inverse ( inv-generating-map-fibonacci-pair-Fin k) ( issec-inv-generating-map-fibonacci-pair-Fin k) ( isretr-inv-generating-map-fibonacci-pair-Fin k) fibonacci-pair-Fin : (k : ℕ) → ℕ → Fin (succ-ℕ k) × Fin (succ-ℕ k) fibonacci-pair-Fin k zero-ℕ = pair (zero-Fin k) (one-Fin k) fibonacci-pair-Fin k (succ-ℕ n) = generating-map-fibonacci-pair-Fin k (fibonacci-pair-Fin k n) compute-fibonacci-pair-Fin : (k : ℕ) (n : ℕ) → Id ( fibonacci-pair-Fin k n) ( pair ( mod-succ-ℕ k (Fibonacci-ℕ n)) ( mod-succ-ℕ k (Fibonacci-ℕ (succ-ℕ n)))) compute-fibonacci-pair-Fin k zero-ℕ = refl compute-fibonacci-pair-Fin k (succ-ℕ zero-ℕ) = ap-binary pair refl (right-unit-law-add-Fin k (one-Fin k)) compute-fibonacci-pair-Fin k (succ-ℕ (succ-ℕ n)) = ap-binary pair ( ap pr2 (compute-fibonacci-pair-Fin k (succ-ℕ n))) ( ( ap-binary ( add-Fin (succ-ℕ k)) ( ap pr2 (compute-fibonacci-pair-Fin k (succ-ℕ n))) ( ap pr1 (compute-fibonacci-pair-Fin k (succ-ℕ n)))) ∙ ( inv ( mod-succ-add-ℕ k ( Fibonacci-ℕ (succ-ℕ (succ-ℕ n))) ( Fibonacci-ℕ (succ-ℕ n)))))
Repetitions in the Fibonacci sequence on Fin (k + 1) × Fin (k + 1)
has-ordered-repetition-fibonacci-pair-Fin : (k : ℕ) → ordered-repetition-of-values-ℕ (fibonacci-pair-Fin k) has-ordered-repetition-fibonacci-pair-Fin k = ordered-repetition-of-values-nat-to-count ( count-prod (count-Fin (succ-ℕ k)) (count-Fin (succ-ℕ k))) ( fibonacci-pair-Fin k) is-ordered-repetition-fibonacci-pair-Fin : ℕ → ℕ → UU lzero is-ordered-repetition-fibonacci-pair-Fin k x = Σ ℕ (λ y → (le-ℕ y x) × (fibonacci-pair-Fin k y ＝ fibonacci-pair-Fin k x)) minimal-ordered-repetition-fibonacci-pair-Fin : (k : ℕ) → minimal-element-ℕ (is-ordered-repetition-fibonacci-pair-Fin k) minimal-ordered-repetition-fibonacci-pair-Fin k = minimal-element-repetition-of-values-sequence-count ( count-prod (count-Fin (succ-ℕ k)) (count-Fin (succ-ℕ k))) ( fibonacci-pair-Fin k)
The Pisano periods
pisano-period : ℕ → ℕ pisano-period k = pr1 (minimal-ordered-repetition-fibonacci-pair-Fin k) is-ordered-repetition-pisano-period : (k : ℕ) → is-ordered-repetition-fibonacci-pair-Fin k (pisano-period k) is-ordered-repetition-pisano-period k = pr1 (pr2 (minimal-ordered-repetition-fibonacci-pair-Fin k)) is-lower-bound-pisano-period : (k : ℕ) → is-lower-bound-ℕ ( is-ordered-repetition-fibonacci-pair-Fin k) ( pisano-period k) is-lower-bound-pisano-period k = pr2 (pr2 (minimal-ordered-repetition-fibonacci-pair-Fin k)) cases-is-repetition-of-zero-pisano-period : (k x y : ℕ) → Id (pr1 (is-ordered-repetition-pisano-period k)) x → Id (pisano-period k) y → is-zero-ℕ x cases-is-repetition-of-zero-pisano-period k zero-ℕ y p q = refl cases-is-repetition-of-zero-pisano-period k (succ-ℕ x) zero-ℕ p q = ex-falso ( concatenate-eq-le-eq-ℕ ( inv p) ( pr1 (pr2 (is-ordered-repetition-pisano-period k))) ( q)) cases-is-repetition-of-zero-pisano-period k (succ-ℕ x) (succ-ℕ y) p q = ex-falso ( contradiction-leq-ℕ y y (refl-leq-ℕ y) ( concatenate-eq-leq-ℕ y (inv q) (is-lower-bound-pisano-period k y R))) where R : is-ordered-repetition-fibonacci-pair-Fin k y R = triple x ( concatenate-eq-le-eq-ℕ ( inv p) ( pr1 (pr2 (is-ordered-repetition-pisano-period k))) ( q)) ( is-injective-is-equiv ( is-equiv-generating-map-fibonacci-pair-Fin k) ( ( ap (fibonacci-pair-Fin k) (inv p)) ∙ ( ( pr2 (pr2 (is-ordered-repetition-pisano-period k))) ∙ ( ap (fibonacci-pair-Fin k) q)))) is-repetition-of-zero-pisano-period : (k : ℕ) → is-zero-ℕ (pr1 (is-ordered-repetition-pisano-period k)) is-repetition-of-zero-pisano-period k = cases-is-repetition-of-zero-pisano-period k ( pr1 (is-ordered-repetition-pisano-period k)) ( pisano-period k) ( refl) ( refl) compute-fibonacci-pair-Fin-pisano-period : (k : ℕ) → Id (fibonacci-pair-Fin k (pisano-period k)) (fibonacci-pair-Fin k zero-ℕ) compute-fibonacci-pair-Fin-pisano-period k = ( inv (pr2 (pr2 (is-ordered-repetition-pisano-period k)))) ∙ ( ap (fibonacci-pair-Fin k) (is-repetition-of-zero-pisano-period k))
Properties
Pisano periods are nonzero
le-zero-pisano-period : (k : ℕ) → le-ℕ zero-ℕ (pisano-period k) le-zero-pisano-period k = concatenate-eq-le-ℕ { x = zero-ℕ} { y = pr1 (is-ordered-repetition-pisano-period k)} { z = pisano-period k} ( inv (is-repetition-of-zero-pisano-period k)) ( pr1 (pr2 (is-ordered-repetition-pisano-period k))) is-nonzero-pisano-period : (k : ℕ) → is-nonzero-ℕ (pisano-period k) is-nonzero-pisano-period k p = ex-falso (concatenate-le-eq-ℕ (le-zero-pisano-period k) p)
k + 1 divides the Fibonacci number at pisano-period k
div-fibonacci-pisano-period : (k : ℕ) → div-ℕ (succ-ℕ k) (Fibonacci-ℕ (pisano-period k)) div-fibonacci-pisano-period k = div-is-zero-mod-succ-ℕ k ( Fibonacci-ℕ (pisano-period k)) ( ( ap pr1 (inv (compute-fibonacci-pair-Fin k (pisano-period k)))) ∙ ( inv ( ap pr1 { x = fibonacci-pair-Fin k zero-ℕ} { y = fibonacci-pair-Fin k (pisano-period k)} ( ( ap ( fibonacci-pair-Fin k) ( inv (is-repetition-of-zero-pisano-period k))) ∙ ( pr2 (pr2 (is-ordered-repetition-pisano-period k)))))))