Closed low-valuation counts for every odd prime

The full distribution specializes to compact formulas at valuations zero and one. These are arithmetic counts on the complete block below p ^ k, not asymptotic estimates.

theorem OddPrimeValuationDistribution.coeff_zero_oddCarryPolynomial (half length : ℕ) : (oddCarryPolynomial half length).coeff 0 = (half + 1) ^ length

The zero-carry coefficient in odd base 2 * half + 1.

theorem OddPrimeValuationDistribution.coeff_zero_oddCarryPolynomialFrom_one_succ (half length : ℕ) : (oddCarryPolynomialFrom half 1 (length + 1)).coeff 0 = half * (half + 1) ^ length

Zero additional carries from incoming carry one, for positive word length.

theorem OddPrimeValuationDistribution.coeff_one_oddCarryPolynomial_add_two (half length : ℕ) : (oddCarryPolynomial half (length + 2)).coeff 1 = half * (half + 1) ^ (length + 1) + (length + 1) * half ^ 2 * (half + 1) ^ length

Exact one-carry coefficient for every odd base, parameterized by block length length + 2.

theorem OddPrimeValuationDistribution.card_oddPrimeBlock_valuation_zero (half : ℕ) (hhalf : 0 < half) [Fact (Nat.Prime (oddBase half))] (length : ℕ) : Fintype.card (OddPrimeBlockWithValuation half length 0) = (half + 1) ^ length

Exact count of valuation-zero integers in a complete odd-prime block.

theorem OddPrimeValuationDistribution.card_oddPrimeBlock_valuation_one (half : ℕ) (hhalf : 0 < half) [Fact (Nat.Prime (oddBase half))] (length : ℕ) : Fintype.card (OddPrimeBlockWithValuation half (length + 2) 1) = half * (half + 1) ^ (length + 1) + (length + 1) * half ^ 2 * (half + 1) ^ length

Exact count of valuation-one integers in every complete odd-prime block of length at least two.

theorem OddPrimeValuationDistribution.coeff_oddPrimeValuationPolynomial_recurrence (half : ℕ) (hhalf : 0 < half) [Fact (Nat.Prime (oddBase half))] (length value : ℕ) : (oddPrimeValuationPolynomial half (length + 2)).coeff (value + 1) + oddBase half * (oddPrimeValuationPolynomial half length).coeff value = (half + 1) * (oddPrimeValuationPolynomial half (length + 1)).coeff (value + 1) + (half + 1) * (oddPrimeValuationPolynomial half (length + 1)).coeff value

Coefficient recurrence for the exact valuation counts.

theorem OddPrimeValuationDistribution.card_ternaryBlock_valuation_lt_two (length : ℕ) : Fintype.card (OddPrimeBlockWithValuation 1 (length + 2) 0) + Fintype.card (OddPrimeBlockWithValuation 1 (length + 2) 1) = (length + 7) * 2 ^ length

Ternary specialization: among the integers below 3 ^ (length + 2), the number whose central binomial coefficient has 3-adic valuation zero or one is exactly (length + 7) * 2 ^ length.