Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Reduced Numerators Modulo Three

Abstract

The reduction can consume whatever it likes: if every divisor on the denominator side is one modulo three, the reduced numerator is determined anyway.

Arguments are positive naturals. The quadratic below is the one whose roots are the primitive cube roots of unity, written out rather than taken from a cyclotomic library so the arithmetic stays elementary.

Theorem 1.1 (Reduction without tracking).

Proof. Machine-checked in Lean as D5/S3/Factorization/A091259.reduced_numerator_mod_three (✓ std3). ∎

Source. Repository-derived.

Commentary.

This is the step the printed material does not supply. Cancelling a fraction could consume a factor of three or leave one behind, and following that through the exponents is delicate. It is also unnecessary: after cancelling, the two cofactors are coprime, so the denominator cofactor divides the other side’s denominator, and the remaining factor divides it too. Every divisor there being one modulo three fixes the answer regardless of what was cancelled.

Definition 1.2 (The quadratic).

Formalization. D5/S3/Factorization/A091259.cyclotomicThree (✓ std3).

Source. Repository-derived.

Commentary.

Its values at prime powers carry the whole local behaviour.

Theorem 1.3 (The local classification).

Proof. Machine-checked in Lean as D5/S3/Factorization/A091259.localNumerator_mod (✓ std3). ∎

Source. Repository-derived.

Commentary.

A prime congruent to two contributes zero at odd exponents and one at even ones; the prime three contributes one throughout; a prime congruent to one contributes a single factor of three on each side and the quotients are one. The exponent parity is what the indicator on the other side is reading.

Theorem 1.4 (The conjecture).

Proof. Machine-checked in Lean as D5/S3/Factorization/A091259.a091259_mod_three (✓ std3). ∎

Resolves. Problems/oeis-a091259-reduced-numerator-mod-three (proved) by D5/S3/Factorization/A091259.a091259_mod_three.

Source. Repository-derived.

Acknowledgement. OEIS Foundation Inc. (2024). OEIS A091259. URL: https://oeis.org/A091259.

Commentary.

The divisor sums are multiplicative, so the cross-multiplication holds factor by factor, with the denominator side built from the local factors with their threes stripped. Every divisor there is one modulo three, so the reduction lemma applies and the local classification assembles into the indicator.

The classical criterion behind the indicator is taken as printed on the source’s neighbouring entry and is not reproved here. The adjacent conjecture about which denominators occur is untouched; only its easy direction enters, and that direction is what the stripped construction supplies.

References