Reference · Natural numbers

rainbow.math.nat.power

Natural numberssrc/rainbow/math/nat/power.clj1 definitions, 5 theorems

Natural-number exponentiation base^exp, defined by recursion on the exponent: power b 0 = 1 power b (succ e) = b * (power b e). This is the growth primitive missing from the arithmetic core: it is what the full-factorial design size n^k, sparse-sampling node counts (branching^depth), and -- crucially -- the geometric-convergence modulus need. The archimedean bound d0 <= eps * 2^n that drives the contraction distance below any threshold is stated in terms of 2^n = power 2 n, so this definition and its monotonicity are the foundation for the general forall-epsilon convergence theorem. Requires nat and nat/multiply (carried by the D63 checkpoint).

nat/power :
  (x₁ x₂ : ℕ)
  → ℕ

nat/power-step-unfold :
  (base exp : ℕ)
  → nat/power base (data/succ exp) = nat/multiply base (nat/power base exp)

nat/power-zero :
  (base : ℕ)
  → nat/power base 0 = 1

nat/power-two-cubed :
  → nat/power 2 3 = 8

nat/power-three-squared :
  → nat/power 3 2 = 9

nat/power-two-to-zero :
  → nat/power 2 0 = 1