bibkey: oeis2024a091259 authors: OEIS Foundation Inc. year: 2024 title: OEIS A091259 doi: null url: https://oeis.org/A091259 claim: A comment on OEIS A091259 conjectures that the reduced numerator of the ratio of the cubic to the linear divisor sum is congruent modulo three to a prime-exponent indicator. strata_touched:
- D5/S3/Factorization/A091259 license: citation-only triage: anchor
OEIS A091259
The entry records the numerator of the ratio of the divisor sum of cubes to the ordinary divisor sum, taken in lowest terms. Michel Marcus conjectured on August 11, 2024 that this numerator, read modulo three, agrees with the indicator recorded in a neighbouring entry. The caller found it still labelled Conjecture on September 9, 2026.
The indicator on the other side
The neighbouring entry states its own criterion in terms of prime exponents: the indicator is one exactly when every prime congruent to two modulo three occurs to an even exponent. That criterion is printed there, so the Lean statement uses it directly and does not reprove the classical equivalence with representability by the quadratic form.
What makes the step nontrivial
Writing the local factor at a prime power as a ratio of values of the quadratic whose roots are the primitive cube roots of unity, the residues fall out case by case. What does not fall out is the reduction: cancelling the fraction could in principle consume a factor of three or leave one behind, and tracking that through the exponents is the part the printed material does not supply.
The module avoids the tracking entirely. It proves a general lemma: when a cross-multiplication relates two pairs and every divisor of the denominator side is one modulo three, the reduced numerator agrees modulo three with the other numerator. The reduction may consume whatever it likes; the conclusion does not depend on which factors it consumed.
What the Lean module proves
D5/S3/Factorization/A091259 states the congruence for every positive
argument. Between the general reduction lemma and the main theorem sit the
local classification at prime powers, the behaviour of the quadratic modulo
three, and the multiplicative assembly.
ASSUMED-UNVERIFIED: the identification of the printed numerator and the neighbouring indicator with the module’s definitions is a human reading of the two entries, not a machine proof that they denote the same functions.
Search log
- Caller reading, 2026-09-09: the seat reported checking both entries and their revision histories, finding the conjecture still open and the indicator’s prime-exponent criterion printed on the neighbouring page. It also reported that the adjacent conjecture about the denominators is not needed: only its easy direction, that every prime factor of the reduced denominator is one modulo three, enters here.
- The seat’s receipt is
所查来源未找到, explicitly not a claim that no proof exists anywhere. It stated it had independently recomputed the congruence to twenty thousand; the orchestrator did not reproduce that range. - Caller verification, 2026-09-09: the orchestrator checked the congruence to three thousand, the value set of the numerator modulo three, the key ratio identity at prime powers, and the four residue cases. Readings are in the problem entry.
Verified locator
- URL: https://oeis.org/A091259
- Indicator entry: https://oeis.org/A353816
- Adjacent denominator entry: https://oeis.org/A091258