Exact certificates from bounded comparisons

The exponent search preserves a bracket between powers of two. The significand search preserves a bracket between consecutive integers. Exact comparison at the integer and its half-integer supplies the accuracy certificate consumed by the existing rounding proof.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.AlgebraicRounding.cast_powerOfTwo (exponent : ℤ) : ↑(powerOfTwo exponent) = Flocq.bpow Numerics.binaryRadix exponent

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.AlgebraicRounding.bisect_bracket (accept : ℕ → Bool) (valueAt : ℕ → ℝ) (target : ℝ) (haccept : ∀ (index : ℕ), accept index = true ↔ valueAt index ≤ target) (fuel lower upper : ℕ) (horder : lower < upper) (hspan : upper - lower ≤ 2 ^ fuel) (hlower : valueAt lower ≤ target) (hupper : target < valueAt upper) : valueAt (bisect accept fuel lower upper) ≤ target ∧ target < valueAt (bisect accept fuel lower upper + 1)

A sufficiently deep bounded search ends at adjacent candidates enclosing the target. Only exact comparison and an initial bracket are needed; the proof follows both search branches.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.AlgebraicRounding.lowerExponent_lt_upperExponent (fmt : FloatFormat) : lowerExponent fmt < upperExponent fmt

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.AlgebraicRounding.exponentSpan_pos (fmt : FloatFormat) : 0 < exponentSpan fmt

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.AlgebraicRounding.binade_ge_lowerExponent (fmt : FloatFormat) (compare : ℚ → Ordering) : lowerExponent fmt ≤ binade fmt compare

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.AlgebraicRounding.binade_bounds (fmt : FloatFormat) (compare : ℚ → Ordering) (target : ℝ) (hcompare : ∀ (candidate : ℚ), compare candidate = cmp target ↑candidate) (hlower : Flocq.bpow Numerics.binaryRadix (lowerExponent fmt) ≤ target) (hupper : target < Flocq.bpow Numerics.binaryRadix (upperExponent fmt)) : Flocq.bpow Numerics.binaryRadix (binade fmt compare) ≤ target ∧ target < Flocq.bpow Numerics.binaryRadix (binade fmt compare + 1)

The first search locates consecutive powers of two around the exact target.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.AlgebraicRounding.scaled_compare (compare : ℚ → Ordering) (target : ℝ) (exponent : ℤ) (hcompare : ∀ (candidate : ℚ), compare candidate = cmp target ↑candidate) (candidate : ℚ) : compare (candidate * powerOfTwo exponent) = cmp (target / Flocq.bpow Numerics.binaryRadix exponent) ↑candidate

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.AlgebraicRounding.accuracyAt_represents (compare : ℚ → Ordering) (target : ℝ) (mantissa : ℕ) (hcompare : ∀ (candidate : ℚ), compare candidate = cmp target ↑candidate) (hfloor : ↑mantissa ≤ target ∧ target < ↑mantissa + 1) : accuracyRepresents mantissa (accuracyAt compare mantissa) target

Comparisons with the integer and half-integer determine a valid accuracy certificate.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.AlgebraicRounding.truncatedMantissa_bounds (fmt : FloatFormat) (compare : ℚ → Ordering) (target : ℝ) (exponent : ℤ) (hcompare : ∀ (candidate : ℚ), compare candidate = cmp target ↑candidate) (hlower : 0 ≤ target / Flocq.bpow Numerics.binaryRadix exponent) (hupper : target / Flocq.bpow Numerics.binaryRadix exponent < 2 ^ (fmt.fracWidth + 3)) : ↑(truncatedMantissa fmt compare exponent) ≤ target / Flocq.bpow Numerics.binaryRadix exponent ∧ target / Flocq.bpow Numerics.binaryRadix exponent < ↑(truncatedMantissa fmt compare exponent) + 1

The second search returns the exact integer part of the scaled magnitude.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.AlgebraicRounding.certificate_scaled_bounds (fmt : FloatFormat) (compare : ℚ → Ordering) (target : ℝ) (hcompare : ∀ (candidate : ℚ), compare candidate = cmp target ↑candidate) (hlower : Flocq.bpow Numerics.binaryRadix (lowerExponent fmt) ≤ target) (hupper : target < Flocq.bpow Numerics.binaryRadix (upperExponent fmt)) : 1 ≤ target / Flocq.bpow Numerics.binaryRadix (certificate fmt compare).exponent ∧ target / Flocq.bpow Numerics.binaryRadix (certificate fmt compare).exponent < 2 ^ (fmt.fracWidth + 3)

Two guard bits suffice for a positive truncated mantissa throughout the search interval.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.AlgebraicRounding.certificate_spec (fmt : FloatFormat) (hfmt : fmt.isIEEE = true) (compare : ℚ → Ordering) (target : ℝ) (hcompare : ∀ (candidate : ℚ), compare candidate = cmp target ↑candidate) (hlower : Flocq.bpow Numerics.binaryRadix (lowerExponent fmt) ≤ target) (hupper : target < Flocq.bpow Numerics.binaryRadix (upperExponent fmt)) : have c := certificate fmt compare; c.mantissa ≠ 0 ∧ accuracyRepresents c.mantissa c.accuracy (target / Flocq.bpow Numerics.binaryRadix c.exponent) ∧ c.exponent ≤ fmt.toModel.targetExponent (Float.Model.totalExponent c.mantissa c.exponent)

Every interior oracle result supplies a valid nonzero accuracy certificate and satisfies the normalizer's no-left-shift precondition. All bounds depend on the descriptor, not a fixed width.