Range and refinement laws for packed two-limb boundaries

The abstract theorems in this module let operation proofs reason about decoded options without unfolding the packed decoder. Re-encoding agrees with a model-valued operation whenever the NaR code and finite kernel agree separately.

theorem FloatLib.Floats.Formats.Posit.Model.NativeLimbPacked.Boundary.unaryCode_lt {narCode bound : ℕ} (operation : Numerics.Dyadic → ℕ) (value : Option Numerics.Dyadic) (hnarCode : narCode < bound) (hoperation : ∀ (finite : Numerics.Dyadic), operation finite < bound) : unaryCode narCode operation value < bound

A unary boundary is in range when both its NaR code and finite kernel are in range.

theorem FloatLib.Floats.Formats.Posit.Model.NativeLimbPacked.Boundary.binaryCode_lt {narCode bound : ℕ} (operation : Numerics.Dyadic → Numerics.Dyadic → ℕ) (left right : Option Numerics.Dyadic) (hnarCode : narCode < bound) (hoperation : ∀ (leftValue rightValue : Numerics.Dyadic), operation leftValue rightValue < bound) : binaryCode narCode operation left right < bound

A binary boundary is in range when its NaR code and every finite result are in range.

theorem FloatLib.Floats.Formats.Posit.Model.NativeLimbPacked.Boundary.ternaryCode_lt {narCode bound : ℕ} (operation : Numerics.Dyadic → Numerics.Dyadic → Numerics.Dyadic → ℕ) (left right third : Option Numerics.Dyadic) (hnarCode : narCode < bound) (hoperation : ∀ (leftValue rightValue thirdValue : Numerics.Dyadic), operation leftValue rightValue thirdValue < bound) : ternaryCode narCode operation left right third < bound

A ternary boundary is in range when its NaR code and every finite result are in range.

theorem FloatLib.Floats.Formats.Posit.Model.NativeLimbPacked.Boundary.ofNatBits_unaryCode {format : Format} (narCode : ℕ) (operation : Numerics.Dyadic → ℕ) (semantic : Numerics.Dyadic → Model format) (value : Option Numerics.Dyadic) (hnarCode : ofNatBits narCode = nar format) (hoperation : ∀ (finite : Numerics.Dyadic), ofNatBits (operation finite) = semantic finite) : ofNatBits (unaryCode narCode operation value) = unaryResult (nar format) semantic value

Re-encoding a unary boundary agrees with its model-valued operation when the NaR code and finite kernel do. The decoded option remains abstract throughout the proof.

theorem FloatLib.Floats.Formats.Posit.Model.NativeLimbPacked.Boundary.ofNatBits_unaryCode_of_eq {format : Format} (narCode : ℕ) (operation : Numerics.Dyadic → ℕ) (semantic : Numerics.Dyadic → Model format) (encodedValue semanticValue : Option Numerics.Dyadic) (hvalue : encodedValue = semanticValue) (hnarCode : ofNatBits narCode = nar format) (hoperation : ∀ (finite : Numerics.Dyadic), ofNatBits (operation finite) = semantic finite) : ofNatBits (unaryCode narCode operation encodedValue) = unaryResult (nar format) semantic semanticValue

Unary refinement with separate encoded and semantic decoder results. Keeping their equality as an argument avoids rewriting inside a concrete packed-decoder expression in operation modules.

theorem FloatLib.Floats.Formats.Posit.Model.NativeLimbPacked.Boundary.ofNatBits_binaryCode {format : Format} (narCode : ℕ) (operation : Numerics.Dyadic → Numerics.Dyadic → ℕ) (semantic : Numerics.Dyadic → Numerics.Dyadic → Model format) (left right : Option Numerics.Dyadic) (hnarCode : ofNatBits narCode = nar format) (hoperation : ∀ (leftValue rightValue : Numerics.Dyadic), ofNatBits (operation leftValue rightValue) = semantic leftValue rightValue) : ofNatBits (binaryCode narCode operation left right) = binaryResult (nar format) semantic left right

Re-encoding a binary boundary agrees with its model-valued operation when the NaR code and finite kernel do.

theorem FloatLib.Floats.Formats.Posit.Model.NativeLimbPacked.Boundary.ofNatBits_binaryCode_of_eq {format : Format} (narCode : ℕ) (operation : Numerics.Dyadic → Numerics.Dyadic → ℕ) (semantic : Numerics.Dyadic → Numerics.Dyadic → Model format) (encodedLeft encodedRight semanticLeft semanticRight : Option Numerics.Dyadic) (hleft : encodedLeft = semanticLeft) (hright : encodedRight = semanticRight) (hnarCode : ofNatBits narCode = nar format) (hoperation : ∀ (leftValue rightValue : Numerics.Dyadic), ofNatBits (operation leftValue rightValue) = semantic leftValue rightValue) : ofNatBits (binaryCode narCode operation encodedLeft encodedRight) = binaryResult (nar format) semantic semanticLeft semanticRight

Binary refinement with separate encoded and semantic decoder results. The equalities are consumed by this small abstract theorem rather than by each packed operation proof.

theorem FloatLib.Floats.Formats.Posit.Model.NativeLimbPacked.Boundary.ofNatBits_ternaryCode {format : Format} (narCode : ℕ) (operation : Numerics.Dyadic → Numerics.Dyadic → Numerics.Dyadic → ℕ) (semantic : Numerics.Dyadic → Numerics.Dyadic → Numerics.Dyadic → Model format) (left right third : Option Numerics.Dyadic) (hnarCode : ofNatBits narCode = nar format) (hoperation : ∀ (leftValue rightValue thirdValue : Numerics.Dyadic), ofNatBits (operation leftValue rightValue thirdValue) = semantic leftValue rightValue thirdValue) : ofNatBits (ternaryCode narCode operation left right third) = ternaryResult (nar format) semantic left right third

Re-encoding a ternary boundary agrees with its model-valued operation when the NaR code and finite kernel do.

theorem FloatLib.Floats.Formats.Posit.Model.NativeLimbPacked.Boundary.ofNatBits_ternaryCode_of_eq {format : Format} (narCode : ℕ) (operation : Numerics.Dyadic → Numerics.Dyadic → Numerics.Dyadic → ℕ) (semantic : Numerics.Dyadic → Numerics.Dyadic → Numerics.Dyadic → Model format) (encodedLeft encodedRight encodedThird semanticLeft semanticRight semanticThird : Option Numerics.Dyadic) (hleft : encodedLeft = semanticLeft) (hright : encodedRight = semanticRight) (hthird : encodedThird = semanticThird) (hnarCode : ofNatBits narCode = nar format) (hoperation : ∀ (leftValue rightValue thirdValue : Numerics.Dyadic), ofNatBits (operation leftValue rightValue thirdValue) = semantic leftValue rightValue thirdValue) : ofNatBits (ternaryCode narCode operation encodedLeft encodedRight encodedThird) = ternaryResult (nar format) semantic semanticLeft semanticRight semanticThird

Ternary refinement with distinct packed and semantic decoder results.