Reference · Natural numbers

rainbow.math.nat.pair-index-inverse

Natural numberssrc/rainbow/math/nat/pair_index_inverse.clj0 definitions, 4 theorems

INVERTING THE PAIR INDEX. The families store a matrix entry (u, v) at slot v + u*n and read a slot c back as (row-of n c, col-of n c). nat_divmod proves c = col-of n c + row-of n c * n with col-of n c < n. This module proves the converse, that the decomposition is unique, so a slot names its entry: nat/pair-index-unique-row : a < n -> a' < n -> a + b*n = a' + b'*n -> b = b' nat/pair-index-unique-col : a < n -> a' < n -> a + b*n = a' + b'*n -> a = a' nat/row-of-pair-index : a < n -> row-of n (a + b*n) = b nat/col-of-pair-index : a < n -> col-of n (a + b*n) = a Uniqueness is by trichotomy on b, b': if b < b' then a + b*n < (b+1)*n <= b'*n <= a' + b'*n, which contradicts the equation; symmetrically for b' < b. Then a = a' by cancellation.

Depends onmath.nat.divmod

nat/pair-index-unique-row :
  (n a b a2 b2 : ℕ) (ha : nat/strict-below a n) (ha2 : nat/strict-below a2 n)
  (h : algebra/nat-add a (nat/multiply b n) = algebra/nat-add a2 (nat/multiply b2 n))
  → b = b2

nat/pair-index-unique-col :
  (n a b a2 b2 : ℕ) (ha : nat/strict-below a n) (ha2 : nat/strict-below a2 n)
  (h : algebra/nat-add a (nat/multiply b n) = algebra/nat-add a2 (nat/multiply b2 n))
  → a = a2

nat/row-of-pair-index :
  (n a b : ℕ) (ha : nat/strict-below a n)
  → nat/row-of n (algebra/nat-add a (nat/multiply b n)) = b

nat/col-of-pair-index :
  (n a b : ℕ) (ha : nat/strict-below a n)
  → nat/col-of n (algebra/nat-add a (nat/multiply b n)) = a