A C double by its \(64\) bits of IEEE 754 binary64, in a structure with no equality of its own (equality of the bits is not ==); and the operations that ratpoints applies to doubles, as gcc and glibc compute them with rounding to nearest, ties to even: the comparisons, false when either side is a NaN and otherwise the order of a key (the bits without the sign bit, negated when it is set); negation and fabs; the exact value of a finite double; the double nearest to \(\pm m\, 2^k\) and to \(\pm n/d\); the conversions from and to long, and to unsigned long; and frexp, ldexp and nextafter towards \(\pm \)HUGE_VAL, which pass a signalling NaN on as it is, where glibc quiets it (ratpoints passes them no NaN). These functions model the platform and hold no C range.

For the options of a search (Definition 2.11) and the height bound \(H \ge 1\), the normalized options: the least denominator \(1\) for one below \(1\); the largest denominator \(H\) for one below \(1\) or above \(H\); the depth of the Sturm step capped at \(\mathrm{DBL\_ MANT\_ DIG} + 2 = 55\), beyond which the ends of the intervals of the step would not all be doubles; and the switch of the reversal turned off, for the private bit RATPOINTS_NO_REVERSE_AUTO, when the caller gives search intervals or the normalized range is not \(1, \dots , H\) (find_points.c:4659-4661, find_points.c:4678-4689). The search intervals of a search: for none given, the default interval \([-h, h]\), where \(h\) is the double of \(H\), moved up to the next double when \(h {\lt} 2^{63}\) and the long of \(h\) is below \(H\); otherwise the caller’s intervals, or none, for RATPOINTS_BAD_ARGS, when an interval has not \(l \le u\) or does not begin above the end of the one before it, compared as doubles, so that a NaN end is refused too (find_points.c:4831-4855).

1. (1)

   An end \(x\) (find_points.c:3264-3271, find_points.c:3272-3291, find_points.c:3292-3299): its sign, \(x {\lt} 0\) as in C, so that \(-0.0\) is not negative; for \(|x| {\lt} 2^{63}\), \(|x| = m\, 2^{-s}\) with \(m\) odd or \(s = 0\), except that \(s\) is capped at \(127\), where \(m\, 2^{-s} \ne |x|\) but \(b\, m\, 2^{-s}\) and \(b|x|\) both lie strictly between \(0\) and \(1\) for \(1 \le b {\lt} 2^{63}\); otherwise \(m = 2^{63}\) and \(s = 0\); and the rounding \(r = 2^s - 1\) when the end wants \(b|x|\) rounded up (a lower end with \(x \ge 0\), an upper end with \(x {\lt} 0\)), else \(r = 0\). Its scaled value at \(b\), \(\min (2^{64} - 1, \lfloor (b m + r)/2^s \rfloor )\), is computed on two words (find_points.c:3231-3238).

2. (2)

   The form \((M, C, \mathit{sh})\) of an end (find_points.c:3304-3318), for which \((b M + C) \gg \mathit{sh}\) fits a long for every \(b \le b_{\mathrm{high}}\): \((0, \mp H, 0)\) for an end at or beyond the height bound on its side (\(x \le -H\) at a lower end, \(x \ge H\) at an upper end); \((\pm m, C, s)\), with \(C = 2^s - 1\) at a lower end and \(0\) at an upper end, when \(s {\lt} 64\) and \(m \le \lfloor (2^{63} - 1 - C)/b_{\mathrm{high}} \rfloor \); and none otherwise.

3. (3)

   The bounds of the search intervals (find_points.c:3323-3340): the two ends of each interval, which is taken inline, with the forms of its ends, when \(H \le 2^{63} - 65\) and both ends have a form, and otherwise gets the forms of an empty interval.

4. (4)

   The bits of an interval at \(b\) for a class of the numerators (find_points.c:3410-3434): \(\mathit{lo} = \lceil b l \rceil \) and \(\mathit{hi} = \lfloor b u \rfloor \) from the forms; the code \(2\) for \(\mathit{lo} {\gt} H\); for \(\mathit{hi} {\lt} -H\) the code \(1\) if the interval is taken inline, and otherwise what interval_bits_exact computes from the scaled ends (find_points.c:3381-3406); and otherwise the code \(0\) with the bits of the first and the last numerator of the class in \(\max (\mathit{lo}, -H), \dots , \min (\mathit{hi}, H)\).

5. (5)

   The bounds of an interval represent a range \(\mathit{lo}, \dots , \mathit{hi}\) at \(b\) when, for every class of a packing (Chapter 9: stride \(2^k\) with \(k {\lt} \mathrm{numStrides}\) and \(k \le 6\), residue \(a_0 {\lt} 2^k\)), their bits have the code \(2\) only for a range above \(H\), the code \(1\) only for one below \(-H\), and otherwise the bits of the numerators of the class in \(\max (\mathit{lo}, -H), \dots , \min (\mathit{hi}, H)\). The bounds of a run give a list of ranges at \(b\) when there is one for each interval, represented by its bounds, each with \(\mathit{lo} \le \mathit{hi} + 1\), increasing and strictly apart.

The bisection, the nested function iterate of gcc (sturm.c:197-208, sturm.c:228-233, sturm.c:261-267), works on intervals whose ends are \(n/2^e\), with longs \(n\) and \(e\), or \(\mp \infty \), written \(\mp \mathrm{LONG\_ MAX}\) with the exponent \(0\). It evaluates the rows of the chain at \(n/2^e\) by Horner’s rule in integers, which computes \(2^{e \deg s}\) times the value of the row \(s\), and counts their sign changes, zeros skipped. An interval with the counts \(c_l\), \(c_r\) at its ends and the signs \(\sigma _l\), \(\sigma _r\) of \(f\) just inside them is dropped when \(c_l = c_r\) and \(\sigma _l {\lt} 0\); it is kept when \(c_l = c_r\) and \(\sigma _l {\gt} 0\), or at the depth of the step, its ends converted to doubles, \(\mathrm{ldexp}((\mathrm{double})\, n, -e)\), and appended to the intervals kept, or joined to the last of them when that ends at its lower end (== of doubles); and otherwise it is split at its midpoint \(m\), the left half bisected first, both halves with the count and the sign of \(f\) at \(m\), except that at a root \(m\) the left half gets the count plus \(1\) and \(-\mathrm{sign}\, f'(m)\), the right half \(\mathrm{sign}\, f'(m)\). The midpoint is \(0\) for \([-\infty , +\infty ]\); \(-1\) or \(2 n_r\) for \([-\infty , n_r]\) and \(1\) or \(2 n_l\) for \([n_l, +\infty ]\), as the finite end is \(0\) or not; and otherwise half the sum of the ends over the larger denominator. An interval is well formed at the depth \(\delta \) when it has one of the four shapes that the bisection meets (the whole line; an infinite interval whose finite end, of exponent \(0\), is \(0\) or on its side of \(0\); two finite ends, equal exponents being \(0\)), its exponents lie between \(0\) and \(\delta \), its finite numerators over the larger exponent are at most \(2^{\delta }/4\) in absolute value from the depth \(1\) on, and its ends increase.

The intersection with the caller’s intervals goes by two cursors: of the two current intervals, compared as doubles, the one that begins first is skipped when it ends before the other begins; otherwise their intersection is noted and the cursor of the one that ends first moves on (sturm.c:289-322). The Sturm step on \(f\) of degree \(d \ge 1\) with \(c_d \ne 0\) (sturm.c:86-97, sturm.c:177-190, sturm.c:269-273): none when the remainder chain is none; no interval when the counts at \(\mp \infty \) agree, so that \(f\) has no real root, and \(c_0 {\lt} 0\); otherwise the intervals that the bisection keeps from \([-\infty , +\infty ]\), started with the counts and the signs of \(f\) at \(\mp \infty \), intersected with the caller’s intervals. The Sturm step of the search, on the polynomial that the reversal check hands on, at the normalized depth (find_points.c:4879-4892): with the step off, the intervals as they are; the refusal \(\mathrm{notSquarefree}\) when the chain is none; the intervals left, when there are some; and when there are none, none for an even \(d\) whose leading coefficient is not a square, so that the search returns at once, there being no point at infinity either, and otherwise no intervals with the flag sturm_empty, by which the search delivers the points at infinity only.

A definition of the proofs, not of the model: for the polynomial \(c\) of degree \(d\) that the reversal check hands on, \(H\) and the options, none when the search intervals are none or the Sturm step of the search refuses or returns at once; no interval when it sets sturm_empty; and otherwise the values of the intervals that it leaves. For well-formed intervals of the caller:

1. (1)

   every \(x\) in the region lies in the caller’s intervals, or the caller gives none;

2. (2)

   if the chain does not fail when the step is on, the region is none only for an even \(d\) whose leading coefficient is not a square;

3. (3)

   assuming Sturm’s theorem when the step is on, for \(0 {\lt} d {\lt} 2^{57}\) the degree of \(c\), \(1 \le H {\lt} 2^{63}\) and a chain that does not fail when the step is on: every \(a/b\) with \(b {\gt} 0\), \(|a| \le H\) and \(F(a, b) \ge 0\) in the caller’s intervals, or anywhere when there are none, lies in the region, which is not none.