Refinement of direct two-limb posit decoding

The two-limb backend inspects a packed 128-bit code without first rebuilding an arbitrary-precision natural. This module proves each primitive observation (zero detection, individual bits, regime length, fields, and the resulting dyadic value) equal to the exact-width posit model.

The proofs are separate from Decode.Runtime, so importing the decoder does not import these dependencies. Arithmetic refinements use toDyadic?_eq_model for stored words and the continuation laws for kernels that consume native significands directly.

theorem FloatLib.Floats.Formats.Posit.Model.NativeLimb.isZero_eq_true_iff (value : Numerics.FixedWord.UInt128) : isZero value = true ↔ value.toNat = 0

The fixed-limb zero test is exactly mathematical equality with zero.

theorem FloatLib.Floats.Formats.Posit.Model.NativeLimb.bitAt_eq_testBit (value : Numerics.FixedWord.UInt128) (index : ℕ) : bitAt value index = value.toNat.testBit index

Native two-limb bit inspection agrees with natural-number bit inspection.

theorem FloatLib.Floats.Formats.Posit.Model.NativeLimb.lowBits_toNat (value : Numerics.FixedWord.UInt128) (width : ℕ) : (lowBits value width).toNat = value.toNat % 2 ^ width

Two-limb low-bit extraction is exact at every zero-extended width.

theorem FloatLib.Floats.Formats.Posit.Model.NativeLimb.countLeadingZeros_eq_model (value : Numerics.FixedWord.UInt128) (width : ℕ) : countLeadingZeros value width = Model.countLeadingRun value.toNat width false

Native two-limb logarithmic zero counting agrees with the exact model scan.

theorem FloatLib.Floats.Formats.Posit.Model.NativeLimb.countLeadingRun_eq_model (value : Numerics.FixedWord.UInt128) (width : ℕ) (bit : Bool) : countLeadingRun value width bit = Model.countLeadingRun value.toNat width bit

Two-limb and reference-model regime scans return the same run length.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.NativeLimb.nonnegativeDyadicAt_negative (format : Format) (code : Numerics.FixedWord.UInt128) : (nonnegativeDyadicAt format code).negative = false

The direct candidate decoder always clears the sign field.

theorem FloatLib.Floats.Formats.Posit.Model.NativeLimb.lowBits_complement_increment_toNat (format : Format) (code : Numerics.FixedWord.UInt128) (heligible : Eligible format) (hcode : code.toNat < format.modulus) (hnonzero : code.toNat ≠ 0) : (lowBits (complement code).increment format.bits).toNat = format.modulus - code.toNat

Reducing a full-carrier two's complement to the format width yields exact-width subtraction.

Both magnitude extraction and sign restoration use this identity.

theorem FloatLib.Floats.Formats.Posit.Model.NativeLimb.toDyadic?_eq_model (format : Format) (code : Numerics.FixedWord.UInt128) (heligible : Eligible format) (hcode : code.toNat < format.modulus) : toDyadic? format code = (ofNatBits code.toNat).toDyadic?

The total two-limb decoder agrees with Model.toDyadic? on every in-range word.

theorem FloatLib.Floats.Formats.Posit.Model.NativeLimb.map_withTwoDyadicFields_eq_match_toDyadic? {α β : Type} (projection : α → β) (format : Format) (left right : Numerics.FixedWord.UInt128) (onNaR : α) (nativeContinuation : Bool → Numerics.FixedWord.UInt128 → ℤ → Bool → Numerics.FixedWord.UInt128 → ℤ → α) (exactContinuation : Bool → ℕ → ℤ → Bool → ℕ → ℤ → β) (hrefine : ∀ (leftNegative : Bool) (leftSignificand : Numerics.FixedWord.UInt128) (leftExponent : ℤ) (rightNegative : Bool) (rightSignificand : Numerics.FixedWord.UInt128) (rightExponent : ℤ), projection (nativeContinuation leftNegative leftSignificand leftExponent rightNegative rightSignificand rightExponent) = exactContinuation leftNegative leftSignificand.toNat leftExponent rightNegative rightSignificand.toNat rightExponent) : projection (withTwoDyadicFields format left right onNaR nativeContinuation) = match toDyadic? format left with | none => projection onNaR | some leftValue => match toDyadic? format right with | none => projection onNaR | some rightValue => exactContinuation leftValue.negative leftValue.significand leftValue.exponent rightValue.negative rightValue.significand rightValue.exponent

Projecting a carrier-valued two-input decoder agrees with an exact mathematical continuation whenever the carrier continuation satisfies the supplied pointwise refinement law.

Native binary kernels retain UInt128 significands; their refinements use the corresponding Nat values.

theorem FloatLib.Floats.Formats.Posit.Model.NativeLimb.withThreeDyadicFields_eq_match_toDyadic? {α : Type} (format : Format) (left right addend : Numerics.FixedWord.UInt128) (onNaR : α) (continuation : Bool → ℕ → ℤ → Bool → ℕ → ℤ → Bool → ℕ → ℤ → α) : (withThreeDyadicFields format left right addend onNaR fun (leftNegative : Bool) (leftSignificand : Numerics.FixedWord.UInt128) (leftExponent : ℤ) (rightNegative : Bool) (rightSignificand : Numerics.FixedWord.UInt128) (rightExponent : ℤ) (addendNegative : Bool) (addendSignificand : Numerics.FixedWord.UInt128) (addendExponent : ℤ) => continuation leftNegative leftSignificand.toNat leftExponent rightNegative rightSignificand.toNat rightExponent addendNegative addendSignificand.toNat addendExponent) = match toDyadic? format left with | none => onNaR | some leftValue => match toDyadic? format right with | none => onNaR | some rightValue => match toDyadic? format addend with | none => onNaR | some addendValue => continuation leftValue.negative leftValue.significand leftValue.exponent rightValue.negative rightValue.significand rightValue.exponent addendValue.negative addendValue.significand addendValue.exponent

Eliminating three native words is the nested exact-dyadic decoder.

The runtime continuation receives fixed-width significands while the theorem exposes their mathematical values to proof-facing clients.