A canonical factorial digit is the floor of the scaled preceding remainder

import Definitions.Def_ErdosProblems_Erdos68_CanonicalFactorialDigits
import Mathlib.Algebra.Order.Floor.Ring
import Mathlib.Data.Nat.Factorial.Basic
import Mathlib.Tactic

/-!
# Erdős #68: canonical factorial digits

For the factorial-denominator series

`sum (n >= 2), 1 / (n! - 1)`.

the natural factorial-scale floors give a mixed-radix digit expansion.  This
module develops that expansion for an arbitrary real number: the digits lie
in their canonical ranges, the fractional remainders satisfy the radix
recurrence, and every finite truncation has an explicit remainder term.

The construction is independent of the particular series.  Applied to
Erdős #68, it reduces the digit approach to proving that the canonical
remainder never enters a terminal zero tail.
-/


open scoped BigOperators







/-! ## Rational inputs

For a rational number `a / q`, factorial scaling is integral once `q ≤ n`.
Consequently the canonical digit at radix `n + 1` vanishes.  This is a
termination criterion for rational inputs; it does not assert that the Erdős
#68 series is rational or supply recurrence estimates for its partial sums. -/

open ErdosProblems.Erdos68

theorem ErdosProblems.Erdos68.canonicalDigit_eq_floor_mul_remainder
    (x : ℝ) (m : ℕ) (hm : 1 ≤ m) :
    canonicalDigit x m =
      ⌊(m : ℝ) * canonicalRemainder x (m - 1)⌋ := by sorry