Reference · Natural numbers

rainbow.math.nat.distributive

Natural numberssrc/rainbow/math/nat/distributive.clj0 definitions, 2 theorems

Left-distributivity of nat multiplication over addition: a * (b + c) = a * b + a * c for all a, b, c, the semiring law missing from nat_semiring (which has associativity, commutativity of addition, multiply-one-right, but not distributivity). Proved axiom-free by induction on the FIRST factor a (nat/multiply recurses on its left argument). The base a = 0 is reflexive (both sides reduce to 0). The successor step reduces the goal, via the multiply computation rule, to a commutative-monoid rearrangement (b + c) + (p*b + p*c) = (b + p*b) + (c + p*c), which is discharged by routing both sides through the common term b + ((c + p*b) + p*c) using add associativity (algebra/nat-add-associative) and add commutativity (nat/add-commutative), transported with equality/transitive, equality/symmetric, and equality/congruent-function. This unblocks the geometric-convergence denominator closed form den(seq d0 N) = den(d0) * 2^N, the last analytic ingredient of the general forall-epsilon convergence modulus, and fills a fundamental gap in the nat semiring.

nat/multiply-distributes-add :
  (a b c : ℕ)
  → nat/multiply a (algebra/nat-add b c) = algebra/nat-add (nat/multiply a b) (nat/multiply a c)

nat/multiply-zero-right :
  (x : ℕ)
  → nat/multiply x 0 = 0