Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

bibkey: cloitre2002a074724 authors: Benoit Cloitre; Michel Marcus; Peter Bala year: 2022 title: “OEIS A074724, highest power of 3 dividing F(4n), with the Marcus and Bala conjectures” doi: null url: https://oeis.org/A074724 claim: “%N Highest power of 3 dividing F(4n) where F(k) is the k-th Fibonacci number. %F a(n) = 3^A051064(n) (conjectured). - Michel Marcus, May 17 2022 %F Conjecture: a(n) = (sigma(3n) - sigma(n))/(sigma(3n) - 3*sigma(n)), where sigma(n) = A000203(n). Equivalently, a(n) = A088838(n) - A074724(n). - Peter Bala, Jun 10 2022” strata_touched:

  • D5/S3/Arith/CloitreFibFourThreeAdicValuationSigma license: citation-only triage: anchor

OEIS A074724

Cloitre’s sequence is the highest power of three dividing the Fibonacci number at index 4n. The year 2022 records the Marcus and Bala conjectures; the entry’s AUTHOR line dates Cloitre’s contribution to September 4, 2002.

For positive natural n, A051064(n) is v_3(3n) = v_3(n) + 1, where v_3 is padicValNat 3. The valuation clause therefore states a(n) = 3^(v_3(n)+1). Bala’s formula is represented with the denominator multiplied out in natural numbers: a(n) * (sigma(3n) - 3*sigma(n)) = sigma(3n) - sigma(n). Writing n = 3^e m with 3 not dividing m gives sigma(3n) - 3*sigma(n) = sigma(m) > 0; this positivity is proved inside the Lean proof. The displayed subtractions are natural-number subtractions. The sentence beginning “Equivalently, a(n) = A088838(n) - A074724(n)” is preserved in the quotation but is not part of the settled claim.

Lengyel (1995) gave the general p-adic valuation of Fibonacci numbers in the literature. This is prior literature for the valuation clause; the Lean module proves the relevant 3-adic identity directly from Fibonacci divisibility, Cassini’s identity and exponent induction. The valuation formula is therefore not claimed as a new discovery in the mathematical literature.

The theorem assumes 0 < n. At zero, Lean’s totalized valuation is zero and the definition gives a(0) = 1; zero has no highest power of three dividing it.

Verified locator

  • URL: https://oeis.org/A074724
  • %N (verbatim): Highest power of 3 dividing F(4n) where F(k) is the k-th Fibonacci number.
  • %F (Marcus, verbatim): a(n) = 3^A051064(n) (conjectured). - Michel Marcus, May 17 2022
  • %F (Bala, verbatim): Conjecture: a(n) = (sigma(3n) - sigma(n))/(sigma(3n) - 3*sigma(n)), where sigma(n) = A000203(n). Equivalently, a(n) = A088838(n) - A074724(n). - Peter Bala, Jun 10 2022
  • %A (verbatim): Benoit Cloitre, Sep 04 2002

The locator lines were checked against https://oeis.org/A074724 on 2026-09-15. Lengyel (1995) is prior literature for the valuation clause.