2025-11-27

define a custom data type that represents the sum $d_k{b}^k+d_{k-1}{b}^{k-1}\cdots +d_0$.

• this would structurally resemble a linked list of digits, but you could also ensure that it's the "correct" form, accurately encoding the base-$b$ digits; i.e., that each term $d_k{b}^k$ is the greatest $b^k$ factor that's lesser than $n$.

you would need to define an equivalence (isomorphism) between the natural numbers and your custom list type.

the digital sum function would be exactly as you defined it: it would traverse the custom list-like type, and sum the digits. very cool feature.

for the final proof, you would do induction on your custom type, i.e. prove it for the empty sum, then for your type's equivalent to cons.

• start by applying your previously-defined equivalence to get $n=d_k{b}^k+\cdots d_0$.

• pretty much a one-to-one translation from there!!

define functions that "pull out" individual terms from $n$.

• e.g. a function take-leading-digit that, given a natural number, returns a triple $(d_k,b^k,r)$ such that $d_k{b}^k+r=n$ and $d_k$ is the first digit of $n$.

• these functions will be used in the induction step in the final proof and optionally to define the digit sum function.

most complicated part will probably be defining the digit sum function. it'll require well-founded induction and some remainder/quotient/modulo theorems.

final proof will do induction on $n$ instead of on the list of terms.