Shared proofs for fixed-word posit backends

The executable boundaries for UInt8, UInt16, UInt32, and UInt64 remain separate so Lean can compile each one with its native calling convention. Their range arguments, however, are mathematical facts about the posit format rather than the carrier. This module holds those shared facts and keeps them out of the specialized runtime files.

theorem FloatLib.Floats.Formats.Posit.Configured.Backend.FixedWords.result_lt_capacity {format : Format} {capacity exactResult : ℕ} (width_le : format.bits ≤ capacity) (result_lt : exactResult < format.modulus) : exactResult < 2 ^ capacity

A result below the exact format modulus also fits any carrier at least as wide as the format.

theorem FloatLib.Floats.Formats.Posit.Configured.Backend.FixedWords.result_mod_capacity {format : Format} {capacity exactResult : ℕ} (width_le : format.bits ≤ capacity) (result_lt : exactResult < format.modulus) : exactResult % 2 ^ capacity = exactResult

Reducing an exact format result modulo a sufficiently wide carrier does not change the result.

theorem FloatLib.Floats.Formats.Posit.Configured.Backend.FixedWords.observed_lt_modulus {format : Format} {capacity observed exactResult : ℕ} (width_le : format.bits ≤ capacity) (observed_eq : observed = exactResult % 2 ^ capacity) (result_lt : exactResult < format.modulus) : observed < format.modulus

An observed result remains below the format modulus when narrowing to the carrier preserves the exact result.

Packed-word range invariants

theorem FloatLib.Floats.Formats.Posit.Configured.Backend.FixedWords.packedAdd_lt_modulus {format : Format} (eligible : Model.NativeWord.Eligible format) (left right : UInt64) (hleft : left.toNat < format.modulus) (hright : right.toNat < format.modulus) : (Model.NativeWordArithmetic.PackedSignedSum.addWordsCodeWordValid eligible left right hleft hright).toNat < format.modulus

Packed native-word addition returns a valid posit code.

theorem FloatLib.Floats.Formats.Posit.Configured.Backend.FixedWords.packedSub_lt_modulus {format : Format} (eligible : Model.NativeWord.Eligible format) (left right : UInt64) (hleft : left.toNat < format.modulus) (hright : right.toNat < format.modulus) : (Model.NativeWordArithmetic.PackedSignedSum.subWordsCodeWordValid eligible left right hleft hright).toNat < format.modulus

Packed native-word subtraction returns a valid posit code.

theorem FloatLib.Floats.Formats.Posit.Configured.Backend.FixedWords.packedMul_lt_modulus {format : Format} (eligible : Model.NativeWord.Eligible format) (left right : UInt64) (hleft : left.toNat < format.modulus) (hright : right.toNat < format.modulus) : (Model.NativeWordArithmetic.PackedProduct.mulWordsCodeWordValid eligible left right hleft hright).toNat < format.modulus

Packed native-word multiplication returns a valid posit code.

theorem FloatLib.Floats.Formats.Posit.Configured.Backend.FixedWords.packedDiv_lt_modulus {format : Format} (eligible : Model.NativeWord.Eligible format) (left right : UInt64) (hleft : left.toNat < format.modulus) (hright : right.toNat < format.modulus) : (Model.NativeWordArithmetic.PackedQuotient.divWordsCodeWordValid eligible left right hleft hright).toNat < format.modulus

Packed native-word division returns a valid posit code.

theorem FloatLib.Floats.Formats.Posit.Configured.Backend.FixedWords.packedSqrt_lt_modulus {format : Format} (eligible : Model.NativeWord.Eligible format) (value : UInt64) (hvalue : value.toNat < format.modulus) : (Model.NativeWordArithmetic.PackedSquareRoot.sqrtWordCodeWordValid eligible value hvalue).toNat < format.modulus

Packed native-word square root returns a valid posit code.

theorem FloatLib.Floats.Formats.Posit.Configured.Backend.FixedWords.packedFma_lt_modulus {format : Format} (eligible : Model.NativeWord.Eligible format) (left right addend : UInt64) (hleft : left.toNat < format.modulus) (hright : right.toNat < format.modulus) (haddend : addend.toNat < format.modulus) : (Model.NativeWordArithmetic.PackedSignedSum.fmaWordsCodeWordValid eligible left right addend hleft hright haddend).toNat < format.modulus

Packed native-word fused multiply-add returns a valid posit code.