doc-next-gen

Init.Data.Int.DivMod.Basic

Module docstring

{"## Quotient and remainder

There are three main conventions for integer division, referred here as the E, F, T rounding conventions. All three pairs satisfy the identity x % y + (x / y) * y = x unconditionally, and satisfy x / 0 = 0 and x % 0 = x.

Historical notes

In early versions of Lean, the typeclasses provided by / and % were defined in terms of tdiv and tmod, and these were named simply as div and mod.

However we decided it was better to use ediv and emod for the default typeclass instances, as they are consistent with the conventions used in SMT-LIB, and Mathlib, and often mathematical reasoning is easier with these conventions. At that time, we did not rename div and mod to tdiv and tmod (along with all their lemma).

In September 2024, we decided to do this rename (with deprecations in place), and later we intend to rename ediv and emod to div and mod, as nearly all users will only ever need to use these functions and their associated lemmas.

In December 2024, we removed div and mod, but have not yet renamed ediv and emod. ","### E-rounding division This pair satisfies 0 ≤ emod x y < natAbs y for y ≠ 0. ","### T-rounding division ","### F-rounding division This pair satisfies fdiv x y = floor (x / y). ","# bmod (\"balanced\" mod)

Balanced mod (and balanced div) are a division and modulus pair such that b * (Int.bdiv a b) + Int.bmod a b = a and -b/2 ≤ Int.bmod a b < b/2 for all a : Int and b > 0.

Note that unlike emod, fmod, and tmod, bmod takes a natural number as the second argument, rather than an integer.

This function is used in omega as well as signed bitvectors. "}

Int.ediv definition
: (@& Int) → (@& Int) → Int
Full source 
/--
Integer division that uses the E-rounding convention. Usually accessed via the `/` operator.
Division by zero is defined to be zero, rather than an error.

In the E-rounding convention (Euclidean division), `Int.emod x y` satisfies `0 ≤ Int.emod x y < Int.natAbs y`
for `y ≠ 0` and `Int.ediv` is the unique function satisfying `Int.emod x y + (Int.edivx y) * y = x`
for `y ≠ 0`.

This means that `Int.ediv x y` is `⌊x / y⌋` when `y > 0` and `⌈x / y⌉` when `y < 0`.

This function is overridden by the compiler with an efficient implementation. This definition is
the logical model.

Examples:
* `(7 : Int) / (0 : Int) = 0`
* `(0 : Int) / (7 : Int) = 0`
* `(12 : Int) / (6 : Int) = 2`
* `(12 : Int) / (-6 : Int) = -2`
* `(-12 : Int) / (6 : Int) = -2`
* `(-12 : Int) / (-6 : Int) = 2`
* `(12 : Int) / (7 : Int) = 1`
* `(12 : Int) / (-7 : Int) = -1`
* `(-12 : Int) / (7 : Int) = -2`
* `(-12 : Int) / (-7 : Int) = 2`
-/
@[extern "lean_int_ediv"]
def ediv : (@& Int) → (@& Int) → Int
  | ofNat m, ofNat n => ofNat (m / n)
  | ofNat m, -[n+1]  => -ofNat (m / succ n)
  | -[_+1],  0       => 0
  | -[m+1],  ofNat (succ n) => -[m / succ n +1]
  | -[m+1],  -[n+1]  => ofNat (succ (m / succ n))
Euclidean division on integers
Informal description
The Euclidean division function on integers, denoted $x \div y$, is defined for all integers $x$ and $y$ with the following properties: 1. For $y \neq 0$, it satisfies $0 \leq x \bmod y < |y|$ where $\bmod$ is the corresponding modulus operation. 2. Division by zero is defined to return zero. 3. For $y > 0$, $x \div y = \lfloor x / y \rfloor$. 4. For $y < 0$, $x \div y = \lceil x / y \rceil$. This function is part of the E-rounding convention for integer division.
Int.emod definition
: (@& Int) → (@& Int) → Int
Full source 
/--
Integer modulus that uses the E-rounding convention. Usually accessed via the `%` operator.

In the E-rounding convention (Euclidean division), `Int.emod x y` satisfies `0 ≤ Int.emod x y < Int.natAbs y`
for `y ≠ 0` and `Int.ediv` is the unique function satisfying `Int.emod x y + (Int.edivx y) * y = x`
for `y ≠ 0`.

This function is overridden by the compiler with an efficient implementation. This definition is
the logical model.

Examples:
* `(7 : Int) % (0 : Int) = 7`
* `(0 : Int) % (7 : Int) = 0`
* `(12 : Int) % (6 : Int) = 0`
* `(12 : Int) % (-6 : Int) = 0`
* `(-12 : Int) % (6 : Int) = 0`
* `(-12 : Int) % (-6 : Int) = 0`
* `(12 : Int) % (7 : Int) = 5`
* `(12 : Int) % (-7 : Int) = 5`
* `(-12 : Int) % (7 : Int) = 2`
* `(-12 : Int) % (-7 : Int) = 2`
-/
@[extern "lean_int_emod"]
def emod : (@& Int) → (@& Int) → Int
  | ofNat m, n => ofNat (m % natAbs n)
  | -[m+1],  n => subNatNat (natAbs n) (succ (m % natAbs n))
Euclidean modulus on integers
Informal description
The Euclidean modulus function on integers, denoted $x \bmod y$, is defined for all integers $x$ and $y$ with the following properties: 1. For $y \neq 0$, it satisfies $0 \leq x \bmod y < |y|$. 2. Modulus by zero is defined to return $x$. 3. For positive $n$, $m \bmod n$ is equivalent to the modulus operation on natural numbers. 4. For negative $x$, $-x \bmod n$ is computed as $n - (x+1 \bmod n) - 1$. This function is part of the E-rounding convention for integer division and modulus.
Int.instDiv instance
: Div Int
Full source 
/--
The `Div Int` and `Mod Int` instances use `Int.ediv` and `Int.emod` for compatibility with SMT-LIB and
because mathematical reasoning tends to be easier.
-/
instance : Div Int where
  div := Int.ediv
Euclidean Division on Integers
Informal description
The integers $\mathbb{Z}$ are equipped with a division operation following the Euclidean (E-rounding) convention, where for any integers $x$ and $y$, the division $x / y$ satisfies: 1. For $y \neq 0$, $0 \leq x \bmod y < |y|$ where $\bmod$ is the corresponding modulus operation. 2. Division by zero is defined to return zero. 3. For $y > 0$, $x / y = \lfloor x / y \rfloor$. 4. For $y < 0$, $x / y = \lceil x / y \rceil$. This operation is compatible with SMT-LIB and simplifies mathematical reasoning.
Int.instMod instance
: Mod Int
Full source 
/--
The `Div Int` and `Mod Int` instances use `Int.ediv` and `Int.emod` for compatibility with SMT-LIB and
because mathematical reasoning tends to be easier.
-/
instance : Mod Int where
  mod := Int.emod
Euclidean Modulus Operation on Integers
Informal description
The integers $\mathbb{Z}$ are equipped with a modulus operation following the Euclidean (E-rounding) convention, where for any integers $x$ and $y$, the modulus $x \bmod y$ satisfies: 1. For $y \neq 0$, $0 \leq x \bmod y < |y|$. 2. Modulus by zero is defined to return $x$. This operation is compatible with SMT-LIB and simplifies mathematical reasoning.
Int.ofNat_ediv theorem
(m n : Nat) : (↑(m / n) : Int) = ↑m / ↑n
Full source 
@[norm_cast] theorem ofNat_ediv (m n : Nat) : (↑(m / n) : Int) = ↑m / ↑n := rfl
Preservation of Floor Division under Natural Number Embedding in Integers
Informal description
For any natural numbers $m$ and $n$, the canonical image of the floor division $m / n$ in the integers equals the Euclidean division of the canonical images of $m$ and $n$ in the integers. In other words, $\lfloor m / n \rfloor = \lfloor m / n \rfloor$ when viewed as integer division.
Int.ofNat_ediv_ofNat theorem
{a b : Nat} : (↑a / ↑b : Int) = (a / b : Nat)
Full source 
theorem ofNat_ediv_ofNat {a b : Nat} : (↑a / ↑b : Int) = (a / b : Nat) := rfl
Preservation of Division under Natural Number to Integer Cast
Informal description
For any natural numbers $a$ and $b$, the Euclidean division of the integer casts of $a$ and $b$ equals the natural number cast of the floor division of $a$ by $b$, i.e., $\lceil a \rceil / \lceil b \rceil = \lceil a / b \rceil$ where $/$ denotes Euclidean division on integers and floor division on natural numbers respectively.
Int.negSucc_ediv_ofNat_succ theorem
{a b : Nat} : ((-[a+1]) / ↑(b + 1) : Int) = -[a / succ b+1]
Full source 
@[norm_cast]
theorem negSucc_ediv_ofNat_succ {a b : Nat} : ((-[a+1]) / ↑(b+1) : Int) = -[a / succ b +1] := rfl
Euclidean Division of Negative Integer by Positive Integer
Informal description
For any natural numbers $a$ and $b$, the Euclidean division of the negative integer $- (a + 1)$ by the positive integer $b + 1$ equals the negative integer $- \left(\left\lfloor \frac{a}{b + 1} \right\rfloor + 1\right)$.
Int.negSucc_ediv_negSucc theorem
{a b : Nat} : ((-[a+1]) / (-[b+1]) : Int) = ((a / (b + 1)) + 1 : Nat)
Full source 
theorem negSucc_ediv_negSucc {a b : Nat} : ((-[a+1]) / (-[b+1]) : Int) = ((a / (b + 1)) + 1 : Nat) := rfl
Euclidean Division of Negative Successors in Integers
Informal description
For any natural numbers $a$ and $b$, the Euclidean division of the negative successor $-a-1$ by the negative successor $-b-1$ in the integers equals the successor of the floor division of $a$ by $b+1$ in the natural numbers. That is, $$\frac{-a-1}{-b-1} = \left\lfloor\frac{a}{b+1}\right\rfloor + 1$$
Int.ofNat_ediv_negSucc theorem
{a b : Nat} : (ofNat a / (-[b+1])) = -(a / (b + 1) : Nat)
Full source 
theorem ofNat_ediv_negSucc {a b : Nat} : (ofNat a / (-[b+1])) = -(a / (b + 1) : Nat) := rfl
Euclidean Division of Natural Number by Negative Successor: $a / (-b-1) = -\left\lfloor \frac{a}{b+1} \right\rfloor$
Informal description
For any natural numbers $a$ and $b$, the Euclidean division of the non-negative integer $a$ by the negative integer $-b-1$ equals the negation of the floor division of $a$ by $b+1$ in the natural numbers. That is, $$a / (-b-1) = -\left\lfloor \frac{a}{b+1} \right\rfloor$$
Int.negSucc_emod_ofNat theorem
{a b : Nat} : -[a+1] % (b : Int) = subNatNat b (succ (a % b))
Full source 
theorem negSucc_emod_ofNat {a b : Nat} : -[a+1] % (b : Int) = subNatNat b (succ (a % b)) := rfl
Euclidean Modulus of Negative Successor by Natural Number: $(-a-1) \bmod b = b - (a \bmod b + 1)$
Informal description
For any natural numbers $a$ and $b$, the Euclidean modulus of the negative successor $-a-1$ by the natural number $b$ (viewed as an integer) equals the result of subtracting $(a \bmod b) + 1$ from $b$ in the natural numbers. That is, $$(-a-1) \bmod b = b - (a \bmod b + 1)$$
Int.negSucc_emod_negSucc theorem
{a b : Nat} : -[a+1] % -[b+1] = subNatNat (b + 1) (succ (a % (b + 1)))
Full source 
theorem negSucc_emod_negSucc {a b : Nat} : -[a+1] % -[b+1] = subNatNat (b + 1) (succ (a % (b + 1))) := rfl
Euclidean Modulus of Negative Successor by Negative Successor: $(-a-1) \bmod (-b-1) = (b + 1) - (a \bmod (b + 1) + 1)$
Informal description
For any natural numbers $a$ and $b$, the Euclidean modulus of the negative integer $-a-1$ by the negative integer $-b-1$ is equal to $(b + 1) - (a \bmod (b + 1) + 1)$. That is, $$(-a-1) \bmod (-b-1) = (b + 1) - (a \bmod (b + 1) + 1)$$
Int.tdiv definition
: (@& Int) → (@& Int) → Int
Full source 
/--
Integer division using the T-rounding convention.

In [the T-rounding convention][t-rounding] (division with truncation), all rounding is towards zero.
Division by 0 is defined to be 0. In this convention, `Int.tmod a b + b * (Int.tdiv a b) = a`.

[t-rounding]: https://dl.acm.org/doi/pdf/10.1145/128861.128862

This function is overridden by the compiler with an efficient implementation. This definition is the
logical model.

Examples:
* `(7 : Int).tdiv (0 : Int) = 0`
* `(0 : Int).tdiv (7 : Int) = 0`
* `(12 : Int).tdiv (6 : Int) = 2`
* `(12 : Int).tdiv (-6 : Int) = -2`
* `(-12 : Int).tdiv (6 : Int) = -2`
* `(-12 : Int).tdiv (-6 : Int) = 2`
* `(12 : Int).tdiv (7 : Int) = 1`
* `(12 : Int).tdiv (-7 : Int) = -1`
* `(-12 : Int).tdiv (7 : Int) = -1`
* `(-12 : Int).tdiv (-7 : Int) = 1`
-/
@[extern "lean_int_div"]
def tdiv : (@& Int) → (@& Int) → Int
  | ofNat m, ofNat n =>  ofNat (m / n)
  | ofNat m, -[n +1] => -ofNat (m / succ n)
  | -[m +1], ofNat n => -ofNat (succ m / n)
  | -[m +1], -[n +1] =>  ofNat (succ m / succ n)
Truncating integer division
Informal description
The function `Int.tdiv` implements integer division using the T-rounding convention, where division rounds towards zero. For any integers $a$ and $b$, the result of `Int.tdiv a b` is the integer quotient obtained by dividing $a$ by $b$ and truncating towards zero. Division by zero is defined to return zero. This function satisfies the identity $a = b \cdot \text{Int.tdiv } a b + \text{Int.tmod } a b$ for all integers $a$ and $b$.
Int.tmod definition
: (@& Int) → (@& Int) → Int
Full source 
/-- Integer modulo using the T-rounding convention.

In [the T-rounding convention][t-rounding] (division with truncation), all rounding is towards zero.
Division by 0 is defined to be 0 and `Int.tmod a 0 = a`.

In this convention, `Int.tmod a b + b * (Int.tdiv a b) = a`. Additionally,
`Int.natAbs (Int.tmod a b) = Int.natAbs a % Int.natAbs b`, and when `b` does not divide `a`,
`Int.tmod a b` has the same sign as `a`.

[t-rounding]: https://dl.acm.org/doi/pdf/10.1145/128861.128862

This function is overridden by the compiler with an efficient implementation. This definition is the
logical model.

Examples:
* `(7 : Int).tmod (0 : Int) = 7`
* `(0 : Int).tmod (7 : Int) = 0`
* `(12 : Int).tmod (6 : Int) = 0`
* `(12 : Int).tmod (-6 : Int) = 0`
* `(-12 : Int).tmod (6 : Int) = 0`
* `(-12 : Int).tmod (-6 : Int) = 0`
* `(12 : Int).tmod (7 : Int) = 5`
* `(12 : Int).tmod (-7 : Int) = 5`
* `(-12 : Int).tmod (7 : Int) = -5`
* `(-12 : Int).tmod (-7 : Int) = -5`
-/
@[extern "lean_int_mod"]
def tmod : (@& Int) → (@& Int) → Int
  | ofNat m, ofNat n =>  ofNat (m % n)
  | ofNat m, -[n +1] =>  ofNat (m % succ n)
  | -[m +1], ofNat n => -ofNat (succ m % n)
  | -[m +1], -[n +1] => -ofNat (succ m % succ n)
Truncating integer modulo operation
Informal description
The function `Int.tmod` implements the integer modulo operation using the T-rounding convention, where the remainder has the same sign as the dividend. For any integers $a$ and $b$, the result satisfies: 1. $a = b \cdot \text{Int.tdiv } a b + \text{Int.tmod } a b$, 2. $\text{Int.natAbs } (\text{Int.tmod } a b) = \text{Int.natAbs } a \% \text{Int.natAbs } b$, 3. If $b \neq 0$ and $b$ does not divide $a$, then $\text{Int.tmod } a b$ has the same sign as $a$. Division by zero is defined by $\text{Int.tmod } a 0 = a$.
Int.ofNat_tdiv theorem
(m n : Nat) : ↑(m / n) = tdiv ↑m ↑n
Full source 
theorem ofNat_tdiv (m n : Nat) : ↑(m / n) = tdiv ↑m ↑n := rfl
Embedding Preserves Floor Division under Truncating Division
Informal description
For any natural numbers $m$ and $n$, the canonical embedding of the floor division $m / n$ into the integers equals the truncating division of the embeddings of $m$ and $n$, i.e., $\uparrow(m / n) = \text{tdiv}(\uparrow m, \uparrow n)$.
Int.fdiv definition
: Int → Int → Int
Full source 
/--
Integer division using the F-rounding convention.

In the F-rounding convention (flooring division), `Int.fdiv x y` satisfies `Int.fdiv x y = ⌊x / y⌋`
and `Int.fmod` is the unique function satisfying `Int.fmod x y + (Int.fdiv x y) * y = x`.

Examples:
* `(7 : Int).fdiv (0 : Int) = 0`
* `(0 : Int).fdiv (7 : Int) = 0`
* `(12 : Int).fdiv (6 : Int) = 2`
* `(12 : Int).fdiv (-6 : Int) = -2`
* `(-12 : Int).fdiv (6 : Int) = -2`
* `(-12 : Int).fdiv (-6 : Int) = 2`
* `(12 : Int).fdiv (7 : Int) = 1`
* `(12 : Int).fdiv (-7 : Int) = -2`
* `(-12 : Int).fdiv (7 : Int) = -2`
* `(-12 : Int).fdiv (-7 : Int) = 1`
-/
def fdiv : Int → Int → Int
  | 0,       _       => 0
  | ofNat m, ofNat n => ofNat (m / n)
  | ofNat (succ m), -[n+1] => -[m / succ n +1]
  | -[_+1],  0       => 0
  | -[m+1],  ofNat (succ n) => -[m / succ n +1]
  | -[m+1],  -[n+1]  => ofNat (succ m / succ n)
Flooring division on integers
Informal description
The flooring division function on integers, denoted $\lfloor x / y \rfloor$, satisfies the identity $x \operatorname{fmod} y + (x \operatorname{fdiv} y) \cdot y = x$ for all integers $x$ and $y$, with the convention that $x \operatorname{fdiv} 0 = 0$ and $x \operatorname{fmod} 0 = x$. Specifically: - For nonnegative integers $m$ and $n$, $\operatorname{fdiv} m n = \lfloor m / n \rfloor$ - For negative denominators, it follows the flooring convention (e.g., $\operatorname{fdiv} 12 (-6) = -2$) - For negative numerators, it also follows the flooring convention (e.g., $\operatorname{fdiv} (-12) 6 = -2$)
Int.fmod definition
: Int → Int → Int
Full source 
/--
Integer modulus using the F-rounding convention.

In the F-rounding convention (flooring division), `Int.fdiv x y` satisfies `Int.fdiv x y = ⌊x / y⌋`
and `Int.fmod` is the unique function satisfying `Int.fmod x y + (Int.fdiv x y) * y = x`.

Examples:

* `(7 : Int).fmod (0 : Int) = 7`
* `(0 : Int).fmod (7 : Int) = 0`

* `(12 : Int).fmod (6 : Int) = 0`
* `(12 : Int).fmod (-6 : Int) = 0`
* `(-12 : Int).fmod (6 : Int) = 0`
* `(-12 : Int).fmod (-6 : Int) = 0`

* `(12 : Int).fmod (7 : Int) = 5`
* `(12 : Int).fmod (-7 : Int) = -2`
* `(-12 : Int).fmod (7 : Int) = 2`
* `(-12 : Int).fmod (-7 : Int) = -5`

-/
def fmod : Int → Int → Int
  | 0,       _       => 0
  | ofNat m, ofNat n => ofNat (m % n)
  | ofNat (succ m),  -[n+1]  => subNatNat (m % succ n) n
  | -[m+1],  ofNat n => subNatNat n (succ (m % n))
  | -[m+1],  -[n+1]  => -ofNat (succ m % succ n)
Flooring modulus on integers
Informal description
The integer modulus function using the F-rounding (flooring division) convention, denoted $\operatorname{fmod}$, satisfies the identity $x \operatorname{fmod} y + \lfloor x / y \rfloor \cdot y = x$ for all integers $x$ and $y$, with the convention that $x \operatorname{fmod} 0 = x$. Specifically: - For nonnegative integers $m$ and $n$, $\operatorname{fmod} m n = m \% n$ (the usual remainder) - For negative denominators, it follows the flooring convention (e.g., $\operatorname{fmod} 12 (-7) = -2$) - For negative numerators, it also follows the flooring convention (e.g., $\operatorname{fmod} (-12) 7 = 2$)
Int.ofNat_fdiv theorem
: ∀ m n : Nat, ↑(m / n) = fdiv ↑m ↑n
Full source 
theorem ofNat_fdiv : ∀ m n : Nat, ↑(m / n) = fdiv ↑m ↑n
  | 0, _ => by simp [fdiv]
  | succ _, _ => rfl
Natural Number Floor Division Embeds to Integer Floor Division
Informal description
For any natural numbers $m$ and $n$, the canonical embedding of the floor division $m / n$ from natural numbers to integers equals the flooring division of the embedded values, i.e., $\lfloor m / n \rfloor = \lfloor m / n \rfloor$ where the left side is natural number division and the right side is integer flooring division.
Int.bmod definition
(x : Int) (m : Nat) : Int
Full source 
/--
Balanced modulus.

This version of integer modulus uses the balanced rounding convention, which guarantees that
`-m / 2 ≤ Int.bmod x m < m/2` for `m ≠ 0` and `Int.bmod x m` is congruent to `x` modulo `m`.

If `m = 0`, then `Int.bmod x m = x`.

Examples:
* `(7 : Int).bmod 0 = 7`
* `(0 : Int).bmod 7 = 0`
* `(12 : Int).bmod 6 = 0`
* `(12 : Int).bmod 7 = -2`
* `(12 : Int).bmod 8 = -4`
* `(12 : Int).bmod 9 = 3`
* `(-12 : Int).bmod 6 = 0`
* `(-12 : Int).bmod 7 = 2`
* `(-12 : Int).bmod 8 = -4`
* `(-12 : Int).bmod 9 = -3`
-/
def bmod (x : Int) (m : Nat) : Int :=
  let r := x % m
  if r < (m + 1) / 2 then
    r
  else
    r - m
Balanced modulus function on integers
Informal description
The balanced modulus function `Int.bmod` takes an integer $x$ and a natural number $m$ and returns an integer $r$ such that: 1. If $m = 0$, then $r = x$. 2. If $m \neq 0$, then $-m/2 \leq r < m/2$ and $r \equiv x \pmod{m}$. More precisely, the function computes $r$ as the remainder of $x$ modulo $m$ (using Euclidean division), and adjusts it to lie in the balanced range $[-m/2, m/2)$ by subtracting $m$ if necessary.
Int.bdiv definition
(x : Int) (m : Nat) : Int
Full source 
/--
Balanced division.

This returns the unique integer so that `b * (Int.bdiv a b) + Int.bmod a b = a`.

Examples:
* `(7 : Int).bdiv 0 = 0`
* `(0 : Int).bdiv 7 = 0`
* `(12 : Int).bdiv 6 = 2`
* `(12 : Int).bdiv 7 = 2`
* `(12 : Int).bdiv 8 = 2`
* `(12 : Int).bdiv 9 = 1`
* `(-12 : Int).bdiv 6 = -2`
* `(-12 : Int).bdiv 7 = -2`
* `(-12 : Int).bdiv 8 = -1`
* `(-12 : Int).bdiv 9 = -1`
-/
def bdiv (x : Int) (m : Nat) : Int :=
  if m = 0 then
    0
  else
    let q := x / m
    let r := x % m
    if r < (m + 1) / 2 then
      q
    else
      q + 1
Balanced division of integers
Informal description
The balanced division function `Int.bdiv` takes an integer $x$ and a natural number $m$ and returns the unique integer $q$ such that $m \cdot q + \text{Int.bmod}\ x\ m = x$ and the remainder $\text{Int.bmod}\ x\ m$ satisfies $-\frac{m}{2} \leq \text{Int.bmod}\ x\ m < \frac{m}{2}$ when $m > 0$. If $m = 0$, the result is $0$. More precisely, when $m \neq 0$, the function computes the Euclidean quotient $q = x / m$ and remainder $r = x \% m$, then adjusts $q$ by $+1$ if $r \geq \frac{m+1}{2}$ to ensure the remainder falls in the balanced range.