Containment for the cached logarithms of j / 32

Each cached entry is logUnreduced on the grid of Internal.logTableBits fractional bits, so it encloses its logarithm (containsReal_logUnreduced), and outward coarsening keeps every real member on a coarser grid (Interval.BinaryGrid.containsReal_coarsen). containsReal_logTableAt? combines the two for every read the table answers.

theorem FloatLib.Numerics.Enclosure.BinaryGrid.containsReal_logTableAt? {index precision : ℕ} {I : Interval ℤ} (h : logTableAt? index precision = some I) : Interval.ContainsReal (Interval.BinaryGrid.decode precision) I (Real.log ↑(↑(index + 24) / 32))

A table read encloses the logarithm of its entry.