Totient Nondivisors and Consecutive-Totient Lcm Records

Abstract

Totient nondivisor values are exactly consecutive-totient lcm jumps, and 1275120 refutes the proposed exception set for equality with the power-sum sequence.

OEIS A378640 (Xausa, 2024-12-05) asks whether its values agree with A095366 outside numbers sixty times an odd number, and whether its distinct values are A076245 after the initial one. The first question is refuted here at N = 1275120; the second is answered affirmatively by a general range characterization derived in this repository.

The counterexample and range theorem share the function a and its BadTotient minimality machinery, so they are placed in one module. Natural subtraction is truncated. For N >= 1, powerSum_eq_positive_index_sum identifies the Finset.range implementation with the atom’s literal sum ∑_{1 ≤ j < k} j^N. The lcm over an empty range is one.

Definition 1.1 (Failure of totient divisibility).

$$\forall N\in \mathbb{N},m\in \mathbb{N},\mathrm{BadTotient}\left(N,m\right)\iff \left(2\le m\wedge \left(\neg \phi \left(m\right)\mid N\right)\right)$$

Formalization. D5/S3/Factorization/TotientNondivisorRecords.BadTotient (✓ std3).

Source. Repository-derived.

Commentary.

BadTotient(N,m) is exactly the conjunction that m is at least two and Euler’s totient phi(m) does not divide N.

Definition 1.2 (Least totient nondivisor).

$$\forall N\in \mathbb{N},a\left(N\right)=\mathrm{if}0<N\mathrm{then}\min \left(\{m:\mathbb{N}\mid \mathrm{BadTotient}\left(N,m\right)\}\right)\mathrm{else}0$$

Formalization. D5/S3/Factorization/TotientNondivisorRecords.a (✓ std3).

Source. Repository-derived.

Commentary.

For positive N, a(N) is Nat.find applied to the existence of a BadTotient, hence the minimum displayed. The totalized value at N = 0 is zero; the OEIS A378640 sequence is used only on positive inputs.

Definition 1.3 (Finite power sum).

$$\forall N\in \mathbb{N},k\in \mathbb{N},\mathrm{powerSum}\left(N,k\right)=\sum _{0\le j<k}{j}^N$$

Formalization. D5/S3/Factorization/TotientNondivisorRecords.powerSum (✓ std3).

Source. Repository-derived.

Commentary.

The range contains precisely 0 through k-1. The public theorem powerSum_eq_positive_index_sum proves that for N >= 1 its zeroth term vanishes, leaving the atom’s sum ∑_{1 ≤ j < k} j^N.

Theorem 1.4 (Range sum equals the positive-index sum).

$$\forall N\in \mathbb{N},k\in \mathbb{N},(1\le N)\Rightarrow (\mathrm{powerSum}\left(N,k\right)=\sum _{1\le j<k}{j}^N)$$

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

Source. Repository-derived.

Commentary.

For every positive exponent, the j = 0 term is zero, so the range implementation equals ∑_{1 ≤ j < k} j^N. This is the exact power sum transcribed in the OEIS A095366 clause of the source atom.

Definition 1.5 (Power-sum divisor predicate).

$$\forall N\in \mathbb{N},k\in \mathbb{N},\mathrm{PowerSumDivisor}\left(N,k\right)\iff \left(2\le k\wedge k\mid \mathrm{powerSum}\left(N,k\right)\right)$$

Formalization. D5/S3/Factorization/TotientNondivisorRecords.PowerSumDivisor (✓ std3).

Source. Repository-derived.

Commentary.

A power-sum divisor is at least two and divides the corresponding finite sum.

Definition 1.6 (Least power-sum divisor).

$$\forall N\in \mathbb{N},A095366\left(N\right)=\mathrm{sInf}\left(\{k:\mathbb{N}\mid \mathrm{PowerSumDivisor}\left(N,k\right)\}\right)$$

Formalization. D5/S3/Factorization/TotientNondivisorRecords.A095366 (✓ std3).

Source. Repository-derived.

Commentary.

This is Nat.sInf of exactly the natural numbers satisfying PowerSumDivisor. A095366_eq_literal identifies it publicly with the least k > 1 dividing ∑_{1 ≤ j < k} j^N, the A095366 definition cited by OEIS A378640 (Xausa, 2024); for exponent 1275120 the proof supplies 53 as an inhabitant.

Theorem 1.7 (A095366 has the atom’s literal definition).

$$\forall N\in \mathbb{N},(1\le N)\Rightarrow (A095366\left(N\right)=\mathrm{sInf}\left(\{k:\mathbb{N}\mid (1<k\wedge k\mid \sum _{1\le j<k}{j}^N)\}\right))$$

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

Source. Repository-derived.

Commentary.

For every positive exponent, A095366 is exactly the infimum of k > 1 that divide ∑_{1 ≤ j < k} j^N. This transcribes the OEIS A095366 definition in the source atom and follows from powerSum_eq_positive_index_sum.

Definition 1.8 (Consecutive-totient lcm).

$$\forall t\in \mathbb{N},L\left(t\right)={\mathrm{lcm}}_{0\le i<t}\phi \left(i+1\right)$$

Formalization. D5/S3/Factorization/TotientNondivisorRecords.L (✓ std3).

Source. Repository-derived.

Commentary.

The finite range 0 <= i < t is shifted by one, so this is exactly the lcm of phi(1) through phi(t), the A076245 construction cited by OEIS A378640 (Xausa, 2024). The t = 0 range is empty.

Theorem 1.9 (The empty lcm).

$$L\left(0\right)=1$$

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

Source. Repository-derived.

Commentary.

Finset.lcm over the empty range is one.

Theorem 1.10 (Divisibility by the consecutive-totient lcm).

$$\forall t\in \mathbb{N},N\in \mathbb{N},L\left(t\right)\mid N\iff \left(\forall j\in \mathbb{N},1\le j\Rightarrow \left(j\le t\Rightarrow \phi \left(j\right)\mid N\right)\right)$$

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

Source. Repository-derived.

Commentary.

Finset.lcm_dvd_iff turns divisibility by L(t) into simultaneous divisibility by every phi(j) with 1 <= j <= t.

Theorem 1.11 (Strict lcm jumps detect a new totient).

$$\forall m\in \mathbb{N},2\le m\Rightarrow \left(L\left(m-1\right)<L\left(m\right)\iff \left(\neg \phi \left(m\right)\mid L\left(m-1\right)\right)\right)$$

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

Source. Repository-derived.

Commentary.

Monotonicity gives L(m-1) dividing L(m). Equality holds exactly when the new factor phi(m) already divides L(m-1), yielding the stated strict-jump criterion.

Theorem 1.12 (The value set is the strict-jump set).

$$\forall m\in \mathbb{N},2\le m\Rightarrow \left(\left(\exists N\in \mathbb{N},1\le N\wedge a\left(N\right)=m\right)\iff L\left(m-1\right)<L\left(m\right)\right)$$

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

Source. Repository-derived.

Commentary.

Forward, minimality of a(N) makes every earlier totient divide N, so L(m-1) divides N while phi(m) does not. Reverse, the explicit positive witness N = L(m-1) has all earlier totients as divisors and excludes phi(m). Thus the value set for m >= 2 is A076245 without its initial one.

Theorem 1.13 (The lower totients divide the witness).

$$\forall i\in \mathrm{Fin}\left(51\right),1\le \mathrm{val}\left(i\right)\Rightarrow \phi \left(\mathrm{val}\left(i\right)\right)\mid 1275120$$

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

Source. Repository-derived.

Commentary.

Kernel decide checks every finite index i below 51 and proves that phi(i.val) divides 1275120 whenever i.val is positive.

Theorem 1.14 (The totient at 51).

$$\phi \left(51\right)=32$$

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

Source. Repository-derived.

Commentary.

Kernel decide computes phi(51) exactly as 32.

Theorem 1.15 (The witness modulo 32).

$$1275120\mathrm{mod}32=16$$

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

Source. Repository-derived.

Commentary.

Exact natural-number normalization computes the remainder as 16.

Theorem 1.16 (The witness modulo 120).

$$1275120\mathrm{mod}120=0$$

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

Source. Repository-derived.

Commentary.

Exact natural-number normalization computes the remainder as zero.

Theorem 1.17 (The least totient nondivisor at 1275120).

$$a\left(1275120\right)=51$$

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

Source. Repository-derived.

Commentary.

Kernel decide certifies phi(j) dividing 1275120 for every 1 <= j <= 50. It also certifies phi(51) = 32, while 1275120 has remainder 16 modulo 32.

Theorem 1.18 (The power sum modulo 51).

$$\mathrm{powerSum}\left(1275120,51\right)\equiv 31(\mathrm{mod}51)$$

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

Source. Repository-derived.

Commentary.

Kernel-producing modular reduction computes the power sum as congruent to 31 modulo 51.

Theorem 1.19 (The power sum modulo 53).

$$\mathrm{powerSum}\left(1275120,53\right)\equiv 0(\mathrm{mod}53)$$

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

Source. Repository-derived.

Commentary.

Kernel-producing modular reduction computes the power sum as congruent to zero modulo 53.

Theorem 1.20 (The power-sum value is not 51).

$$A095366\left(1275120\right)\ne 51$$

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

Source. Repository-derived.

Commentary.

A095366_eq_literal makes the certificate about the atom’s sum ∑_{1 ≤ j < k} j^1275120. Kernel-producing modular reduction gives its value at k = 51 congruent to 31 modulo 51 and its value at k = 53 congruent to zero modulo 53. Hence 53 inhabits the literal defining set but 51 does not.

Theorem 1.21 (The witness lies outside the proposed exception family).

$$\neg \left(\exists k\in \mathbb{N},1275120=60\cdot \left(2\cdot k+1\right)\right)$$

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

Source. Repository-derived.

Commentary.

The certified zero remainder modulo 120 contradicts the remainder 60 forced by any representation of 1275120 as sixty times an odd number.

Theorem 1.22 (Counterexample to the proposed exception set).

$$(a\left(1275120\right)=51)\wedge \left((A095366\left(1275120\right)\ne 51)\wedge (\neg \left(\exists k\in \mathbb{N},1275120=60\cdot \left(2\cdot k+1\right)\right))\right).$$

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

Source. Repository-derived.

Commentary.

All three certified clauses are stated together: a(1275120) is 51, the A095366 value is not 51, and 1275120 is outside the claimed exception form. Therefore the proposed equality-exception description is false.

References

• Truth anchor: D5/S3/Factorization/TotientNondivisorRecords.A095366
• Truth anchor: D5/S3/Factorization/TotientNondivisorRecords.A095366_1275120_ne_51
• Truth anchor: D5/S3/Factorization/TotientNondivisorRecords.A095366_eq_literal
• Truth anchor: D5/S3/Factorization/TotientNondivisorRecords.BadTotient
• Truth anchor: D5/S3/Factorization/TotientNondivisorRecords.L
• Truth anchor: D5/S3/Factorization/TotientNondivisorRecords.L_dvd_iff
• Truth anchor: D5/S3/Factorization/TotientNondivisorRecords.L_jump_iff_not_dvd
• Truth anchor: D5/S3/Factorization/TotientNondivisorRecords.L_zero
• Truth anchor: D5/S3/Factorization/TotientNondivisorRecords.PowerSumDivisor
• Truth anchor: D5/S3/Factorization/TotientNondivisorRecords.a
• Truth anchor: D5/S3/Factorization/TotientNondivisorRecords.a_1275120
• Truth anchor: D5/S3/Factorization/TotientNondivisorRecords.exception_set_claim_false
• Truth anchor: D5/S3/Factorization/TotientNondivisorRecords.mod_1275120_120
• Truth anchor: D5/S3/Factorization/TotientNondivisorRecords.mod_1275120_32
• Truth anchor: D5/S3/Factorization/TotientNondivisorRecords.not_exception_form
• Truth anchor: D5/S3/Factorization/TotientNondivisorRecords.powerSum
• Truth anchor: D5/S3/Factorization/TotientNondivisorRecords.powerSum_1275120_mod_51
• Truth anchor: D5/S3/Factorization/TotientNondivisorRecords.powerSum_1275120_mod_53
• Truth anchor: D5/S3/Factorization/TotientNondivisorRecords.powerSum_eq_positive_index_sum
• Truth anchor: D5/S3/Factorization/TotientNondivisorRecords.range_iff_lcm_jump
• Truth anchor: D5/S3/Factorization/TotientNondivisorRecords.totient_51_eq_32
• Truth anchor: D5/S3/Factorization/TotientNondivisorRecords.totients_lt_51_dvd_1275120