Finite factorial moments and divisor-channel numerators

import Mathlib.Algebra.BigOperators.Ring.Finset
import Mathlib.Data.Nat.Factorial.Basic

/-!
# Channel breakpoint rigidity for Erdős problem 68

For a finite coefficient family whose indices all lie in one quotient band
`[k d, (k + 1) d)`, every factorial coefficient is the same fixed multiple
`(d!)^k` of its `d`-channel coefficient.  Hence cancellation of that channel
forces cancellation of the factorial moment.  In the first band, a nonzero
factorial moment together with channel cancellation requires at least one
support index to reach the breakpoint `2d`.

The namespace `Erdos68` is the finite-family presentation; it is distinct
from the Finsupp presentation in `ErdosProblems.Erdos68`.  No declaration
constructs a cancelling coefficient family, treats several channels
simultaneously, estimates a residual, or decides rationality of the #68
series.
-/

namespace Erdos68

/-- Factorial-weighted sum of a finite coefficient family. -/
def factorialMoment {ι : Type*} [Fintype ι] (coeff : ι → ℤ) (index : ι → ℕ) : ℤ :=
  ∑ j, coeff j * (index j).factorial

/-- The integer numerator of the `d`-th divisor channel. -/
def channelNumerator {ι : Type*} [Fintype ι]
    (coeff : ι → ℤ) (index : ι → ℕ) (d : ℕ) : ℤ :=
  ∑ j, coeff j * ((index j).factorial / d.factorial ^ (index j / d) : ℕ)

















end Erdos68