Reference · Natural numbers

rainbow.math.nat.divmod

Natural numberssrc/rainbow/math/nat/divmod.clj0 definitions, 8 theorems

Row/column of a FLAT PAIR INDEX, kernel-side, with the bounds the pair-vector families need (Floyd-Warshall's round is a block of n*n components indexed by c = col + row*n). nat/at-most-split : a <= b -> a = b \/ a < b (case on the witness) nat/at-most-or-strict-below : b <= a \/ a < b (totality, through nat/decide-at-most) nat/col-of n c, nat/row-of n c -- a carry recursion on c: the column steps by one and wraps to zero (row steps) when the decided test `succ (succ col) <= n` fails nat/col-of-below : 0 < n -> col-of n c < n nat/col-row-decomposition : 0 < n -> c = col-of n c + (row-of n c) * n nat/row-of-below : 0 < n -> c < n*n -> row-of n c < n (from the decomposition by contradiction: n <= row would put row*n >= n*n above c) nat/pair-index-below : a < n -> b < n -> a + b*n < n*n The wrap test decides `succ (succ col) <= n` rather than `succ col = n` so that its true branch gives the strict bound directly (decide-at-most-true-sound) and its false branch, together with col < n and at-most-split, forces succ col = n.

Depends onmath.nat.strict-below-moremath.nat.at-most-addmath.rational.nnrat.harmonic-convergencemath.rational.signed.decide-completeness

nat/at-most-split :
  (a b : ℕ)
  (h : a ≤ b)
  → proposition/disjunction (a = b) (nat/strict-below a b)

nat/at-most-or-strict-below :
  (a b : ℕ)
  → proposition/disjunction (b ≤ a) (nat/strict-below a b)

nat/col-of :
  (x₁ x₂ : ℕ)
  → ℕ

nat/row-of :
  (x₁ x₂ : ℕ)
  → ℕ

nat/col-of-below :
  (n : ℕ) (hn : nat/strict-below 0 n) (c : ℕ)
  → nat/strict-below (nat/col-of n c) n

nat/col-row-decomposition :
  (n : ℕ) (hn : nat/strict-below 0 n) (c : ℕ)
  → c = algebra/nat-add (nat/col-of n c) (nat/multiply (nat/row-of n c) n)

nat/row-of-below :
  (n : ℕ) (hn : nat/strict-below 0 n) (c : ℕ)
  (hc : nat/strict-below c (nat/multiply n n))
  → nat/strict-below (nat/row-of n c) n

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