Doubling carries in an arbitrary odd base

Write an odd base as 2 * half + 1. This module defines the two-state doubling transducer in that base and proves its arithmetic correctness. When the base is prime, the carry count is exactly the prime-adic valuation of the central binomial coefficient.

def OddPrimeValuationDistribution.oddBase (half : ℕ) : ℕ

The odd base represented by its lower half-size.

Equations

• OddPrimeValuationDistribution.oddBase half = 2 * half + 1

def OddPrimeValuationDistribution.oddDoubleCarryStep (half carry digit : ℕ) : ℕ

Outgoing carry while doubling one digit in the odd base 2 * half + 1.

Equations

• OddPrimeValuationDistribution.oddDoubleCarryStep half carry digit = (2 * digit + carry) / OddPrimeValuationDistribution.oddBase half

def OddPrimeValuationDistribution.oddDoubleCarryCountAux (half : ℕ) : List ℕ → ℕ → ℕ

Number of outgoing carries while doubling a little-endian word in an odd base.

Equations

• One or more equations did not get rendered due to their size.
• OddPrimeValuationDistribution.oddDoubleCarryCountAux half [] x✝ = 0

def OddPrimeValuationDistribution.oddDoubleDigitsAux (half : ℕ) : List ℕ → ℕ → List ℕ

Output digits while doubling in an odd base. The final carry is retained as the most significant output digit.

Equations

• One or more equations did not get rendered due to their size.
• OddPrimeValuationDistribution.oddDoubleDigitsAux half [] x✝ = [x✝]

theorem OddPrimeValuationDistribution.oddBase_pos (half : ℕ) : 0 < oddBase half

theorem OddPrimeValuationDistribution.oddBase_one_lt {half : ℕ} (hhalf : 0 < half) : 1 < oddBase half

theorem OddPrimeValuationDistribution.oddDoubleCarryStep_le_one {half carry digit : ℕ} (hcarry : carry ≤ 1) (hdigit : digit < oddBase half) : oddDoubleCarryStep half carry digit ≤ 1

theorem OddPrimeValuationDistribution.oddDoubleCarryStep_lt_base {half carry digit : ℕ} (hhalf : 0 < half) (hcarry : carry ≤ 1) (hdigit : digit < oddBase half) : oddDoubleCarryStep half carry digit < oddBase half

theorem OddPrimeValuationDistribution.oddDoubleCarryStep_local (half carry digit : ℕ) : (2 * digit + carry) % oddBase half + oddBase half * oddDoubleCarryStep half carry digit = 2 * digit + carry

theorem OddPrimeValuationDistribution.oddDoubleCarryStep_zero_of_lt_succ {half digit : ℕ} (hdigit : digit < half + 1) : oddDoubleCarryStep half 0 digit = 0

theorem OddPrimeValuationDistribution.oddDoubleCarryStep_one_of_succ_le {half digit : ℕ} (hlower : half + 1 ≤ digit) (hupper : digit < oddBase half) : oddDoubleCarryStep half 0 digit = 1

theorem OddPrimeValuationDistribution.oddDoubleCarryStep_zero_of_lt {half digit : ℕ} (hdigit : digit < half) : oddDoubleCarryStep half 1 digit = 0

theorem OddPrimeValuationDistribution.oddDoubleCarryStep_one_of_le {half digit : ℕ} (hlower : half ≤ digit) (hupper : digit < oddBase half) : oddDoubleCarryStep half 1 digit = 1

theorem OddPrimeValuationDistribution.oddDoubleDigitsAux_length (half : ℕ) (digits : List ℕ) (carry : ℕ) : (oddDoubleDigitsAux half digits carry).length = digits.length + 1

theorem OddPrimeValuationDistribution.oddDoubleDigitsAux_lt_base {half : ℕ} (hhalf : 0 < half) {digits : List ℕ} {carry : ℕ} (hcarry : carry ≤ 1) (hdigits : ∀ digit ∈ digits, digit < oddBase half) (value : ℕ) : value ∈ oddDoubleDigitsAux half digits carry → value < oddBase half

theorem OddPrimeValuationDistribution.oddDoubleDigitsAux_ofDigits {half : ℕ} {digits : List ℕ} {carry : ℕ} (hcarry : carry ≤ 1) (hdigits : ∀ digit ∈ digits, digit < oddBase half) : Nat.ofDigits (oddBase half) (oddDoubleDigitsAux half digits carry) = 2 * Nat.ofDigits (oddBase half) digits + carry

theorem OddPrimeValuationDistribution.oddDoubleDigitsAux_sum_add_carries {half : ℕ} {digits : List ℕ} {carry : ℕ} (hcarry : carry ≤ 1) (hdigits : ∀ digit ∈ digits, digit < oddBase half) : (oddDoubleDigitsAux half digits carry).sum + (oddBase half - 1) * oddDoubleCarryCountAux half digits carry = 2 * digits.sum + carry

theorem OddPrimeValuationDistribution.padicValNat_oddPrime_centralBinom_ofDigits_eq_carryCount (half : ℕ) (hhalf : 0 < half) [Fact (Nat.Prime (oddBase half))] (digits : List ℕ) (hdigits : ∀ digit ∈ digits, digit < oddBase half) : padicValNat (oddBase half) (Nat.ofDigits (oddBase half) digits).centralBinom = oddDoubleCarryCountAux half digits 0

In an odd prime base, Kummer's central-binomial valuation is exactly the number of carries produced by doubling any valid padded digit word.