add exploratory code for talk, with (mult n) inventing binary numbers, 2^n proof, and attempts to formalize the exponent