bibkey: oeis2024a374911 authors: OEIS Foundation Inc. year: 2024 title: OEIS A374911 doi: null url: https://oeis.org/A374911 claim: The entry defines the power-residue recursion and explicitly asks whether three and nine are its only indices with value four. strata_touched:

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

OEIS A374911

Bryle Morga submitted the entry on July 23, 2024. Its definition is a(0) = 1, and a(n) = a(2^n mod n) + a(3^n mod n) for positive n. The comments explicitly ask: “Are 3 and 9 the only solutions to a(n) = 4?” The entry also lists the indices for values one, two and three, and states a(2^n) = 3 for n > 0. These statements supply the problem and its context; the entry does not supply the complete classification proof.

The Lean module defines the original recursion and proves the level sets for values one through four over all natural indices. The zero branch is tested before either recursive call, so the natural-number convention for remainder modulo zero cannot cause self-reference.

Verified locator

url: https://oeis.org/A374911

Read the full text entry on 2026-09-10, revision marker #26 Nov 04 2024 18:12:33. The definition is the NAME field and the value-four question is in COMMENTS. The three direct cross references are A000079, A015910 and A066601; all three were opened, with no proof of this classification found there. There is no DOI for this OEIS entry.

Proof scope

The proof in this repository uses known least-prime-factor and valuation arguments, with the former and the powers-of-three residue formula attributed to A036236. No claim of originality is made for those prerequisites.

The full-surjectivity conjecture and the questions about value five are not addressed. Unopened papers and untested Lean dataset fragments remain ASSUMED-UNVERIFIED.