Mixed-radix arithmetic

These lemmas identify the quotient and remainder of one bounded row-major digit. The compiler uses them to cancel coordinate decoding after a checked transform has been composed with a tensor index.

theorem TorchLean.Tensor.Internal.MixedRadix.div_encode (remainder digit radix : Nat) (h : remainder < radix) : (remainder + radix * digit) / radix = digit

Dividing an encoded mixed-radix value by its radix recovers the higher digit.

theorem TorchLean.Tensor.Internal.MixedRadix.mod_encode (remainder digit radix : Nat) (h : remainder < radix) : (remainder + radix * digit) % radix = remainder

Taking the remainder of an encoded mixed-radix value recovers its lower digit.

theorem TorchLean.Tensor.Internal.MixedRadix.div_eq_mod_add_mul_div (value lowerRadix upperRadix : Nat) : value / lowerRadix % upperRadix + upperRadix * (value / (lowerRadix * upperRadix)) = value / lowerRadix

After removing one lower radix, quotient and remainder at the next radix reconstruct the remaining mixed-radix index.