Standard posit quire capacity

The Posit Standard (2022) 16n-bit quire satisfies two finite-term capacity guarantees:

• fewer than 2^(23 + 4n) ordinary posit addends cannot overflow the associated quire; and
• fewer than 2^31 exact products of two ordinary posits cannot overflow it.

The proof first bounds one posit relative to minPos, then transports that bound to the quire's fixed scale. A list-level absolute-value argument proves that every signed sum within the stated exclusive term limit remains an OrdinaryCoefficient, excluding both two's-complement overflow and the reserved quire-NaR word.

Accumulation applies these coefficient bounds to the executable accumulation loops.

References

• Posit Working Group, Standard for Posit Arithmetic (2022), March 2, 2022, Sections 3.4 and 5.11, https://posithub.org/docs/posit_standard-2.pdf.

def FloatLib.Floats.Formats.Posit.Quire.Model.positSumTermLimit (format : Format) : ℕ

Exclusive upper bound on the number of ordinary posit addends guaranteed to fit in a standard quire.

def FloatLib.Floats.Formats.Posit.Quire.Model.productSumTermLimit : ℕ

Exclusive upper bound on the number of exact posit products guaranteed to fit in a standard quire.

def FloatLib.Floats.Formats.Posit.Quire.Model.positCoefficientBound (format : Format) : ℕ

Uniform quire-coefficient magnitude bound for one ordinary posit.

def FloatLib.Floats.Formats.Posit.Quire.Model.productCoefficientBound (format : Format) : ℕ

Uniform quire-coefficient magnitude bound for one exact product of two ordinary posits.

theorem FloatLib.Floats.Formats.Posit.Quire.Model.natAbs_coefficientOfDyadic_le_positCoefficientBound {format : Format} (value : Posit.Model format) (dyadic : Numerics.Dyadic) (hvalue : value.toDyadic? = some dyadic) : (coefficientOfDyadic format dyadic).natAbs ≤ positCoefficientBound format

One ordinary posit contributes at most 2^(12(n-2)) quire coefficient units.

theorem FloatLib.Floats.Formats.Posit.Quire.Model.natAbs_coefficientOfDyadic_mul_le_productCoefficientBound {format : Format} (left right : Posit.Model format) (leftDyadic rightDyadic : Numerics.Dyadic) (hleft : left.toDyadic? = some leftDyadic) (hright : right.toDyadic? = some rightDyadic) : (coefficientOfDyadic format (leftDyadic.mul rightDyadic)).natAbs ≤ productCoefficientBound format

One exact product of two ordinary posits contributes at most 2^(16(n-2)) quire coefficient units.

theorem FloatLib.Floats.Formats.Posit.Quire.Model.ordinaryCoefficient_sum_of_length_lt_positSumTermLimit {format : Format} (coefficients : List ℤ) (hcoefficient : ∀ coefficient ∈ coefficients, coefficient.natAbs ≤ positCoefficientBound format) (hlength : coefficients.length < positSumTermLimit format) : OrdinaryCoefficient format coefficients.sum

Any coefficient list shorter than the ordinary-addend limit has an ordinary sum, provided each term satisfies the uniform posit coefficient bound.

theorem FloatLib.Floats.Formats.Posit.Quire.Model.ordinaryCoefficient_sum_of_length_lt_productSumTermLimit {format : Format} (coefficients : List ℤ) (hcoefficient : ∀ coefficient ∈ coefficients, coefficient.natAbs ≤ productCoefficientBound format) (hlength : coefficients.length < productSumTermLimit) : OrdinaryCoefficient format coefficients.sum

Any coefficient list shorter than the exact-product limit has an ordinary sum, provided each term satisfies the uniform product coefficient bound.