Mathlib ordering and enumeration for configured posits

Configured values use packed carriers selected from their static width. The certified codec is an equivalence with the exact-width model, so the standard posit order and finite enumeration can be transported through any lawful model codec, including primitive words, word pairs, and wide BitVec storage.

def FloatLib.Floats.Formats.Posit.Configured.Family.modelEquiv {format : Format} {plan : StoragePlan format} {code : Type} [ExecFloat.ModelCodec plan (Model format) code] : ExecFloat (Family format code plan) ≃ Model format

Certified equivalence between a configured runtime value and its exact-width proof model.

@[instance_reducible]

instance FloatLib.Floats.Formats.Posit.Configured.Family.instFinEnumExecFloat {format : Format} {plan : StoragePlan format} {code : Type} [ExecFloat.ModelCodec plan (Model format) code] : FinEnum (ExecFloat (Family format code plan))

Finite enumeration transported from all exact-width posit words.

@[instance_reducible]

instance FloatLib.Floats.Formats.Posit.Configured.Family.instLinearOrderExecFloat {format : Format} {plan : StoragePlan format} {code : Type} [ExecFloat.ModelCodec plan (Model format) code] : LinearOrder (ExecFloat (Family format code plan))

Standard posit comparison order on the public configured carrier.

The transport is representation-independent and preserves NaR as the least word under the two's-complement comparison rule. This is an order on encodings, including NaR. The DecidableEq field reuses the carrier's existing instance rather than a second one built from toModel.