Verified fixed-word division candidates

The radix-2^32 runtime loop is a candidate generator. Its quotient and remainder are accepted when native multiplication and addition independently certify the exact Euclidean division equation and remainder bound. If that check rejects the candidate, the runtime selects a restoring accumulator; this module proves that accumulator equal to the logical recurrence and certifies its result on normalized inputs of precision + 1 bits with 64 < precision ≤ 126.

theorem FloatLib.Numerics.FixedWord.CertifiedDivision.CandidateShift.toNat_bounds (precision : ℕ) (hprecision : 64 < precision ∧ precision ≤ 126) (shift : CandidateShift) : 64 < toNat precision shift ∧ toNat precision shift < 128

Both candidate shifts of an in-range precision lie strictly between one and two words.

theorem FloatLib.Numerics.FixedWord.CertifiedDivision.certificate_complete (precision : ℕ) (hprecision : 64 < precision ∧ precision ≤ 126) (num den : UInt128) (shift : CandidateShift) (quotient remainder : UInt128) (hdecomposition : quotient.toNat * den.toNat + remainder.toNat = num.toNat * 2 ^ CandidateShift.toNat precision shift) (hremainder : remainder.toNat < den.toNat) : certificate precision num den shift quotient remainder = true

The executable certificate accepts every representable Euclidean decomposition for the two shifts used by two-limb division.

This is completeness of the independent checker, not of the speculative Algorithm D generator.

theorem FloatLib.Numerics.FixedWord.CertifiedDivision.certificate_sound (precision : ℕ) (hprecision : 64 < precision ∧ precision ≤ 126) (num den : UInt128) (shift : CandidateShift) (quotient remainder : UInt128) (hvalid : certificate precision num den shift quotient remainder = true) : quotient.toNat * den.toNat + remainder.toNat = num.toNat * 2 ^ CandidateShift.toNat precision shift ∧ remainder.toNat < den.toNat

A successful native certificate proves the exact quotient/remainder decomposition and Euclidean remainder bound. The proof does not depend on the radix-2^32 candidate generator.

theorem FloatLib.Numerics.FixedWord.CertifiedDivision.restoringCandidate_eq_quotientSteps128 (precision : ℕ) (num den : UInt128) (shift : CandidateShift) : restoringCandidate precision num den shift = RestoringQuotient.quotientSteps128 den (CandidateShift.toNat precision shift) (restoringInitial num den)

The allocation-light restoring repair agrees with the logical two-limb recurrence.

Runtime code calls the primitive-word accumulator directly. This theorem is the proof boundary that lets the mathematical argument continue through quotientSteps128.

theorem FloatLib.Numerics.FixedWord.CertifiedDivision.restoringCandidate_complete (precision : ℕ) (hprecision : 64 < precision ∧ precision ≤ 126) (num den : UInt128) (shift : CandidateShift) (hnum : 2 ^ precision ≤ num.toNat ∧ num.toNat < 2 ^ (precision + 1)) (hden : 2 ^ precision ≤ den.toNat ∧ den.toNat < 2 ^ (precision + 1)) (hshift : shift = if den.toNat ≤ num.toNat then CandidateShift.exact else CandidateShift.extra) : certificate precision num den shift (restoringCandidate precision num den shift).quotient (restoringCandidate precision num den shift).remainder = true

The restoring repair produces a certified candidate for normalized precision + 1-bit significands.

The shift is precision when the numerator is at least the denominator and precision + 1 otherwise. Those are exactly the two cases selected by the two-limb backends.

theorem FloatLib.Numerics.FixedWord.CertifiedDivision.checkedCandidate_eq_repair_of_certificate_false (precision : ℕ) (num den : UInt128) (shift : CandidateShift) (hrejected : certificate precision num den shift (candidate precision num den shift).1 (candidate precision num den shift).2 = false) : checkedCandidate precision num den shift = { quotient := (restoringCandidate precision num den shift).quotient, remainder := (restoringCandidate precision num den shift).remainder }

An independently rejected Algorithm D candidate selects the restoring repair.

The conclusion holds for any operands whose candidate fails the certificate.

theorem FloatLib.Numerics.FixedWord.CertifiedDivision.checkedCandidate_complete (precision : ℕ) (hprecision : 64 < precision ∧ precision ≤ 126) (num den : UInt128) (shift : CandidateShift) (hnum : 2 ^ precision ≤ num.toNat ∧ num.toNat < 2 ^ (precision + 1)) (hden : 2 ^ precision ≤ den.toNat ∧ den.toNat < 2 ^ (precision + 1)) (hshift : shift = if den.toNat ≤ num.toNat then CandidateShift.exact else CandidateShift.extra) : certificate precision num den shift (checkedCandidate precision num den shift).quotient (checkedCandidate precision num den shift).remainder = true

The checked candidate is complete on the normalized two-limb division domain.

The fast candidate is used when its independent certificate succeeds; otherwise the proved restoring loop supplies the quotient and remainder. Thus the selected pair itself is certified, without a second runtime check or an unreachable backend fallback.

theorem FloatLib.Numerics.FixedWord.CertifiedDivision.checkedCandidate_sound (precision : ℕ) (hprecision : 64 < precision ∧ precision ≤ 126) (num den : UInt128) (shift : CandidateShift) (hnum : 2 ^ precision ≤ num.toNat ∧ num.toNat < 2 ^ (precision + 1)) (hden : 2 ^ precision ≤ den.toNat ∧ den.toNat < 2 ^ (precision + 1)) (hshift : shift = if den.toNat ≤ num.toNat then CandidateShift.exact else CandidateShift.extra) : (checkedCandidate precision num den shift).quotient.toNat * den.toNat + (checkedCandidate precision num den shift).remainder.toNat = num.toNat * 2 ^ CandidateShift.toNat precision shift ∧ (checkedCandidate precision num den shift).remainder.toNat < den.toNat

The candidate selected by the fast-check-or-repair runtime path satisfies Euclidean division.

This is the consumer-facing form of checkedCandidate_complete: callers receive the exact equation and strict remainder bound directly, without reopening the executable certificate.

theorem FloatLib.Numerics.FixedWord.CertifiedDivision.roundQuotient_toNat (den quotient remainder : UInt128) (numerator : ℕ) (hdenFit : den.toNat < 2 ^ 127) (hdecomposition : quotient.toNat * den.toNat + remainder.toNat = numerator) (hremainder : remainder.toNat < den.toNat) (hquotientFit : quotient.toNat + 1 < 2 ^ 128) : (roundQuotient den quotient remainder).toNat = Numerics.roundQuotientEven numerator den.toNat

Native quotient rounding agrees with exact nearest-even rational rounding for a certified Euclidean decomposition.

theorem FloatLib.Numerics.FixedWord.CertifiedDivision.roundQuotient_toNat_eq_or (den quotient remainder : UInt128) (hquotientFit : quotient.toNat + 1 < 2 ^ 128) : (roundQuotient den quotient remainder).toNat = quotient.toNat ∨ (roundQuotient den quotient remainder).toNat = quotient.toNat + 1

Native quotient rounding returns the input quotient or its successor when incrementing fits.